Contents of Report

[Data of Report]

Report Number:: TR0751
Date of Registration:: 1992.03
English Title:: Lazy Model Generation for Improving the Efficiency of Forward Reasoning Theorem Provers
Japanese Title:: ***
English Author:: R.Hasegawa,M.Koshimura,H.Koshimura
Japanese:: ***
Name of Organization to which author belongs:: ICOT,Toshiba,Mitsubishi
PDF:: tr0751.pdf

	Abstract	.... 2
1	Introduction	.... 2
2	Model genrenation Method	.... 3
2.1	Avoiding Redundancy in Conjunctive Matching	.... 4
3	Algorithms for model Generation	.... 6
3.1	Basic Algorithym	.... 6
3.2	Full-Test Algorithym	.... 7
3.3	Lazy Algorithym	.... 8
3.4	Optimization of Unit Tester Clauses	.... 9
4	Complexity Algorithym	.... 10
4.1	Basic Algorithym	.... 11
4.2	Full-Test Algorithym	.... 12
4.3	Lazy Algorithym	.... 13
4.4	Optimization of Unit Tester Clauses	.... 14
4.5	Summary of Complexity Analysis	.... 15
5	Imprementation of Lazy Conjunctive Matching in KL1	.... 16
5.1	Outline of KL1	.... 16
5.2	Eager Conjunctive Matching	.... 17
5.3	Lazy Conjunctive Matching	.... 18
6	Results	.... 20
6.1	Features of Hard Horn problems	.... 20
6.2	Performance	.... 20
	Acknowledgements	.... 23
	References	.... 23

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