[Prev][Next][Index][Thread]

Paper on a very simple cut elimination

[ TYPES is back!  Several messages follow... -B ]

Hello,

I'd be delighted in receiving comments about a very simple cut 
elimination method, which you can find in the paper below, to be 
presented at next CSL '03. I'm especially interested in comments from 
people in the types community about possible computational 
interpretations.

The paper is contained in my PhD thesis, which might be interesting 
to people wishing to know more about the calculus of structures, in 
the special case of classical logic.

Best,

-Kai


Atomic Cut Elimination for Classical Logic
short paper

System SKS is a set of rules for classical propositional logic 
presented in the calculus of structures. Like sequent systems and 
unlike natural deduction systems, it has an explicit cut rule, which 
is admissible. In contrast to sequent systems, the cut rule can 
easily be restricted to atoms. This allows for a very simple cut 
elimination procedure based on plugging in parts of a proof, like 
normalisation in natural deduction and unlike cut elimination in the 
sequent calculus. It should thus be a good common starting point for 
investigations into both proof search as computation and proof 
normalisation as computation.

<http://www.wv.inf.tu-dresden.de/~kai/AtomicCutElimination-short.pdf>


Deep Inference and Symmetry in Classical Proofs
PhD thesis

In this thesis we see deductive systems for classical propositional 
and predicate logic which use deep inference, i.e. inference rules 
apply arbitrarily deep inside formulas, and a certain symmetry, which 
provides an involution on derivations. Like sequent systems, they 
have a cut rule which is admissible. Unlike sequent systems, they 
enjoy various new interesting properties. Not only the identity 
axiom, but also cut, weakening and even contraction are reducible to 
atomic form. This leads to inference rules that are local, meaning 
that the effort of applying them is bounded, and finitary, meaning 
that, given a conclusion, there is only a finite number of premises 
to choose from. The systems also enjoy new normal forms for 
derivations and, in the propositional case, a cut elimination 
procedure that is drastically simpler than the ones for sequent 
systems.

<http://www.wv.inf.tu-dresden.de/~kai/phd.pdf>


Web page on the calculus of structures:
<http://www.ki.inf.tu-dresden.de/~guglielm/Research/>