Contents of Report

[Data of Report]

Report Number:: TR0726
Date of Registration:: 1992.01
English Title:: Lazy Model Generation for Implementing Efficient Theorem Proves
Japanese Title:: ***
English Author:: R.Hasegawa,M.Koshimura,H.Fujita
Japanese:: ***
Name of Organization to which author belongs:: ICOT,Toshiba<Mitsubishi
PDF:: tr0726.pdf

	Abstract	.... 2
1	Introduction	.... 2
2	Model Generation Method	.... 3
2.1	Avoiding redundancy in conjunctive matching	.... 4
3	Algorithm for Model Generation	.... 5
3.1	Naive algorithm	.... 6
3.2	Basic algorithm	.... 6
3.3	Lazy algorithm	.... 7
3.4	Optimization	.... 8
4	Complexity Analysis	.... 10
4.1	Naive algorithm	.... 11
4.2	Basic algorithm	.... 12
4.3	Lazy algorithm	.... 12
4.4	Optimization	.... 13
5	Imprementation of Lazy Conjunctive Matching in KL1	.... 14
5.1	Eager Conjunctive Matching	.... 14
5.2	Lazy Conjunctive Matching	.... 16
6	Experimental Results	.... 18
6.1	Features of hard problems	.... 18
6.2	Perfomance measurement	.... 18
7	Conclusion	.... 19
	Reference	.... 20

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