logic-classes-1.4.8: Framework for propositional and first order logic, theorem proving

Safe HaskellSafe-Inferred




class Negatable formula whereSource

The class of formulas that can be negated. There are some types that can be negated but do not support the other Boolean Logic operators, such as the Literal class.


negatePrivate :: formula -> formulaSource

Negate a formula in a naive fashion, the operators below prevent double negation.



:: (formula -> r)

called for normal formulas

-> (formula -> r)

called for negated formulas

-> formula 
-> r 

Test whether a formula is negated or normal

negated :: Negatable formula => formula -> BoolSource

Is this formula negated at the top level?

(.~.) :: Negatable formula => formula -> formulaSource

Negate the formula, avoiding double negation

(¬) :: Negatable formula => formula -> formulaSource

negative :: Negatable formula => formula -> BoolSource

positive :: Negatable formula => formula -> BoolSource