Paper Info
Title
Proof search tree and cut elimination
Abstract
A new cut elimination method is obtained here by "proof mining" (unwinding) from the following non-effective proof that begins with extracting an infinite branch B when the canonical search tree τ for a given formula E of first order logic is not finite. The branch B determines a semivaluation so that B |= E and (*) every semivaluation can be extended to a total valuation. Since for every derivation d of E and every model M, M |= E, this provides a contradiction showing that τ is finite, ∃l(τ l). A primitive recursive function L(d) such that τ L(d) is obtained using instead of (*) the statement: For every r, if the canonical search tree τr+1 with cuts of complexity r + 1 is finite, then τr is finite. In our proof the reduction of (r+1)-cuts does not introduce new r-cuts but preserves only one of the branches.
Year
DOI
Venue
2008
10.1007/978-3-540-78127-1_28
Pillars of Computer Science
Keywords
Field
DocType
infinite branch b,following non-effective proof,proof search tree,new cut elimination method,branch b,canonical search tree,new r-cuts,formula e,order logic,model m,proof mining,first order logic
Discrete mathematics,Proof search,Combinatorics,Primitive recursive function,First-order logic,Proof mining,Mathematics,Contradiction,Search tree
Conference
Volume
ISSN
ISBN
4800
0302-9743
3-540-78126-9
Citations 
PageRank 
References 
0
0.34
2
Authors
1
Name
Order
Citations
PageRank
Grigori Mints123572.76