論文

査読有り
2000年7月

Relative efficiency of propositional proof systems: resolution vs. cut-free LK

ANNALS OF PURE AND APPLIED LOGIC
  • NH Arai

104
1-3
開始ページ
3
終了ページ
16
記述言語
英語
掲載種別
研究論文(学術雑誌)
出版者・発行元
ELSEVIER SCIENCE BV

Resolution and cut-free LK are the most popular propositional systems used for logical automated reasoning. The question whether or not resolution and cut-free LK have the same efficiency on the system of CNF formulas has been asked and studied since 1960 (Reckhow, Ph.D. Thesis, University of Toronto, 1976; A. Urquhart, the complexity of propositional proofs, Bull. of Symbolic Logic 1 (1995) 425-467). It was shown in Cook and Reckhow, J. Symbolic Logic 44 (1979) 36-50 that tree resolution has super-polynomial speed-up over (tree) cut-free LK. Naturally, the current issue is whether or not resolution and cut-free LK expressed as directed acyclic graphs (DAG) have the same efficiency. In this paper, we introduce a new algorithm to eliminate atomic cuts and show that cut-free LK (DAG) polynomially simulates resolution when the input formula is expressed as a k-CNF formula. As a corollary, we show that regular resolution does not polynomially simulate cut-free LK (DAG). We also show that cut-free LK (DAG) polynomially simulates regular resolution. (C) 2000 Elsevier Science B.V. All rights reserved. MSC: 03F05; 03F20.


リンク情報
Web of Science
https://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcAuth=JSTA_CEL&SrcApp=J_Gate_JST&DestLinkType=FullRecord&KeyUT=WOS:000088044300002&DestApp=WOS_CPL
共同研究・競争的資金等の研究課題
命題論理の証明の長さに関する研究
URL
http://www.sciencedirect.com/science/article/pii/S0168007200000051
ID情報
  • ISSN : 0168-0072
  • eISSN : 1873-2461
  • Web of Science ID : WOS:000088044300002

エクスポート
BibTeX RIS