Safe Haskell | None |
---|---|
Language | Haskell98 |
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) |
(Eq v, Eq f) => Eq (CTerm v f) Source | |
(Data v, Data f) => Data (CTerm v f) Source | |
(Ord v, Ord f) => Ord (CTerm v f) Source | |
(Variable v, Function f v) => Term (CTerm v f) v f Source | |
(Variable v, Predicate p, Function f v) => Apply (Sentence v p f) p (CTerm v f) Source | |
Predicate p => AtomEq (Sentence v p f) p (CTerm v f) Source |
data Connective Source
data Quantifier Source
data ConjunctiveNormalForm v p f Source
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 |
(Eq v, Eq f) => Eq (NormalTerm v f) Source | |
(Data v, Data f) => Data (NormalTerm v f) Source | |
(Ord v, Ord f) => Ord (NormalTerm v f) Source | |
(Variable v, Function f v) => Term (NormalTerm v f) v f Source |
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