Contents of Report

[Data of Report]

Report Number:: TR0606
Date of Registration:: 1990.12
English Title:: A Model Generation Theorem Prover in KL1 Using a Ramified-Stack Algorithm
Japanese Title:: ***
English Author:: H.Fujita,R.Hasegawa
Japanese:: 藤田　博,長谷川　隆三
Name of Organization to which author belongs:: ICOT,ICOT
PDF:: tr0606.pdf

	Abstract	.... 2
1	Introduction	.... 2
2	Meta-Programming in KL1	.... 3
3	Model generation	.... 4
4	MGTP for ground model	.... 6
4.1	Transforming problem clauses to KL1 clauses	.... 6
4.2	A simple MGTP interpreter	.... 8
5	Avoiding redundancy in conjuctive matching	.... 9
5.1	Redundancy in the basic algorithm	.... 9
5.2	Ramified-stack algorithm	.... 10
6	Perfamance evaluation	.... 12
6.1	Performance of MGTP proves on PSI-II	.... 12
6.2	Performance of MGTP-R on Multi-PSI	.... 13
7	Discussion	.... 15
7.1	Indexing	.... 15
7.2	Pruning search space	.... 16
7.3	Partial evaluation	.... 16
7.4	AND parallelism	.... 17
8	Conclusion	.... 17
	Acknowledgements	.... 17
	References	.... 18
	End	.... 20

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