- 著者
-
大芝 猛
- 雑誌
- 情報処理学会研究報告アルゴリズム(AL)
- 巻号頁・発行日
- vol.1991, no.69, pp.1-9, 1991-07-22
1階術語論理の論理式Aが妥当性を肯定的に検証されるとき得られるguide情報を利用するならば,証明図(型)を試行錯誤なくかき上げるアルゴリズムをすでに提示下が、更に人間の理解しやすい証明形式(等)へ変換するアルゴリズムを連結し,自然な証明を一貫した自動証明手続きで得ることへのアプローチを問題とする。このとき完成した前者に続き,後者のLK→NK変換の結果が内容的にも自然なものとするため,まずLKから(+排中律)体系への変換を行うアルゴリズムを提示した。LKの推論の要素はA_1<&・・・&>A_m⟹B_1^<or・・・or>B_nの意味をもつsequent形式で,右辺がn≥2のとき理解しにくい。これを右辺がn≤1のLJ型sequentからなる証明図に一たん分解し,排中律の拡張を用いて再び結合することによりアルゴリズムを実現したが,このとき,人間の証明としても自然な三段論法が導入される。A Convert algorithm LK to (LJ+excluslve middle) and its application to automatic theorem proving are discussed. In LK system, inference rules for sequents of the form A_1,・・・,A_m→B_1,・・・,B_n(n≤2) is different from human reasonig. In fact, it is difficult to translate directly LK-proofs into proors on natural deduction system such as NK. Then we present an algorithm which converts an arbitrary LK-proof to a proof which consists of LJ-sequents whose right side has at most one formula. In application of this algorithm, decreasing process of the number of right side formulas, derives naturally syllogisms whose cut formulas are generalized exclusive middles.