Projects per year
Abstract
Jeřábek showed in 2008 that cuts in propositionallogic deepinference proofs can be eliminated in quasipolynomial time. The proof is an indirect one relying on a result of Atserias, Galesi and Pudlák about monotone sequent calculus and a correspondence between this system and cutfree deepinference proofs. In this paper we give a direct proof of Jeřábek’s result: we give a quasipolynomialtime cutelimination procedure in propositionallogic deep inference. The main new ingredient is the use of a computational trace of deepinference proofs called atomic flows, which are both very simple (they trace only structural rules and forget logical rules) and strong enough to faithfully represent the cutelimination.
Original language  English 

Title of host publication  Logic for programming, artificial intelligence, and reasoning: 16th International Conference, LPAR16, Dakar, Senegal, April 25–May 1, 2010, revised selected papers 
Editors  E M Clarke, A Voronkov 
Place of Publication  Berlin 
Publisher  Springer 
Pages  136153 
Number of pages  18 
ISBN (Electronic)  9783642175114 
ISBN (Print)  9783642175107 
DOIs  
Publication status  Published  2010 
Publication series
Name  Lecture Notes in Computer Science 

Volume  6355 
ISSN (Print)  03029743 
Projects
 1 Finished

COMPLEXITY AND NONDETERMINISM IN DEEP INFERENCE
Guglielmi, A. & Bruscoli, P.
Engineering and Physical Sciences Research Council
1/02/07 → 30/06/08
Project: Research council