Contents of Report

[Data of Report]

Report Number:: TR0094
Date of Registration:: 1984.12
English Title:: Formulation of Induction Formulas in Verification of Prolog Programs
Japanese Title:: ***
English Author:: T.Kanamori,H.Fujita
Japanese:: ***
Name of Organization to which author belongs:: Mitsubishi Electric Corp.,Mitsubishi Electric Corp.
PDF:: tr0094.pdf

	Abstract	.... 2
	Contents	.... 2
1	Introduction	.... 3
2	Preliminaries	.... 3
2.1	Polarity of Subformulas	.... 3
2.2	S-formulas and Goal Formulas	.... 4
2.3	Manipuration of Goal Formulas	.... 4
3	Framework of Verification of Prolog Programs	.... 5
3.1	Programing Language	.... 5
3.2	Specification Language	.... 5
3.3	Framework of Verification	.... 6
4	Generation of Computational Induction Schemes	.... 6
4.1	Computational Induction	.... 6
4.2	Inducible Definite Clause	.... 7
4.3	Generation of Induction Schemes	.... 7
4.4	Generalization	.... 8
4.5	Examples of Induction Schemes	.... 9
5	Merging of Computational Induction Schemes	.... 10
5.1	Mergible Schemes	.... 10
5.2	Tamaki-Sato's Transformation	.... 11
5.3	Derivation of Merged Schemes	.... 12
6	Discussons	.... 14
7	Conclusion	.... 14
	Acknowledgements	.... 15
	References	.... 15
	Appendix	.... 16

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