Proof normalization modulo

被引：42

作者：

Dowek, G ^{[1
]}

Werner, B ^{[1
]}

机构：

[1] Ecole Polytech, LIX, INRIA, F-91128 Palaiseau, France

来源：

JOURNAL OF SYMBOLIC LOGIC | 2003年 / 68卷 / 04期

关键词：

D O I：

10.2178/jsl/1067620188

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

We define a generic notion of cut that applies to many first-order theories. We prove a generic cut elimination theorem showing that the cut elimination property holds for all theories having a so-called pre-model. As a corollary, we retrieve cut elimination for several axiomatic theories, including Church's simple type theory.

引用

页码：1289 / 1316

页数：28

共 50 条

[11] Proof Checking Technology for Satisfiability Modulo Theories
Stump, Aaron
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 228 : 121 - 133
[12] Proof of a conjecture on a congruence modulo 243 for overpartitions
Huang, Xiaoqian
Yao, Olivia X. M.
PERIODICA MATHEMATICA HUNGARICA, 2019, 79 (02) : 227 - 235
[13] Exponentially Handsome Proof Nets and Their Normalization
Acclavio, Matteo
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (353): : 1 - 25
[14] Truth values algebras and proof normalization
Dowek, Gilles
TYPES FOR PROOFS AND PROGRAMS, 2007, 4502 : 110 - 124
[15] A COMPUTATIONAL PROOF OF THE NOETHER NORMALIZATION LEMMA
LOGAR, A
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 357 : 259 - 273
[16] Hardness and Optimality in QBF Proof Systems Modulo NP
Chew, Leroy
THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, SAT 2021, 2021, 12831 : 98 - 115
[17] Axiomatic Constraint Systems for Proof Search Modulo Theories
Rouhling, Damien
Farooque, Mahfuza
Graham-Lengrand, Stephane
Mahboubi, Assia
Notin, Jean-Marc
FRONTIERS OF COMBINING SYSTEMS, FROCOS 2015, 2015, 9322 : 220 - 236
[18] ZERO KNOWLEDGE INTERACTIVE PROOF SYSTEM FOR MODULO OPERATIONS
KUROSAWA, K
IEICE TRANSACTIONS ON COMMUNICATIONS ELECTRONICS INFORMATION AND SYSTEMS, 1991, 74 (08): : 2124 - 2128
[19] Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
Beylin, I
Dybjer, P
TYPES FOR PROOFS AND PROGRAMS, 1996, 1158 : 47 - 61
[20] Proof theory for heterogeneous logic combining formulas and diagrams: proof normalization
Ryo Takemura
Archive for Mathematical Logic, 2021, 60 : 783 - 813

← 1 2 3 4 5 →