Contents of Report

[Data of Report]

Report Number:: TR0395
Date of Registration:: 1988.06
English Title:: Proof Theoretic Approach to the Extraction of Redundancy-free Realizer Codes
Japanese Title:: ***
English Author:: Y.Takayama
Japanese:: 高山　幸秀
Name of Organization to which author belongs:: ICOT
PDF:: tr0395.pdf

	Abstract	.... 2
1	Introduction	.... 2
2	Symple Constructive Logic	.... 4
2.1	Expressions and Inference Rules	.... 4
2.2	Proof Theoretic Terminology Natation	.... 6
2.3	Realizing Variables Sequence and Length of Formulae	.... 7
2.4	Prrof Compilation(Ext Procedure)	.... 8
3	Declaration and Marking of Proof Trees	.... 11
3.1	Declaration to Specifications	.... 11
3.2	Marking	.... 12
4	Critical Applications	.... 18
4.1	Induction Hypothesis and Marking	.... 19
4.2	Critical Segments	.... 19
4.3	Critical( -E)Applications	.... 22
4.4	Critical( -I&E)Applications	.... 22
4.5	Main Theorem	.... 23
5	Proof of the Main Theorem	.... 24
5.1	Form of Normal Proof Trees	.... 24
5.2	Proof of Theorem2	.... 24
6	Modefied Proof Compilation Algorithm	.... 27
7	Example	.... 30
7.1	Extraction of Program by Ext	.... 30
7.2	Declaration	.... 31
8	Conclusion	.... 36
	References	.... 36
	Appendix	.... 38
	End	.... 41

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