(Semantic) Characterization of CutElimination
General Information
Abstract
People
Publications
Related Projects
General Information
The project, funded by the Austrian Science Fund
( FWF ), has started in March 2006 and lasted until November 2009.
Project leader: Dr. Agata Ciabattoni.
Project Abstract
Cutelimination is one of the most important techniques in proof theory.
Roughly speaking, eliminating cuts from a proof generates a new proof without
lemmas, which essentially consists of the syntactic material of the proven theorem.
Since its introduction in 1934, sequent calculus has been one
of the preferred deductive frameworks to formalize and reason about logics.
However, this framework is not capable of handling all interesting and
useful logics. To this end, a large range of variants and extensions of
Gentzen sequent calculi have been introduced in the last few decades.
Among them, hypersequent calculi have been
shown shown to be a rather elegant and simple framework
for ``logic engineering'' that applies to a wide range of nonclassical logics
arising in several areas of mathematics, philosophy and computer science
The aim of the proposed project is a semantic characterization of
cutelimination in sequent and hypersequent calculi,
i.e. the definition of syntactic and semantic criteria that, when
satisfied by such calculi guarantee a certain kind of
cutelimination and, when not satisfied, provides counterexamples.
The central idea is to answer the following questions:
Which are the natural properties that rules have to satisfy in order to
preserve cutelimination?
Is there a uniform method to prove (or disprove) cutelimination
for a wide class of sequent or hypersequent calculi?
The main advantages of such a method would be:
 it becomes easier to prove cutelimination theorems for novel
(sequent type) logic calculi and to find analytic calculi for new logics
 the construction of the cutelimination methods and the checking
of the formal criteria can be automatized  provided the method is
effective.
People
The following researchers were employed in the project:
 Dr. Agata Ciabattoni (head of the Project, March 2006July 2009 with
interruption for maternity leave July 2007October 2007)

Dr. Rosalie Iemhoff (March and April 2006)

Dr George Metcalfe (JuneAugust 2006, JuneJuli 2007, Juli 2008)
 Dr. Clemens Richter (JanuaryApril 2007)
Project Publications
Journals

Algebraic proof theory for substructural logics:
cutelimination and completions.
Annals of Pure and Applied Logic .
Accepted for Publication.
Abstract
( A. Ciabattoni , N. Galatos and K. Terui )

Algebraic and prooftheoretic characterizations of truth stressers
for MTL and its extensions.
Fuzzy Sets and Systems. Accepted for publication 2009.
( A. Ciabattoni , G. Metcalfe and
F. Montagna )

Towards an Algorithmic Construction of CutElimination
Procedures. Mathematical Structures in Computer Science.
2008.
(A. Ciabattoni and A. Leitsch ).

Density Elimination . Theoretical Computer Science. 2008.
( A. Ciabattoni and G. Metcalfe )

Towards
a semantic characterization of cutelimination. Studia logica .
Vol. 82(1). pp. 95  119. 2006.
( A. Ciabattoni and K. Terui ).

Proof Theory for Admissible Rules .
Annals of Pure and Applied Logic .
2009
( R. Iemhoff and G. Metcalfe )
(Peerreviewed) Conferences

Expanding the realm of systematic proof theory.
Proceedings of CSL 2009. LNCS. pp. 163178.
( A. Ciabattoni ,
L. Strassburger and K. Terui )

From axioms to analytic rules in nonclassical logics.
IEEE Symposium on Logic in Computer Science
(LICS'08) .
( A. Ciabattoni , N. Galatos and K. Terui )

Canonical Calculi: Invertibility, AxiomExpansion and (Non)determinism.
Forthcoming in the Proceedings of the 4th Computer Science Symposium in Russia
(CSR2009) Novosibirsk, Russia, 2009.
( A. Avron ,
A. Ciabattoni and A. Zamansky )

Cut elimination for first order Goedel logic
by hyperclause resolution. Proceedings of Logic for Programming and Automated
Reasoning
(LPAR'2008), November 2008
( M. Baaz , A. Ciabattoni
and C.G. Fermüller )

Density Elimination and Rational Completeness for FirstOrder Logics.
Proceedings of the Symposium on Logical Foundations of Computer Science
(LFCS'07) .
New York, June 2007.
( A. Ciabattoni and G. Metcalfe )

Modular CutElimination: Finding Proofs or Counterexamples.
Proceedings of Logic for Programming and Automated
Reasoning
(LPAR'2006),
LNAI 4246. pp. 135149. 2006.
( A. Ciabattoni and K. Terui )
Related Projects
 The Realm of Cut Elimination . (20072008).
Bilateral Cooperation Agreement with France (OeADWTZ).
Head (of the Austrian team): A. Ciabattoni.
Head (of the French team):
Dale Miller.