MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
de Nivelle, Hansdblp
Editor(s):
Baader, Franzdblp
Not MPII Editor(s):
Baader, Franz
BibTeX cite key*:
deNivelle2003b
Title, Booktitle
Title*:
Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms
Booktitle*:
Automated deduction, CADE-19 : 19th International Conference on Automated Deduction
Event, URLs
Conference URL::
http://www.CADE-19.info/
Downloading URL:
Event Address*:
Miami, USA
Language:
English
Event Date*
(no longer used):
July 2003
Organization:
Event Start Date:
14 May 2003
Event End Date:
18 May 2003
Publisher
Name*:
Springer
URL:
http://www.springer-ny.com
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
2741
Number:
Month:
July
Pages:
365-379
Year*:
2003
VG Wort Pages:
ISBN/ISSN:
3-540-40559-3
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We present a way of transforming a resolution proof containing
Skolemization into a natural deduction proof of the same formula
but not using 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.
Keywords:
theorem proving, proof theory
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:
@INPROCEEDINGS{deNivelle2003b,
AUTHOR = {de Nivelle, Hans},
 EDITOR = {Baader, Franz},
 TITLE = {Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms},
 BOOKTITLE = {Automated deduction, CADE-19 : 19th International Conference on Automated Deduction},
 PUBLISHER = {Springer},
 YEAR = {2003},
 VOLUME = {2741},
 PAGES = {365--379},
 SERIES = {Lecture Notes in Artificial Intelligence},
 ADDRESS = {Miami, USA},
 MONTH = {July},
 ISBN = {3-540-40559-3},
}

Entry last modified by Christine Kiesel, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Hans de Nivelle		Created
04/16/2003 01:57:49 PM
Revisions
14.
13.
12.
11.
10.		Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Hans de Nivelle
Hans de Nivelle		Edit Dates
17.06.2004 14:55:26
17.06.2004 14:54:21
17.06.2004 14:47:38
01/29/2004 10:55:41 AM
01/26/2004 01:24:23 PM