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

Data.Logic.Classes.Propositional

Description

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.

Synopsis

# Documentation

class (Ord formula, Negatable formula, Combinable formula, Constants formula, Pretty formula, HasFixity formula, Formula formula atom) => PropositionalFormula formula atom | formula -> atom whereSource

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.

Methods

foldPropositional :: (Combination formula -> r) -> (Bool -> r) -> (atom -> r) -> formula -> rSource

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.

Instances

 (Combinable (PropForm a), Pretty a, HasFixity a, Ord a) => PropositionalFormula (PropForm a) a (Formula (Formula atom) atom, Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom (Combinable (Formula atom), Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom Formula (Formula FOLEQ) FOLEQ => PropositionalFormula (Formula FOLEQ) FOLEQ (Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v, Constants (Formula v p f), Combinable (Formula v p f)) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f)) (Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Show v, Show p, Show f, HasFixity (Formula v p f), Variable v, Predicate p, Function f v) => PropositionalFormula (Formula v p f) (Predicate p (PTerm v f)) (Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v, Combinable (Sentence v p f)) => PropositionalFormula (Sentence v p f) (Sentence v p f)

showPropositional :: PropositionalFormula formula atom => (atom -> String) -> formula -> StringSource

Show a formula in a format that can be evaluated

Arguments

 :: (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 -> FixitySource

convertProp :: forall formula1 atom1 formula2 atom2. (PropositionalFormula formula1 atom1, PropositionalFormula formula2 atom2) => (atom1 -> atom2) -> formula1 -> formula2Source

Convert any instance of a propositional logic expression to any other using the supplied atom conversion function.

combine :: Combinable formula => Combination formula -> formulaSource

A helper function for building folds: ``` foldPropositional combine atomic ``` is a no-op.

negationNormalForm :: PropositionalFormula formula atom => formula -> formulaSource

Simplify and recursively apply nnf.

clauseNormalForm :: forall formula atom. PropositionalFormula formula atom => formula -> formulaSource

clauseNormalForm' :: PropositionalFormula formula atom => formula -> Set (Set formula)Source

clauseNormalFormAlt :: forall formula atom. PropositionalFormula formula atom => formula -> formulaSource

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 -> formulaSource

disjunctiveNormalForm' :: (PropositionalFormula formula atom, Eq formula) => formula -> Set (Set formula)Source

overatoms :: forall formula atom r. PropositionalFormula formula atom => (atom -> r -> r) -> formula -> r -> rSource

Deprecated - use foldAtoms.

foldAtomsPropositional :: PropositionalFormula pf atom => (r -> atom -> r) -> r -> pf -> rSource

Use this to implement foldAtoms

mapAtomsPropositional :: forall formula atom. PropositionalFormula formula atom => (atom -> formula) -> formula -> formulaSource