Contents of Report

[Data of Report]

	Abstract	.... 2
1	Background	.... 2
1.1	Programming Environment	.... 2
1.2	Correctness of Programs	.... 3
1.3	Programming and Theorem Proving	.... 4
2	Proof Checker	.... 6
2.1	An overview	.... 6
2.2	The CAP project and the CAP-LA system	.... 7
2.3	PDL	.... 8
2.4	Proof checking subsystem	.... 10
2.5	Further plans for CAP projects	.... 10
3	Term Rewriting System Generator(Metis)	.... 12
3.1	Preliminaries	.... 12
3.2	Well-founded ordering of terms	.... 14
3.3	Associative and commutative operators	.... 16
3.4	Orientation-free rules and S-strategy	.... 17
	References	.... 20
	End	.... 57

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