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

Data.Logic.Types.FirstOrder

Description

Data types which are instances of the Logic type class for use when you just want to use the classes and you don't have a particular representation you need to use.

Synopsis

# Documentation

data Formula v p f Source

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

Constructors

 Predicate (Predicate p (PTerm v f)) Combine (Combination (Formula v p f)) Quant Quant v (Formula v p f)

Instances

 Typeable3 Formula Bijection (Combination (Formula v p f)) (Combination (Formula v p f)) (Eq v, Eq p, Eq f) => Eq (Formula v p f) (Typeable (Formula v p f), Data v, Data p, Data f) => Data (Formula v p f) (Eq (Formula v p f), Ord v, Ord p, Ord f) => Ord (Formula v p f) (Read v, Read p, Read f) => Read (Formula v p f) (Show v, Show p, Show f) => Show (Formula v p f) (SafeCopy v0, SafeCopy p0, SafeCopy f0) => SafeCopy (Formula v0 p0 f0) Negatable (Formula v p f) (Formula (Formula v p f) (Predicate p (PTerm v f)), Predicate p, Variable v, Function f v, HasFixity (Predicate p (PTerm v f))) => HasFixity (Formula v p f) (Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => Pretty (Formula v p f) (Negatable (Formula v p f), Constants (Formula v p f)) => Combinable (Formula v p f) Constants p => Constants (Formula v p f) (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f)) (Ord (Formula v p f), Negatable (Formula v p f), Pretty (Formula v p f), HasFixity (Formula v p f), 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)) (Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f)) (Combinable (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v Bijection (Formula v p f) (Formula v p f)

data PTerm v f Source

The range of a term is an element of a set.

Constructors

 Var v A variable, either free or bound by an enclosing quantifier. FunApp f [PTerm v f] Function application. Constants are encoded as nullary functions. The result is another term.

Instances

 Typeable2 PTerm (Eq v, Eq f) => Eq (PTerm v f) (Typeable (PTerm v f), Data v, Data f) => Data (PTerm v f) (Eq (PTerm v f), Ord v, Ord f) => Ord (PTerm v f) (Read v, Read f) => Read (PTerm v f) (Show v, Show f) => Show (PTerm v f) (SafeCopy v0, SafeCopy f0) => SafeCopy (PTerm v0 f0) (Variable v, Pretty v, Predicate p, Pretty p, Function f v, Pretty f) => Pretty (Predicate p (PTerm v f)) Constants p => Constants (Predicate p (PTerm v f)) (Ord (PTerm v f), Variable v, Function f v) => Term (PTerm v f) v f Predicate p => AtomEq (Predicate p (PTerm v f)) p (PTerm v f) (Predicate p, Variable v, Function f v) => Atom (Predicate p (PTerm v f)) (PTerm v f) v (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f)) (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f)) (Ord (Formula v p f), Negatable (Formula v p f), Pretty (Formula v p f), HasFixity (Formula v p f), 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)) (Ord (Formula v p f), Negatable (Formula v p f), Combinable (Formula v p f), Constants (Formula v p f), Pretty (Formula v p 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)) (Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f)) (Combinable (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v (Combinable (Formula v p f), Constants (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v

data Predicate p term Source

A temporary type used in the fold method to represent the combination of a predicate and its arguments. This reduces the number of arguments to foldFirstOrder and makes it easier to manage the mapping of the different instances to the class methods.

Constructors

 Equal term term Apply p [term]

Instances

 Typeable2 Predicate (Eq p, Eq term) => Eq (Predicate p term) (Typeable (Predicate p term), Data p, Data term) => Data (Predicate p term) (Eq (Predicate p term), Ord p, Ord term) => Ord (Predicate p term) (Read p, Read term) => Read (Predicate p term) (Show p, Show term) => Show (Predicate p term) (SafeCopy (MigrateFrom (Predicate p term)), SafeCopy p, SafeCopy term) => Migrate (Predicate p term) (SafeCopy p0, SafeCopy term0) => SafeCopy (Predicate p0 term0) HasFixity (Predicate p term) (Variable v, Pretty v, Predicate p, Pretty p, Function f v, Pretty f) => Pretty (Predicate p (PTerm v f)) Constants p => Constants (Predicate p (PTerm v f)) Predicate p => AtomEq (Predicate p (PTerm v f)) p (PTerm v f) (Predicate p, Variable v, Function f v) => Atom (Predicate p (PTerm v f)) (PTerm v f) v (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f)) (Predicate p, Function f v) => Formula (Formula v p f) (Predicate p (PTerm v f)) (Ord (Formula v p f), Negatable (Formula v p f), Pretty (Formula v p f), HasFixity (Formula v p f), 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)) (Ord (Formula v p f), Negatable (Formula v p f), Combinable (Formula v p f), Constants (Formula v p f), Pretty (Formula v p 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)) (Negatable (Formula v p f), Constants (Formula v p f), HasFixity (Predicate p (PTerm v f)), Ord (Formula v p f), Constants p, Ord v, Ord p, Ord f, Constants (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f))) => Literal (Formula v p f) (Predicate p (PTerm v f)) (Combinable (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), AtomEq (Predicate p (PTerm v f)) p (PTerm v f), Constants (Formula v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v (Combinable (Formula v p f), Constants (Formula v p f), Constants (Predicate p (PTerm v f)), HasFixity (Predicate p (PTerm v f)), Pretty (Predicate p (PTerm v f)), Pretty v, Formula (Formula v p f) (Predicate p (PTerm v f)), Formula (Formula v p f) (Predicate p (PTerm v f)), Variable v, Predicate p, Function f v) => FirstOrderFormula (Formula v p f) (Predicate p (PTerm v f)) v