Calculemus

formula<'a> Type

Namespace: Calculemus
Assembly: Calculemus.dll
Parent Module: Formulas
Base Type: obj
All Interfaces: IStructuralEquatable , IComparable<formula<'a>> , IComparable , IStructuralComparable

Abstract syntax tree of polymorphic type of formulas.

Union cases

Union case Description

And(formula<'a>, formula<'a>)

Full Usage: And(formula<'a>, formula<'a>)

Parameters:
    Item1 : formula<'a> - The first conjunct.
    Item2 : formula<'a> - The second conjunct.

Conjunction.

Item1 : formula<'a>

The first conjunct.

Item2 : formula<'a>

The second conjunct.

Atom 'a

Full Usage: Atom 'a

Parameters:
    Item : 'a - The type of the formula: see prop and fol.

Atomic formula.

Item : 'a

The type of the formula: see prop and fol.

Exists(string, formula<'a>)

Full Usage: Exists(string, formula<'a>)

Parameters:
    Item1 : string - The name of the existentially quantified variable.
    Item2 : formula<'a> - The scope of the existential quantification.

Existentially quantified formula.

Item1 : string

The name of the existentially quantified variable.

Item2 : formula<'a>

The scope of the existential quantification.

False

Full Usage: False

Constant formula False.

Forall(string, formula<'a>)

Full Usage: Forall(string, formula<'a>)

Parameters:
    Item1 : string - The name of the universally quantified variable.
    Item2 : formula<'a> - The scope of the universal quantification.

Universally quantified formula.

Item1 : string

The name of the universally quantified variable.

Item2 : formula<'a>

The scope of the universal quantification.

Iff(formula<'a>, formula<'a>)

Full Usage: Iff(formula<'a>, formula<'a>)

Parameters:
    Item1 : formula<'a> - The first member of the equivalence.
    Item2 : formula<'a> - The second member of the equivalence.

Logical Equivalence.

Item1 : formula<'a>

The first member of the equivalence.

Item2 : formula<'a>

The second member of the equivalence.

Imp(formula<'a>, formula<'a>)

Full Usage: Imp(formula<'a>, formula<'a>)

Parameters:
    Item1 : formula<'a> - The antecedent of the implication.
    Item2 : formula<'a> - The conclusion of the implication.

Implication.

Item1 : formula<'a>

The antecedent of the implication.

Item2 : formula<'a>

The conclusion of the implication.

Not formula<'a>

Full Usage: Not formula<'a>

Parameters:
    Item : formula<'a> - The formula being negated.

Negation.

Item : formula<'a>

The formula being negated.

Or(formula<'a>, formula<'a>)

Full Usage: Or(formula<'a>, formula<'a>)

Parameters:
    Item1 : formula<'a> - The first disjunct.
    Item2 : formula<'a> - The second disjunct.

Disjunction.

Item1 : formula<'a>

The first disjunct.

Item2 : formula<'a>

The second disjunct.

True

Full Usage: True

Constant formula True.