Contents of Report

[Data of Report]

Report Number:: TR0175
Date of Registration:: 1986.05
English Title:: Soundness and Completeness of Extended Execution for Proving Properties of Prolog Programs
Japanese Title:: ***
English Author:: T.Kanamori
Japanese:: ***
Name of Organization to which author belongs:: Mitsubishi
PDF:: tr0175.pdf

	Abstract	.... 2
1	Introduction	.... 3
2	Preliminaries	.... 3
2.1	Polarity if Subformulas	.... 3
2.2	S-Formulas and Goal Formulas	.... 4
2.3	Manipulation of Goal Formulas	.... 5
3	An Extention of Execution	.... 6
3.1	Case Spiltting	.... 7
3.2	Definite Clause Inference	.... 8
3.3	"Negation as Failure" Inference	.... 8
3.4	Simplification	.... 9
4	Soundness of Extended Execution	.... 10
4.1	Completion of Prolog Programs	.... 10
4.2	Normal Forms of Goal Formulas	.... 11
4.3	Proof of the Soundness	.... 15
5	Completenss of Extended Execution	.... 16
5.1	Normal Extended Execution	.... 17
5.2	"Negation as Failure" Tree	.... 19
5.3	Fair "Negation as Failure" Derivation	.... 21
5.4	Models Associated with "Negation as Failure" Derivations	.... 22
5.5	Proof of the Completeness	.... 23
6	Discussion	.... 26
7	Conclusion	.... 27
	Acknowledgements	.... 28
	References	.... 28
	End	.... 29

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