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

Combinable (PropForm a) | |

Ord atom => Combinable (Formula atom) | |

Combinable (Formula a) | |

Combinable (Formula a) | |

(Ord v, Ord p, Ord f) => Combinable (Sentence v p f) | |

Constants (Formula v p f) => Combinable (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) | |

Data formula => Data (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