|Page 357 of 800||Search internet|
The thirteen operators of the Logiweb sequent calculus are:
Above, and are sequents and is a term.
A sequent term is a term built up from the sequent operators above. Where operators have parameters named or , the associated arguments must be sequent terms. As an example, a sequent term of form must have a sequent term as first argument but can have an arbitrary term as second argument.
The sequent value of a sequent term can be a sequent or an exception or . The value is if sequent evaluation of the sequent term loops indefinitely.
The sequent evaluator defined on the check page returns an exception or when applied to a non-sequent term. In other words, the sequent evaluator checks, among other, that the sequent term is wellformed.
A sequent is valid if it is the sequent value of some sequent term. As an example,
is valid because it is the sequent value of
|Page 357 of 800||Search logiweb.eu|