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 条

[1] Modular cut-elimination: Finding proofs or counterexamples
Ciabattoni, Agata
Terui, Kazushige
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2006, 4246 : 135 - 149
[2] Failure of cut-elimination in cyclic proofs of separation logic
Kimura D.
Nakazawa K.
Terauchi T.
Unno H.
1600, Japan Society for Software Science and Technology (37): : 39 - 52
[3] An isomorphism between cut-elimination procedure and proof reduction
Nakazawa, Koji
Typed Lambda Calculi and Applications, Proceedings, 2007, 4583 : 336 - 350
[4] STRATIFICATION AND CUT-ELIMINATION
CRABBE, M
JOURNAL OF SYMBOLIC LOGIC, 1991, 56 (01) : 213 - 226
[5] Methods of Cut-Elimination
Buss, Sam
STUDIA LOGICA, 2015, 103 (03) : 663 - 667
[6] Cut-elimination for ω1
Arai, Toshiyasu
ANNALS OF PURE AND APPLIED LOGIC, 2018, 169 (12) : 1246 - 1269
[7] Strong normalisation for a Gentzen-like cut-elimination procedure
Urban, C
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2001, 2044 : 415 - 429
[8] COMMON KNOWLEDGE: A FINITARY CALCULUS WITH A SYNTACTIC CUT-ELIMINATION PROCEDURE
Poggiolesi, Francesca
Hill, Brian
LOGIQUE ET ANALYSE, 2015, (230) : 279 - 306
[9] On a local-step cut-elimination procedure for the intuitionistic sequent calculus
Kikuchi, Kentaro
Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2006, 4246 : 120 - 134
[10] Cut-Elimination for the Modal Grzegorczyk Logic via Non-well-founded Proofs
Savateev, Yury
Shamkanov, Daniyar
LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION: 24TH INTERNATIONAL WORKSHOP, WOLLIC 2017, LONDON, UK, JULY 18-21, 2017, PROCEEDINGS, 2017, 10388 : 321 - 335

← 1 2 3 4 5 →