A CUT-ELIMINATION PROCEDURE DESIGNED FOR EVALUATING PROOFS AS PROGRAMS

被引：0

作者：

SCHMERL, UR ^{[1
]}

机构：

[1] UNIV MUNICH,FAK INFORMAT,W-8014 MUNICH,GERMANY

来源：

LECTURE NOTES IN COMPUTER SCIENCE | 1992年 / 626卷

关键词：

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

This paper describes a method which can be used to determine output values from given input values of programs taking the form of formal proofs. The proofs are constructed in a logic calculus which may include user-defined non-logical inference rules. This calculus is complete in the sense that each computable function can be computed by means of a proof in this calculus. The evaluation method is based mainly on Gentzen's cut-elimination procedure. However the presence of non-logical inference rules requires additional steps to eliminate these rules. Termination of the method is proved by assigning constructive ordinal numbers.

引用

页码：316 / 325

页数：10

共 50 条

[31] Towards a clausal analysis of cut-elimination
Baaz, M
Leitsch, A
JOURNAL OF SYMBOLIC COMPUTATION, 2006, 41 (3-4) : 381 - 410
[32] Reducing redundancy in cut-elimination by resolution
Paleo, Bruno Woltzenlogel
JOURNAL OF LOGIC AND COMPUTATION, 2017, 27 (02) : 577 - 606
[33] CUT-ELIMINATION IN LOGICS WITH DEFINITIONAL REFLECTION
SCHROEDERHEISTER, P
LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 619 : 146 - 171
[34] Cut-elimination and quantification in canonical systems
Zamansky A.
Avron A.
Studia Logica, 2006, 82 (1) : 157 - 176
[35] Phase semantic cut-elimination and normalization proofs of first- and higher-order linear logic
Okada, M
THEORETICAL COMPUTER SCIENCE, 1999, 227 (1-2) : 333 - 396
[36] A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
Bruscoli, Paola
Guglielmi, Alessio
Gundersen, Tom
Parigot, Michel
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING (LPAR-16), 2010, 6355 : 136 - 153
[37] On the computational complexity of cut-elimination in linear logic
Mairson, HG
Terui, K
THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2003, 2841 : 23 - 36
[38] Algebraic proofs of cut elimination
Avigad, J
JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2001, 49 (1-2): : 15 - 30
[39] Quick cut-elimination for strictly positive cuts
Arai, Toshiyasu
ANNALS OF PURE AND APPLIED LOGIC, 2011, 162 (10) : 807 - 815
[40] The Cut-Elimination Theorem for Differential Nets with Promotion
Pagani, Michele
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2009, 5608 : 219 - 233

← 1 2 3 4 5 →