Deep inference and symmetry in classical proofs

Front Cover
Logos Verlag, 2003 - Computers - 93 pages
In this thesis we see deductive systems for classical propositionaland predicate logic which use deep inference, i.e. inferencerules apply arbitrarily deep inside formulas, and a certainsymmetry, which provides an involution on derivations. Likesequent systems, they have a cut rule which is admissible. Unlikesequent systems, they enjoy various new interesting properties. Notonly the identity axiom, but also cut, weakening and even contractionare reducible to atomic form. This leads to inference rules that arelocal, meaning that the effort of applying them is bounded, andfinitely generating, meaning that, given a conclusion, there is only afinite number of premises to choose from. The systems also enjoy newnormal forms for derivations and, in the propositional case, a cutelimination procedure that is drastically simpler than the ones forsequent systems.

From inside the book

What people are saying - Write a review

We haven't found any reviews in the usual places.


Finite Choice
Cut Elimination
Normal Forms

2 other sections not shown

Common terms and phrases

Bibliographic information