Safe Haskell | None |
---|
Documentation
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) |
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
data Quantifier Source
data ConjunctiveNormalForm v p f Source
(Eq v, Eq p, Eq f) => Eq (ConjunctiveNormalForm v p f) |
data NormalSentence v p f Source
NFNot (NormalSentence v p f) | |
NFPredicate p [NormalTerm v f] | |
NFEqual (NormalTerm v f) (NormalTerm v f) |
data NormalTerm v f Source
NormalFunction f [NormalTerm v f] | |
NormalVariable v |
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