Contents of Report

[Data of Report]

Report Number:: TR0522
Date of Registration:: 1989.11
English Title:: Extaraction of Redundacy-Free Programs from Constructive Natural Deduction Proofs
Japanese Title:: ***
English Author:: Y.Takayama
Japanese:: 高山　幸秀
Name of Organization to which author belongs:: ICOT
PDF:: tr0522.pdf

0	Abstract	.... 2
1	Introduction	.... 2
2	Simple Constructive Logic	.... 5
2.1	Expressions and Inference Rules	.... 5
2.2	Proof Theoretic Terminology and Notation	.... 7
2.3	Realizing Variable Sequence and Length of Formulas	.... 8
2.4	Proof Compilation(Ext Procedure)	.... 9
3	Declaration and Marking of Proof Trees	.... 12
3.1	Declaration to Specifications	.... 13
3.2	Marking	.... 14
4	Marking Procedure on Induction Proofs	.... 19
4.1	Marking Condition	.... 19
4.2	Marking with Backtracking	.... 20
4.3	Proof Theoretic Characterization of critical applications	.... 21
5	Modified Proof Compilation Algorithm	.... 26
6	Some Properities of Mark and NExt	.... 29
6.1	Normalization of Marked Proof trees	.... 29
6.2	Next Procedure and projection	.... 31
7	Example	.... 36
7.1	Extaraction of a Prime Number Checker program by Ext	.... 36
7.2	Program Extraction by Declaration,Marking and NExt	.... 37
7.3	Proof Tree Analysis	.... 38
8	Conclusion	.... 40
	References	.... 41
	End	.... 48

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