Logiweb(TM)

8.7.2 Sequents

Prev Up Next Page 356 of 800 Search internet


A Logiweb sequent is a triple << P ,, C ,, R >> where P is a finite set of premisses, C is a finite set of side conditions, and R is a result which holds if the given premisses and side conditions hold. R is a term and P and C are finite sets of terms. Finite sets of terms are represented as lists without repetitions. Finite sets of terms can contain zero, one, or more terms.

A sequent << P ,, C ,, R >> represents the statement that if all terms in the set P are provable and all side conditions in C evaluate to true then R is provable. In other words, the sequent

<< {{ P _ { 1 } ,, ... ,, P _ { m } }} ,, {{ C _ { 1 } ,, ... ,, C _ { n } }} ,, R >>

represents that the statement

P _ { 1 } infer *** infer P _ { m } infer C _ { 1 } endorse *** endorse C _ { n } endorse R

In particular, the sequent << {{}} ,, {{}} ,, R >> represents the statement that R is provable.

Prev Up Next Page 356 of 800 Search logiweb.eu

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