Safe Haskell | None |
---|---|
Language | Haskell98 |
PropositionalFormula is a multi-parameter type class for representing instance of propositional (aka zeroth order) logic datatypes. These are formulas which have truth values, but no "for all" or "there exists" quantifiers and thus no variables or terms as we have in first order or predicate logic. It is intended that we will be able to write instances for various different implementations to allow these systems to interoperate. The operator names were adopted from the Logic-TPTP package.
- class (Ord formula, Negatable formula, Combinable formula, Constants formula, Pretty formula, HasFixity formula, Formula formula atom) => PropositionalFormula formula atom | formula -> atom where
- foldPropositional :: (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> r
- showPropositional :: PropositionalFormula formula atom => (atom -> String) -> formula -> String
- prettyPropositional :: (PropositionalFormula formula atom, HasFixity formula) => (atom -> Doc) -> Fixity -> formula -> Doc
- fixityPropositional :: (HasFixity atom, PropositionalFormula formula atom) => formula -> Fixity
- convertProp :: forall formula1 atom1 formula2 atom2. (PropositionalFormula formula1 atom1, PropositionalFormula formula2 atom2) => (atom1 -> atom2) -> formula1 -> formula2
- combine :: Combinable formula => Combination formula -> formula
- negationNormalForm :: PropositionalFormula formula atom => formula -> formula
- clauseNormalForm :: forall formula atom. PropositionalFormula formula atom => formula -> formula
- clauseNormalForm' :: PropositionalFormula formula atom => formula -> Set (Set formula)
- clauseNormalFormAlt :: forall formula atom. PropositionalFormula formula atom => formula -> formula
- clauseNormalFormAlt' :: PropositionalFormula formula atom => formula -> Set (Set formula)
- disjunctiveNormalForm :: PropositionalFormula formula atom => formula -> formula
- disjunctiveNormalForm' :: (PropositionalFormula formula atom, Eq formula) => formula -> Set (Set formula)
- overatoms :: forall formula atom r. PropositionalFormula formula atom => (atom -> r -> r) -> formula -> r -> r
- foldAtomsPropositional :: PropositionalFormula pf atom => (r -> atom -> r) -> r -> pf -> r
- mapAtomsPropositional :: forall formula atom. PropositionalFormula formula atom => (atom -> formula) -> formula -> formula
Documentation
class (Ord formula, Negatable formula, Combinable formula, Constants formula, Pretty formula, HasFixity formula, Formula formula atom) => PropositionalFormula formula atom | formula -> atom where Source
A type class for propositional logic. If the type we are writing an instance for is a zero-order (aka propositional) logic type there will generally by a type or a type parameter corresponding to atom. For first order or predicate logic types, it is generally easiest to just use the formula type itself as the atom type, and raise errors in the implementation if a non-atomic formula somehow appears where an atomic formula is expected (i.e. as an argument to atomic or to the third argument of foldPropositional.)
The Ord superclass is required so we can put formulas in sets during the normal form computations. Negatable and Combinable are also considered basic operations that we can't build this package without. It is less obvious whether Constants is always required, but the implementation of functions like simplify would be more elaborate if we didn't have it, so we will require it.
foldPropositional :: (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> r Source
Build an atomic formula from the atom type. | A fold function that distributes different sorts of formula to its parameter functions, one to handle binary operators, one for negations, and one for atomic formulas. See examples of its use to implement the polymorphic functions below.
showPropositional :: PropositionalFormula formula atom => (atom -> String) -> formula -> String Source
Show a formula in a format that can be evaluated
:: (PropositionalFormula formula atom, HasFixity formula) | |
=> (atom -> Doc) | |
-> Fixity | The fixity of the parent formula. If the operator being formatted here has a lower precedence it needs to be parenthesized. |
-> formula | |
-> Doc |
Show a formula in a visually pleasing format.
fixityPropositional :: (HasFixity atom, PropositionalFormula formula atom) => formula -> Fixity Source
convertProp :: forall formula1 atom1 formula2 atom2. (PropositionalFormula formula1 atom1, PropositionalFormula formula2 atom2) => (atom1 -> atom2) -> formula1 -> formula2 Source
Convert any instance of a propositional logic expression to any other using the supplied atom conversion function.
combine :: Combinable formula => Combination formula -> formula Source
A helper function for building folds:
foldPropositional combine atomic
is a no-op.
negationNormalForm :: PropositionalFormula formula atom => formula -> formula Source
Simplify and recursively apply nnf.
clauseNormalForm :: forall formula atom. PropositionalFormula formula atom => formula -> formula Source
clauseNormalForm' :: PropositionalFormula formula atom => formula -> Set (Set formula) Source
clauseNormalFormAlt :: forall formula atom. PropositionalFormula formula atom => formula -> formula Source
clauseNormalFormAlt' :: PropositionalFormula formula atom => formula -> Set (Set formula) Source
I'm not sure of the clauseNormalForm functions above are wrong or just different.
disjunctiveNormalForm :: PropositionalFormula formula atom => formula -> formula Source
disjunctiveNormalForm' :: (PropositionalFormula formula atom, Eq formula) => formula -> Set (Set formula) Source
overatoms :: forall formula atom r. PropositionalFormula formula atom => (atom -> r -> r) -> formula -> r -> r Source
Deprecated - use foldAtoms.
foldAtomsPropositional :: PropositionalFormula pf atom => (r -> atom -> r) -> r -> pf -> r Source
Use this to implement foldAtoms
mapAtomsPropositional :: forall formula atom. PropositionalFormula formula atom => (atom -> formula) -> formula -> formula Source