Safe Haskell | None |
---|
Class Logic defines the basic boolean logic operations, AND, OR, NOT, and so on. Definitions which pertain to both propositional and first order logic are here.
- class Negatable formula => Combinable formula where
- (.|.) :: formula -> formula -> formula
- (.&.) :: formula -> formula -> formula
- (.<=>.) :: formula -> formula -> formula
- (.=>.) :: formula -> formula -> formula
- (.<=.) :: formula -> formula -> formula
- (.<~>.) :: formula -> formula -> formula
- (.~|.) :: formula -> formula -> formula
- (.~&.) :: formula -> formula -> formula
- data Combination formula
- combine :: Combinable formula => Combination formula -> formula
- data BinOp
- binop :: Combinable formula => formula -> BinOp -> formula -> formula
- (∧) :: Combinable formula => formula -> formula -> formula
- (∨) :: Combinable formula => formula -> formula -> formula
- (⇒) :: Combinable formula => formula -> formula -> formula
- (⇔) :: Combinable formula => formula -> formula -> formula
- (==>) :: Combinable formula => formula -> formula -> formula
- (<=>) :: Combinable formula => formula -> formula -> formula
- prettyBinOp :: BinOp -> Doc
Documentation
class Negatable formula => Combinable formula whereSource
A type class for logical formulas. Minimal implementation:
(.|.)
(.|.) :: formula -> formula -> formulaSource
Disjunction/OR
(.&.) :: formula -> formula -> formulaSource
Derived formula combinators. These could (and should!) be overridden with expressions native to the instance.
| Conjunction/AND
(.<=>.) :: formula -> formula -> formulaSource
Formula combinators: Equivalence
(.=>.) :: formula -> formula -> formulaSource
Implication
(.<=.) :: formula -> formula -> formulaSource
Reverse implication:
(.<~>.) :: formula -> formula -> formulaSource
Exclusive or
(.~|.) :: formula -> formula -> formulaSource
Nor
(.~&.) :: formula -> formula -> formulaSource
Nand
Negatable (PropForm a) => Combinable (PropForm a) | |
(Negatable (Formula atom), Ord atom) => Combinable (Formula atom) | |
Negatable (Formula a) => Combinable (Formula a) | |
Negatable (Formula a) => Combinable (Formula a) | |
(Negatable (Sentence v p f), Ord v, Ord p, Ord f) => Combinable (Sentence v p f) | |
(Negatable (Formula v p f), Constants (Formula v p f)) => Combinable (Formula v p f) | |
(Negatable (Formula v p f), Formula (Formula v p f) (Predicate p (PTerm v f)), Constants (Formula v p f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => Combinable (Formula v p f) |
data Combination formula Source
Combination
is a helper type used in the signatures of the
foldPropositional
and foldFirstOrder
methods so can represent
all the ways that formulas can be combined using boolean logic -
negation, logical And, and so forth.
Typeable1 Combination | |
Eq formula => Eq (Combination formula) | |
(Typeable (Combination formula), Data formula) => Data (Combination formula) | |
(Eq (Combination formula), Ord formula) => Ord (Combination formula) | |
Read formula => Read (Combination formula) | |
Show formula => Show (Combination formula) | |
SafeCopy formula0 => SafeCopy (Combination formula0) | |
Bijection (Combination (Formula v p f)) (Combination (Formula v p f)) |
combine :: Combinable formula => Combination formula -> formulaSource
A helper function for building folds:
foldPropositional combine atomic
is a no-op.
Represents the boolean logic binary operations, used in the Combination type above.
binop :: Combinable formula => formula -> BinOp -> formula -> formulaSource
Unicode aliases for Combinable class methods
(∧) :: Combinable formula => formula -> formula -> formulaSource
(∨) :: Combinable formula => formula -> formula -> formulaSource
(⇒) :: Combinable formula => formula -> formula -> formulaSource
⇒ can't be a function when -XUnicodeSyntax is enabled.
(⇔) :: Combinable formula => formula -> formula -> formulaSource
Use in Harrison's code
(==>) :: Combinable formula => formula -> formula -> formulaSource
(<=>) :: Combinable formula => formula -> formula -> formulaSource
prettyBinOp :: BinOp -> DocSource