論文

査読有り
2001年

The complexity of analytic tableaux

Conference Proceedings of the Annual ACM Symposium on Theory of Computing
  • Noriko Arai
  • ,
  • Toniann Pitassi
  • ,
  • Alasdair Urquhart

開始ページ
356
終了ページ
363
記述言語
英語
掲載種別
研究論文(国際会議プロシーディングス)
DOI
10.1145/380752.380822

The method of analytic tableaux is employed in many introductory texts and has also been used quite extensively as a basis for automated theorem proving. In this paper, we discuss the complexity of the system as a method for refuting contradictory sets of clauses, and resolve several open questions. We discuss the three forms of analytic tableaux: clausal tableaux, generalized clausal tableaux, and binary tableaux. We resolve the relative complexity of these three forms of tableaux proofs and also resolve the relative complexity of analytic tableaux versus resolution. We show that there is a quasi-polynomial simulation of tree resolution by analytic tableaux; this simulation cannot be improved, since we give a matching lower bound that is tight to within a polynomial.

リンク情報
DOI
https://doi.org/10.1145/380752.380822
共同研究・競争的資金等の研究課題
命題論理の証明の複雑さに関する研究
Scopus
https://www.scopus.com/inward/record.uri?partnerID=HzOxMe3b&scp=0034819571&origin=inward
Scopus Citedby
https://www.scopus.com/inward/citedby.uri?partnerID=HzOxMe3b&scp=0034819571&origin=inward
ID情報
  • DOI : 10.1145/380752.380822
  • ISSN : 0734-9025
  • SCOPUS ID : 0034819571

エクスポート
BibTeX RIS