Contents of Report

[Data of Report]

Report Number:: TR0420
Date of Registration:: ***
English Title:: Proof Theoretic Approach to the Extaraction of Redundancy-free Realiser Codes
Japanese Title:: 構成的証明から冗長性の無いプログラムを導出する証明論的手法
English Author:: Y.Takayama
Japanese:: 高山　幸秀
Name of Organization to which author belongs:: ICOT
PDF:: tr0420.pdf

0	Abstract	.... 1
1	Introduction	.... 2
2	Proof theoretic terjminology and notation	.... 2
3	A Program Extractor System QPC	.... 2
3.1	Q-realisability and Ext Procdedure	.... 3
3.2	Realizing variables and length of formulae	.... 3
4	Declaration to specifications	.... 3
5	Marking	.... 4
5.1	Marking of the( -1)application	.... 4
5.2	Marking of the( -1)application	.... 4
5.3	Marking of the( -1)application	.... 5
5.4	Marking of the( -1)rule	.... 5
6	Critical application	.... 6
6.1	Induction hypothesis and Marking	.... 6
6.2	Critical( -1)and( -E)applications	.... 6
6.3	Critical( -E)applications	.... 7
6.4	Critical( -I&E)applications	.... 7
6.5	Soundness of the Marking Procedure	.... 8
7	Program Extraction Algorithm	.... 8
8	Conclusion	.... 10
9	References	.... 10

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