module Standard: Constructor
Logical constructors with no syntactic simplifications.
val negation : Term.term -> Term.term
Negation of a term.
val conjunction : Term.term -> Term.term -> Term.term
Conjunction of two terms.
val disjunction : Term.term -> Term.term -> Term.term
Disjunction of two terms.
val equivalence : Term.term -> Term.term -> Term.term
Logical equivalence of two (Boolean) terms.
val difference : Term.term -> Term.term -> Term.term
Logical dis-equivalence of two (Boolean) terms.
val implication : Term.term -> Term.term -> Term.term
Implication of two terms.
val conditional : Term.term -> Term.term -> Term.term -> Term.term
Conditional expression: Boolean condition, and Boolean alternatives.
val equality : Term.term -> Term.term -> Term.term
Equality of two non-Boolean terms.
val ite : Term.term -> Term.term -> Term.term -> Term.term
Conditional expression: Boolean condition, non-Boolean alternatives.
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.