Contents of Report

[Data of Report]

	Abstract	.... 2
1	Introduction	.... 2
2	Mathematical Programming	.... 3
2.1	Programming asa Mathematical Documentation	.... 3
2.2	Documentation Language;PDL-QJ	.... 7
2.3	Proof Checker with Proof Finding Facility	.... 10
2.4	Expressive Power of Constructive Logic and Automatic Coding	.... 10
3	Formal Stracture of the System	.... 11
3.1	Outline of QJ and Quty	.... 12
3.2	QPC Logic	.... 15
3.3	Proof Compilation	.... 19
4	Opitimization Technique	.... 24
4.1	Redundancy in Realiser Codes	.... 25
4.2	Proof Normalization	.... 26
4.3	Modified V-code	.... 27
4.4	Extended Projection Method	.... 28
5	Conclusion	.... 41
	Acknowledgement	.... 42
	References	.... 42
	Appendix	.... 45
	End	.... 46

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