Abstract
We present a way of transforming a resolution proof containing Skolemization steps into a natural deduction proof without Skolemization of the same formula. 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.
Cite
CITATION STYLE
de Nivelle, H. (2003). Translation of resolution proofs into short first-order proofs without choice axioms. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 365–379). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_33
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
