Logiweb(TM)

8.7.4 Sequent operator definitions

Prev Up Next Page 358 of 800 Search internet

The sequent operators are defined thus:

array ( left,left,left,left ) x Init & %% = %% & << {{ x }} ,, {{}} ,, x >> \\ << P ,, C ,, p infer t >> Ponens & %% = %% & << P setunion {{ p }} ,, C ,, t >> \\ << P ,, C ,, c endorse t >> Probans & %% = %% & << P ,, C setunion {{ c }} ,, t >> \\ << P ,, C ,, All x : t,( x ) >> at y & %% = %% & << P ,, C ,, t,( y ) >> \\ << P ,, C ,, c endorse t >> Verify & %% = %% & << P ,, C ,, t >> & ( 1 ) \\ p infer << P ,, C ,, t >> & %% = %% & << P setminus {{ p }} ,, C ,, p infer t >> \\ c endorse << P ,, C ,, R >> & %% = %% & << P ,, C setminus {{ c }} ,, c endorse t >> \\ All x : << P ,, C ,, t >> & %% = %% & << P ,, C ,, All x : t >> & ( 2 ) \\ << P ,, C ,, ( x oplus y ) infer z >> Curry & %% = %% & << P ,, C ,, x infer y infer z >> \\ << P ,, C ,, x infer y infer z >> Uncurry & %% = %% & << P ,, C ,, ( x oplus y ) infer z >> \\ << P ,, C ,, n >> Deref & %% = %% & << P ,, C ,, t >> & ( 3 ) \\ << P ,, C ,, t >> id est n & %% = %% & << P ,, C ,, n >> & ( 3 ) \\ << P ,, C ,, R >> ;; << P prime ,, C prime ,, t prime >> & %% = %% & << P setunion ( P prime setminus {{ t }} ) ,, C setunion C prime ,, t prime >> end array

Notes:

(1) If c evaluates to true.

(2) If x avoids all terms in P and C, i.e. if the meta-variable x does not occur free in any of the premisses in P and side conditions in C.

(3) If the statement aspect of n equals t.

Prev Up Next Page 358 of 800 Search logiweb.eu

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