Paper Info
Title
Translation of resolution proofs into short first-order proofs without choice axioms
Abstract
We present a way of transforming a resolution-style proof containing Skolemization into a natural deduction proof without Skolemization. The size of the proof increases only moderately (polynomially). This makes it possible to translate the output of a resolution theorem prover into a purely first-order proof that is moderate in size.
Year
DOI
Venue
2005
10.1016/j.ic.2004.10.011
Inf. Comput.
Keywords
DocType
Volume
short first-order proof,natural deduction proof,03f20,first-order proof,choice axiom,theorem proving,03f05,skolemization,proof theory,68t15,resolution proof,resolution-style proof,resolution theorem prover,natural deduction,theorem prover,first order
Journal
199
Issue
ISSN
Citations 
1-2
Information and Computation
5
PageRank 
References 
Authors
0.63
9
2
Name
Order
Citations
PageRank
hans de nivelle124721.88
franz baader2342.97