Algorithmic introduction of quantified cuts

被引：21

作者：

Hetzl, Stefan ^{[1
]}

Leitsch, Alexander ^{[2
]}

Reis, Giselle ^{[2
]}

Weller, Daniel ^{[1
]}

机构：

[1] Vienna Univ Technol, Inst Discrete Math & Geometry, A-1040 Vienna, Austria

[2] Vienna Univ Technol, Inst Comp Languages, A-1040 Vienna, Austria

来源：

THEORETICAL COMPUTER SCIENCE | 2014年 / 549卷

基金：

奥地利科学基金会;

关键词：

Proof compression; Cut-introduction; Classical logic; First-order logic; COMPLEXITY;

D O I：

10.1016/j.tcs.2014.05.018

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computing a compressed representation of the terms present in the cut-free proof and then cut-formulas that realize such a compression. Finally, a proof using these cut-formulas is constructed. Concerning asymptotic complexity, this method allows an exponential compression of quantifier complexity (the number of quantifier-inferences) of proofs. (C) 2014 Elsevier B.V. All rights reserved.

引用

页码：1 / 16

页数：16

共 41 条

[1] [Anonymous], 1957, J SYMBOLIC LOGIC
[2] [Anonymous], ZAPISKI NAUCHNYKH SE
[3] [Anonymous], 1939, GRUNDLAGEN MATH
[4] On the complexity of Boolean unification
Baader, F
[J]. INFORMATION PROCESSING LETTERS, 1998, 67 (04) : 215 - 220
[5] Baaz M., 1994, Fundamenta Informaticae, V20, P353
[6] Baaz M., 1993, Computer Science Logic. 6th Workshop, CSL '92, P29
[7] ON THE COMPLEXITY OF PROOF DESKOLEMIZATION
Baaz, Matthias
Hetzl, Stefan
Weller, Daniel
[J]. JOURNAL OF SYMBOLIC LOGIC, 2012, 77 (02) : 669 - 686
[8] BOOLOS G, 1984, J PHILOS LOGIC, V13, P372
[9] Bundy A., 2001, HDB AUTOMATED REASON, P845, DOI DOI 10.1016/B978-044450813-3/50015-1
[10] Bundy Alan, 2005, CAMBRIDGE TRACTS THE

← 1 2 3 4 5 →