8.7.3 Sequent operators

Prev Up Next Page 357 of 800 Search internet

The thirteen operators of the Logiweb sequent calculus are:

x InitInit
s PonensModus Ponens
s ProbansModus Probans
s at xInstantiation
s VerifyVerification
x infer sInfer
x endorse sEndorse
All x : sQuantification
s CurryCurrying
s UncurryUncurrying
s DerefDereferencing
s id est xReferencing
s ;; s primeCut

Above, s and s prime are sequents and x is a term.

A sequent term is a term built up from the sequent operators above. Where operators have parameters named s or s prime, the associated arguments must be sequent terms. As an example, a sequent term of form s at x 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 bottom. The value is bottom if sequent evaluation of the sequent term loops indefinitely.

The sequent evaluator defined on the check page returns an exception or bottom 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,

<< {{}} ,, {{}} ,, #x infer #y infer #x >>

is valid because it is the sequent value of

#x infer #y infer #x Init

Prev Up Next Page 357 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05