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

Typeable3 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

Constructors

Function f [CTerm v f]

Variable v

Instances

Typeable2 CTerm

(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

Typeable Connective

data Quantifier

Constructors

ForAll

ExistsCh

Instances

Eq Quantifier

Data Quantifier

Ord Quantifier

Show Quantifier

Typeable 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

Typeable3 NormalSentence

(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

Typeable2 NormalTerm

(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