• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

命題論理の証明の長さに関する研究

Research Project

Project/Area Number 11780236
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionNational Institute of Informatics (2000)
Hiroshima City University (1999)

Principal Investigator

新井 紀子  国立情報学研究所, 情報学基礎研究系, 助教授 (40264931)

Project Period (FY) 1999 – 2000
Project Status Completed (Fiscal Year 2000)
Budget Amount *help
¥2,200,000 (Direct Cost: ¥2,200,000)
Fiscal Year 2000: ¥1,100,000 (Direct Cost: ¥1,100,000)
Fiscal Year 1999: ¥1,100,000 (Direct Cost: ¥1,100,000)
Keywords自動証明 / 証明の複雑さ / 証明論 / 計算の複雑さ / 計算量 / ロジック
Research Abstract

平成11年度に提案した、simple combinatorial reasoningが類似の体系であるsymmetryつきのresolutionよりも体系として優れていることを証明した。すなわち、symmetryつきのresolutionはbackward searchができないという自動証明機向けの体系としての大きな欠点があるばかりでなく、simple combinatorial reasoningでは線形時間で解決可能であるような問題にたいして、指数時間かかることがあることを示した。このことで、simple combinatorial reasoningの優位性を証明したといえる。
一方、simple combinatorial reasoningをC言語を使って自動証明機Godzillaとして実装した。そして、この自動証明機が初等的組み合わせ問題に対してどれだけ短時間で大規模な問題を自動的に解くことができるのかを(1)鳩ノ巣問題(2)部分集合問題(3)k分割問題(4)クリーク色分け問題などを例にとって、実験を行う。その結果、今回開発されたGodzillaが最先端の各種の自動証明機よりも高速で問題解決することが確認された。
上に挙げられた問題に関してはGodzillaの計算時間は入力の二乗程度のオーダであった。ただし、この結果は入力となる命題論理式を元の述語論理式からシステマティックに変換して得た場合であり、入力をシャッフルすると、計算時間は指数時間かかってしまう。このことを改善するため、さまざまなヒューリスティックスを検討して、好結果が得られるものをさらに選りすぐり、改良型Godzillaに発展させた。

Report

(2 results)
  • 2000 Annual Research Report
  • 1999 Annual Research Report
  • Research Products

    (6 results)

All Other

All Publications (6 results)

  • [Publications] N.H.Arai,A.Urquhart.: "Local symmetries in prepositional logic"Proc.TABLEAUX2000,LNAI. 1947. 40-51 (2000)

    • Related Report
      2000 Annual Research Report
  • [Publications] N.H.Arai,R.Masukawa: "How to find symmetries hidden in combinatorial problems,"Proc.Calculemus2000. (2001)

    • Related Report
      2000 Annual Research Report
  • [Publications] N.H.Arai,T.Pttassi,A.Urquhart: "The complexity of analytic tableaux"Proc.STOC2001. (2001)

    • Related Report
      2000 Annual Research Report
  • [Publications] Noriko Arai,Alasdair Urquhart: "Local symmetries in propositional Logic"Lecture Notes in Artificial Intelligence. (予定).

    • Related Report
      1999 Annual Research Report
  • [Publications] Noriko Arai: "Relative efficiency of propositional proof systems:resolution vs.cut-free LK"Annals of Pure and Applied Logic. (予定).

    • Related Report
      1999 Annual Research Report
  • [Publications] 新井紀子,枡川竜治: "知的自動証明機の提案と実装"京都大学数理学研究所講演録. (予定).

    • Related Report
      1999 Annual Research Report

URL: 

Published: 1999-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi