Loading...
Please wait, while we are loading the content...
Similar Documents
On the proof complexity of cut-free bounded deep inference (2011).
| Content Provider | CiteSeerX |
|---|---|
| Author | Das, Anupam |
| Abstract | 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. |
| File Format | |
| Publisher Date | 2011-01-01 |
| Access Restriction | Open |
| Subject Keyword | Proof Complexity Cut-free Bounded Deep Inference Exponential Speed-up Proof Size Deep Inference Short Proof Cut-free Sequent System Unbounded Deep Inference Deep Inference Methodology Propositional Logic Sequent System High Proof Search Non-determinism Cut-free Deep Inference System Proof Search Side Bounded-depth Cut-free System Top-down Symmetry Depth Level |
| Content Type | Text |
