Go backward to 2.1 Commands Go up to 2 Language Go forward to 2.3 Terms

2.2 Formulas

A Formula is one of the following phrases denoting a Boolean value (true or false):

Name [ ( Terms ) ]

An atomic formula: the value of the formula is the value of the denoted predicate where the parameters are bound to the values of the corresponding argument terms.

pred p(x) <=> <=(x, 5);
> predicate p/1.
formula p(4);
> true.

if ( Formula , Formula [ , Formula ] )

A conditional formula: if the first formula (the guard) evaluates to true, the result is the value of the second formula, otherwise it is the result of the third formula. If the guard evaluates to false and the third formula is not given, the result is undefined (evaluation aborts, if guard checking is switched on).

formula if(not(true), false, or(true, false));
> true;
formula if(not(true), false);
> ERROR: guard condition is false.

let ( BoundVariables : Formula )

A formula with some locally bound variables; the value of the formula is the value of the base formula for the denoted variable bindings.

formula let(x = 1, y = 2: <=(x, y));
> true;

not ( Formula )

The negation of a formula: the negation is true if and only if the base formula is false.

formula not(true);
> false.

and ( { Formulas } )

The conjunction of a sequence of formulas; the conjunction is true if and only if every formula in the sequence is true.

formula and(true, not(true), true);
> false.

or ( { Formulas } )

The disjunction of a sequence of formulas; the disjunction is true if and only if some formula in the sequence is true.

formula or(false, and(false, true), not(false));
> true.

implies ( Formula , Formula )

The implication of two formulas: the implication is false if and only if the first formula is true and the second one is false.

formula implies(not(false), false);
> false.

equiv ( Formula , Formula )

The equivalence of two formulas: the equivalence is true if and only if both formulas are true or both are false.

formula equiv(true, or(false, true));
> true;

forall ( IteratorVariables : Formula )

A formula that is universally quantified over a sequence of variables: the universal quantification is true if the base formula is true for every binding of the variables denoted by the iterators.

formula forall(x in nat(1,10), y in nat(1, x): <=(y, x));
> true;

exists ( IteratorVariables : Formula )

A formula that is existentially quantified over a sequence of typed variables; the existential quantification is true if the base formula is true for some binding of the variables denoted by the iterators.

formula exists(x in nat(1, 10), y in nat(x, 10): 
  =(y, *(2, x)));
> true;