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

Safe Haskell None

Data.Logic.Instances.Chiou

# Documentation

data Sentence v p f Source

Constructors

 Connective (Sentence v p f) Connective (Sentence v p f) Quantifier Quantifier [v] (Sentence v p f) Not (Sentence v p f) Predicate p [CTerm v f] Equal (CTerm v f) (CTerm v f)

Instances

 Typeable3 Sentence (Eq v, Eq p, Eq f) => Eq (Sentence v p f) (Typeable (Sentence v p f), Data v, Data p, Data f) => Data (Sentence v p f) (Eq (Sentence v p f), Ord v, Ord p, Ord f) => Ord (Sentence v p f) Negatable (Sentence v p f) (Formula (Sentence v p f) (Sentence v p f), Predicate p, Function f v, Variable v) => HasFixity (Sentence v p f) (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Variable v, Predicate p, Function f v) => Pretty (Sentence v p f) (Negatable (Sentence v p f), Ord v, Ord p, Ord f) => Combinable (Sentence v p f) (Constants p, Eq (Sentence v p f)) => Constants (Sentence v p f) (Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f) Predicate p => AtomEq (Sentence v p f) p (CTerm v f) (Predicate p, Function f v) => Formula (Sentence v p f) (Sentence v p f) (Ord (Sentence v p f), Negatable (Sentence v p f), Constants (Sentence v p f), Pretty (Sentence v p f), HasFixity (Sentence v p 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) (Combinable (Sentence v p f), Constants (Sentence v p f), Constants (Sentence v p f), HasFixity (Sentence v p f), Pretty (Sentence v p f), Pretty v, Formula (Sentence v p f) (Sentence v p f), Variable v, Predicate p, Function f v) => FirstOrderFormula (Sentence v p f) (Sentence v p f) v

data CTerm v f Source

Constructors

 Function f [CTerm v f] Variable v

Instances

 Typeable2 CTerm (Eq v, Eq f) => Eq (CTerm v f) (Typeable (CTerm v f), Data v, Data f) => Data (CTerm v f) (Eq (CTerm v f), Ord v, Ord f) => Ord (CTerm v f) (Ord (CTerm v f), Variable v, Function f v) => Term (CTerm v f) v f (Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f) Predicate p => AtomEq (Sentence v p f) p (CTerm v f)

data Connective Source

Constructors

 Imply Equiv And Or

Instances

 Eq Connective Data Connective Ord Connective Show Connective Typeable Connective

data Quantifier Source

Constructors

 ForAll ExistsCh

Instances

 Eq Quantifier Data Quantifier Ord Quantifier Show Quantifier Typeable Quantifier

data ConjunctiveNormalForm v p f Source

Constructors

 CNF [Sentence v p f]

Instances

 (Eq v, Eq p, Eq f) => Eq (ConjunctiveNormalForm v p f)

data NormalSentence v p f Source

Constructors

 NFNot (NormalSentence v p f) NFPredicate p [NormalTerm v f] NFEqual (NormalTerm v f) (NormalTerm v f)

Instances

 Typeable3 NormalSentence (Eq v, Eq p, Eq f) => Eq (NormalSentence v p f) (Typeable (NormalSentence v p f), Data v, Data p, Data f) => Data (NormalSentence v p f) (Eq (NormalSentence v p f), Ord v, Ord p, Ord f) => Ord (NormalSentence v p f) Negatable (NormalSentence v p f) (Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Predicate p, Function f v, Variable v) => HasFixity (NormalSentence v p f) (Formula (NormalSentence v p f) (NormalSentence v p f), Variable v, Predicate p, Function f v, Combinable (NormalSentence v p f)) => Pretty (NormalSentence v p f) (Constants p, Eq (NormalSentence v p f)) => Constants (NormalSentence v p f) (Predicate p, Function f v, Combinable (NormalSentence v p f)) => Formula (NormalSentence v p f) (NormalSentence v p f) (Constants (NormalSentence v p f), Constants (NormalSentence v p f), HasFixity (NormalSentence v p f), Pretty (NormalSentence v p f), Pretty v, Formula (NormalSentence v p f) (NormalSentence v p f), Combinable (NormalSentence v p f), Term (NormalTerm v f) v f, Variable v, Predicate p, Function f v) => FirstOrderFormula (NormalSentence v p f) (NormalSentence v p f) v

data NormalTerm v f Source

Constructors

 NormalFunction f [NormalTerm v f] NormalVariable v

Instances

 Typeable2 NormalTerm (Eq v, Eq f) => Eq (NormalTerm v f) (Typeable (NormalTerm v f), Data v, Data f) => Data (NormalTerm v f) (Eq (NormalTerm v f), Ord v, Ord f) => Ord (NormalTerm v f) (Ord (NormalTerm v f), Variable v, Function f v) => Term (NormalTerm v f) v f

toSentence :: (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Atom (Sentence v p f) (CTerm v f) v, Function f v, Variable v, Predicate p) => NormalSentence v p f -> Sentence v p fSource

fromSentence :: forall v p f. (FirstOrderFormula (Sentence v p f) (Sentence v p f) v, Predicate p) => Sentence v p f -> NormalSentence v p fSource