首页    期刊浏览 2024年11月30日 星期六
登录注册

文章基本信息

  • 标题:Tableau vs. Sequent Calculi for Minimal Entailment
  • 本地全文:下载
  • 作者:Olaf Beyersdorff ; Leroy Chew
  • 期刊名称:Electronic Colloquium on Computational Complexity
  • 印刷版ISSN:1433-8092
  • 出版年度:2014
  • 卷号:2014
  • 出版社:Universität Trier, Lehrstuhl für Theoretische Computer-Forschung
  • 摘要:

    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.

  • 关键词:circumscription; Minimal entailment; proof systems; sequent calculi; simulations; tableau
国家哲学社会科学文献中心版权所有