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

2000 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 11780236
Research InstitutionNational Institute of Informatics

Principal Investigator

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

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に発展させた。

  • Research Products

    (3 results)

All Other

All Publications (3 results)

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

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

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

URL: 

Published: 2002-04-03   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi