[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/>