Contents of Report

[Data of Report]

Report Number:: TR0096
Date of Registration:: 1984.12
English Title:: Verification of Prolog Programs Using an Extention of Execution
Japanese Title:: ***
English Author:: T.Kanamori,H.Seki
Japanese:: ***
Name of Organization to which author belongs:: Mitsubishi Electric Corp.,Mitsubishi Electric Corp.
PDF:: tr0096.pdf

	Abstract	.... 2
	Contents	.... 2
1	Introduction	.... 3
2	Preliminaries	.... 3
2.1	Polarity of Subformulas	.... 3
2.2	S-formulars and Goal Formulas	.... 4
2.3	Manipulation of Goal Formulas	.... 4
3	Framework of Verification of Prolog Programs	.... 5
3.1	Programming Language	.... 5
3.2	Specification Language	.... 5
3.3	Formulation of Verification	.... 6
4	An Extention of Execution	.... 6
4.1	Case Spiltting	.... 7
4.2	Definite Clause Inference	.... 8
4.3	"Negation as Failure" Inferece	.... 8
4.4	Simplification	.... 9
4.5	Oracle Decision	.... 10
5	Examples	.... 10
5.1	First Order Inferece by Extended Excution	.... 10
5.2	Inductive Proof with Extended Execution	.... 11
5.3	An Exsample for Comparison	.... 11
6	Discussions	.... 13
7	Conclusion	.... 14
	Acknowledgements	.... 15
	References	.... 15

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