Contents of Report

[Data of Report]

Report Number:: TR0746
Date of Registration:: 1992.03
English Title:: A Lazy Model Generation Based Theorem Prover
Japanese Title:: 遅延モデル生成法に基づく定理証明器
English Author:: R.Hasegawa,M.Koshimura,H.Fujita
Japanese:: 長谷川隆三,腰村三幸,藤田博
Name of Organization to which author belongs:: ICOT,Toshiba,Mitsubishi
PDF:: tr0746.pdf

[Contents]

	概要	.... 2
1	はじめに	.... 2
2	モデル生成法	.... 3
2.1	連言照合における冗長性の回避	.... 4
3	モデル生成法アルゴリズム	.... 5
3.1	基本アルゴリズム	.... 6
3.2	全テストアルゴリズム	.... 7
3.3	遅延アルゴリズム	.... 7
3.4	単位負節に対する最適化	.... 8
4	複雑さの解析	.... 9
4.1	基本アルゴリズム	.... 10
4.2	全テストアルゴリズム	.... 11
4.3	遅延アルゴリズム	.... 12
4.4	単位負節に対する最適化	.... 13
4.5	複雑さの解析結果の要約	.... 14
5	KLIによる遅延連言照合の実装	.... 14
5.1	先行連言照合	.... 15
5.2	遅延連言照合	.... 15
6	実験結果	.... 18
6.1	広い探索空間を持つHorn節で記述された問題	.... 18
6.2	性能の測定	.... 19
7	結論	.... 21
	謝辞	.... 21
	参考文献	.... 21
	End	.... 22

目次をクリックすると、PDFファイルが表示されます。

ICOT研究論文（TR）一覧に戻る / Back to the list of ICOT Technical Reports