| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 9656878 | Information and Computation | 2005 | 31 Pages |
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.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Hans de Nivelle,