Contents of Report

[Data of Report]

Report Number:: TR0588
Date of Registration:: 1990.08
English Title:: A Prallel Theorem Prover in KL1 and Its Appication to Program Synthesis
Japanese Title:: ***
English Author:: R.Hasegawa,H.Fujita,M.Fujita
Japanese:: ***
Name of Organization to which author belongs:: ICOT,Mitsubishi,ICOT
PDF:: tr0588.pdf

	Abstract	.... 2
1	Introduction	.... 2
2	Model Generation	.... 4
3	KL1 Based Model Generation Theorem Prover	.... 5
3.1	Variables and Unification	.... 5
3.2	Ground Model	.... 5
3.3	The Interpreter	.... 6
3.4	Performance Comparison for Ground Model	.... 7
4	Extension of MGTP	.... 7
4.1	Nonground Model	.... 7
4.2	Variables and Unification Revisited	.... 9
4.3	Avoiding Redundancy	.... 10
4.4	Heuristics	.... 10
4.5	Performance Comparison for Nonground Model	.... 12
5	Program Synthesis by Parallel Prover	.... 12
5.1	Framework of Program Synthesis	.... 12
5.2	The problem and the Solutions	.... 13
5.3	Sort problem	.... 14
5.4	Program Extraction	.... 16
6	Conclusion	.... 19
	Acknowledgement	.... 20
	References	.... 20

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