Contents of Report

[Data of Report]

Report Number:: TR0328
Date of Registration:: 1987.11
English Title:: Proof Compiling Technique based on Realizability and Proof Normalization
Japanese Title:: ***
English Author:: Y.Takayama
Japanese:: ***
Name of Organization to which author belongs:: ICOT
PDF:: tr0328.pdf

	Abstract	.... 2
1	Introduction	.... 3
2	Proof Compiler	.... 3
2.1	Notational Preliminaries	.... 3
2.2	Inference Rules on Logical Constants and Equalities	.... 7
2.3	Program Extraction Algorithm	.... 8
3	Proof Schema Using Propositional Variables	.... 10
3.1	Proof of Course of Value Induction	.... 10
3.2	Proof Compilation Algorithm for 2nd Ord.all-I/E Rules	.... 11
3.3	Proof Compilation of Course of Value Schema	.... 12
4	Simple Example;GCD Program	.... 13
4.1	GCD Proof	.... 13
4.2	Proof Compilation of GCD proof	.... 14
5	Execution of the Extracted Codes	.... 14
5.1	Tiny Quty Interpreter	.... 14
5.2	Evaluation of the GCD Code	.... 16
6	Optimization Technique	.... 16
6.1	Proof Normalization and Partial Evaluation of Programs	.... 16
6.2	Example of Proof Normalization	.... 18
6.3	Modified V Code	.... 19
7	Incremental Compilation of Proof	.... 20
7.1	Referring Theorems Already Proven	.... 20
7.2	Example of Incremental Compilation	.... 20
8	Conclusion	.... 21
	Acknowledgments	.... 22
	References	.... 22
	End	.... 27

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