Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style

Reports tagged with sequent calculi:
TR14-014 | 28th January 2014
Olaf Beyersdorff, Leroy Chew

The Complexity of Theorem Proving in Circumscription and Minimal Entailment

Circumscription is one of the main formalisms for non-monotonic reasoning. It uses reasoning with minimal models, the key idea being that minimal models have as few exceptions as possible. In this contribution we provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate ... more >>>

TR14-032 | 8th March 2014
Olaf Beyersdorff, Leroy Chew

Tableau vs. Sequent Calculi for Minimal Entailment

In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (J. Autom. Reasoning, 1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e., MLK p-simulates OTAB. The simulation is technically very involved ... more >>>

TR20-159 | 9th October 2020
Leroy Chew, Marijn Heule

Relating existing powerful proof systems for QBF

We advance the theory of QBF proof systems by showing the first simulation of the universal checking format QRAT by a theory-friendly system. We show that the sequent system G fully p-simulates QRAT, including the Extended Universal Reduction (EUR) rule which was recently used to show QRAT does not ... more >>>

ISSN 1433-8092 | Imprint