Data.Logic.Instances.Chiou

Documentation

data Sentence v p f

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

(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

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)

(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

Constructors

Imply

Equiv

And

Or

Instances

Eq Connective

Data Connective

Ord Connective

Show Connective

data Quantifier

Constructors

ForAll

ExistsCh

Instances

Eq Quantifier

Data Quantifier

Ord Quantifier

Show Quantifier

data ConjunctiveNormalForm v p f

Constructors

CNF [Sentence v p f]

Instances

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

data NormalSentence v p f

Constructors

NFNot (NormalSentence v p f)

NFPredicate p [NormalTerm v f]

NFEqual (NormalTerm v f) (NormalTerm v f)

Instances

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

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

(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

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)

(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

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