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

Data.Logic.Types.Harrison.Formulas.FirstOrder

Documentation

data Formula a Source

Constructors

 F T Atom a Not (Formula a) And (Formula a) (Formula a) Or (Formula a) (Formula a) Imp (Formula a) (Formula a) Iff (Formula a) (Formula a) Forall String (Formula a) Exists String (Formula a)

Instances

 Eq a => Eq (Formula a) (Eq (Formula a), Ord a) => Ord (Formula a) Show (Formula FOLEQ) Negatable (Formula atom) HasFixity (Formula FOLEQ) FirstOrderFormula (Formula a) a String => Pretty (Formula a) Negatable (Formula a) => Combinable (Formula a) Constants (Formula a) (Constants a, Pretty a, HasFixity a) => Formula (Formula a) a (Ord (Formula FOLEQ), Negatable (Formula FOLEQ), Combinable (Formula FOLEQ), Constants (Formula FOLEQ), Pretty (Formula FOLEQ), HasFixity (Formula FOLEQ), Formula (Formula FOLEQ) FOLEQ) => PropositionalFormula (Formula FOLEQ) FOLEQ (Negatable (Formula FOLEQ), Constants (Formula FOLEQ), HasFixity FOLEQ, Ord (Formula FOLEQ), Formula (Formula FOLEQ) FOLEQ) => Literal (Formula FOLEQ) FOLEQ (Combinable (Formula a), Constants (Formula a), Variable String, Pretty String, Formula (Formula a) a, Constants a, Pretty a, HasFixity a) => FirstOrderFormula (Formula a) a String