Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR14-032 | 8th March 2014 12:19

Tableau vs. Sequent Calculi for Minimal Entailment

RSS-Feed




TR14-032
Authors: Olaf Beyersdorff, Leroy Chew
Publication: 9th March 2014 16:56
Downloads: 931
Keywords: 


Abstract:

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 and answers an open question posed by Olivetti (1992) on the relation between the two calculi. We also show that the two systems are exponentially separated, i.e., there are formulas which have polynomial-size MLK-proofs, but require exponential-size OTAB-proofs.



ISSN 1433-8092 | Imprint