### Abstract

Original language | English |
---|---|

Title of host publication | Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings |

Place of Publication | Heidelberg |

Publisher | Springer |

Pages | 134-148 |

Number of pages | 15 |

Volume | 6793 LNAI |

ISBN (Print) | 03029743 |

DOIs | |

Publication status | Published - 2011 |

Event | 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, July 4, 2011 - July 8, 2011 - Bern, Switzerland Duration: 1 Jan 2011 → … |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Verlag |

### Conference

Conference | 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, July 4, 2011 - July 8, 2011 |
---|---|

Country | Switzerland |

City | Bern |

Period | 1/01/11 → … |

### Cite this

*Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings*(Vol. 6793 LNAI, pp. 134-148). (Lecture Notes in Computer Science). Heidelberg: Springer. https://doi.org/10.1007/978-3-642-22119-4_12

**On the proof complexity of cut-free bounded deep inference.** / Das, Anupam.

Research output: Chapter in Book/Report/Conference proceeding › Chapter

*Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings.*vol. 6793 LNAI, Lecture Notes in Computer Science, Springer, Heidelberg, pp. 134-148, 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2011, July 4, 2011 - July 8, 2011, Bern, Switzerland, 1/01/11. https://doi.org/10.1007/978-3-642-22119-4_12

}

TY - CHAP

T1 - On the proof complexity of cut-free bounded deep inference

AU - Das, Anupam

PY - 2011

Y1 - 2011

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1007/978-3-642-22119-4_12

U2 - 10.1007/978-3-642-22119-4_12

DO - 10.1007/978-3-642-22119-4_12

M3 - Chapter

SN - 03029743

VL - 6793 LNAI

T3 - Lecture Notes in Computer Science

SP - 134

EP - 148

BT - Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Proceedings

PB - Springer

CY - Heidelberg

ER -