权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

命题逻辑证明长度的研究

基本信息

批准号：
11780236
负责人：
新井紀子
金额：
$ 1.41万
依托单位：
National Institute of Informatics (2000)Hiroshima City University (1999)
依托单位国家：
日本
项目类别：
Grant-in-Aid for Encouragement of Young Scientists (A)
财政年份：
1999
资助国家：
日本
起止时间：
1999 至 2000
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-11780236/
关键词：
自動証明証明の複雑さ証明論計算の複雑さ計算量ロジック

项目摘要

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

Heisei 11 year proposal, simple combinatorial reasoning and similar system, symmetry and resolution, system and excellence Symmetry and resolution are backward search, automatic proof of machine direction and system, simple combinatorial reasoning, linear time, possible solution, exponential time, etc. The superiority of simple combinatorial reasoning is proved. A party, simple combinatorial reasoning C speech The automatic proof machine is used for solving the elementary combination problem in a short time and for solving the large-scale problem automatically.(1) The doomsday problem.(2) The partial set problem.(3) The k-partition problem.(4) The color-separation problem.(5) The automatic proof machine is used for solving the short-time and large-scale problem automatically. As a result, it is confirmed that Godzilla, developed today, can solve problems with various cutting-edge automatic attestors at high speed. On the other hand, the problem is that Godzilla's calculation time is not enough. For example, if a propositional logic expression is used, the propositional logic expression is used to calculate the time index. This is the first time I've ever seen a Godzilla.