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

Safe HaskellNone
LanguageHaskell98

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

Typeable (* -> * -> * -> *) Sentence 
(Eq v, Eq p, Eq f) => Eq (Sentence v p f) 
(Data v, Data p, Data f) => Data (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) 
(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) 
(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) 
(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

(Eq v, Eq f) => Eq (CTerm v f) 
(Data v, Data f) => Data (CTerm v f) 
(Ord v, Ord f) => Ord (CTerm v f) 
Typeable (* -> * -> *) CTerm 
(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

data Quantifier Source

Constructors

ForAll 
ExistsCh 

Instances

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

data NormalTerm v f Source

Constructors

NormalFunction f [NormalTerm v f] 
NormalVariable v 

Instances

(Eq v, Eq f) => Eq (NormalTerm v f) 
(Data v, Data f) => Data (NormalTerm v f) 
(Ord v, Ord f) => Ord (NormalTerm v f) 
Typeable (* -> * -> *) NormalTerm 
(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 f Source

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