On the proof complexity of cut-free bounded deep inference


Das, A., 2011. On the proof complexity of cut-free bounded deep inference. In: Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings. Vol. 6793 LNAI. Heidelberg: Springer-Verlag, pp. 134-148. (Lecture Notes in Computer Science)

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Official URL:


It has recently been shown that cut-free deep inference systems exhibit an exponential speed-up over cut-free sequent systems, in terms of proof size. While this is good for proof complexity, there remains the problem of typically high proof search non-determinism induced by the deep inference methodology: the higher the depth of inference, the higher the non-determinism. In this work we improve on the proof search side by demonstrating that, for propositional logic, the same exponential speed-up in proof size can be obtained in bounded-depth cut-free systems. These systems retain the top-down symmetry of deep inference, but can otherwise be designed at the same depth level of sequent systems. As a result the non-determinism arising from the choice of rules at each stage of a proof is smaller than that of unbounded deep inference, while still giving access to the short proofs of deep inference.


Item Type Book Sections
CreatorsDas, A.
DepartmentsFaculty of Science > Computer Science
ID Code24952


Actions (login required)

View Item