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

Data.Logic.Types.Propositional

Synopsis

Documentation

data Formula atom Source

The range of a formula is {True, False} when it has no free variables.

Constructors

 Combine (Combination (Formula atom)) Atom atom T F

Instances

 Typeable1 Formula Eq atom => Eq (Formula atom) (Typeable (Formula atom), Data atom) => Data (Formula atom) (Eq (Formula atom), Ord atom) => Ord (Formula atom) Show (Formula (Atom Int)) Negatable (Formula atom) (Pretty atom, HasFixity atom, Ord atom) => HasFixity (Formula atom) (Pretty atom, HasFixity atom, Ord atom) => Pretty (Formula atom) (Negatable (Formula atom), Ord atom) => Combinable (Formula atom) Constants (Formula atom) (Pretty atom, HasFixity atom, Ord atom) => Formula (Formula atom) atom (Ord (Formula atom), Negatable (Formula atom), Combinable (Formula atom), Constants (Formula atom), Pretty (Formula atom), HasFixity (Formula atom), Formula (Formula atom) atom, Pretty atom, HasFixity atom, Ord atom) => PropositionalFormula (Formula atom) atom (Negatable (Formula atom), Constants (Formula atom), Formula (Formula atom) atom, Ord (Formula atom), Pretty atom, HasFixity atom, Ord atom) => Literal (Formula atom) atom