Page 357 of 800
| Page 357 of 800 | Search internet |
The thirteen operators of the Logiweb sequent calculus are:
 | Init |
 | Modus Ponens |
 | Modus Probans |
 | Instantiation |
 | Verification |
 | Infer |
 | Endorse |
 | Quantification |
 | Currying |
 | Uncurrying |
 | Dereferencing |
 | Referencing |
 | Cut |
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 |