MPI-INF Logo
Publications

Server    domino.mpi-inf.mpg.de

Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop

Author, Editor
Author(s):
Nonnengart, Andreas
Rock, Georg
Weidenbach, Christoph		dblp
dblp
dblp
Editor(s):
Kirchner, Claude
Kirchner, Hélène		dblp
dblp
BibTeX cite key*:
NonnengartRockWeidenbach98
Title, Booktitle
Title*:
On Generating Small Clause Normal Forms
Booktitle*:
Proceedings of the 15th International Conference on Automated Deduction (CADE-98)
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
Lindau, Germany
Language:
English
Event Date*
(no longer used):
July, 5-10 1998
Organization:
Event Start Date:
14 April 2021
Event End Date:
14 April 2021
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Artificial Intelligence
Volume:
1421
Number:
Month:
July
Pages:
397-411
Year*:
1998
VG Wort Pages:
ISBN/ISSN:
3-540-64675-2
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
In this paper we focus on two powerful techniques to obtain compact clause normal forms:
Renaming of formulae and refined Skolemization methods.
We illustrate their effect on various examples.
By an exhaustive experiment of all first-order TPTP problems,
it shows that our clause normal form transformation yields fewer clauses and fewer literals
than the methods known and used so far.
This often allows for exponentially shorter proofs and,
in some cases, it makes it even possible for a theorem prover to find a proof where it was
unable to do so with more standard clause normal form transformations.
Keywords:
Theorem Proving
Download
Access Level:

Correlation
MPG Unit:
MPG Subunit:
Audience:
experts only
Appearance:
MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat



BibTeX Entry:

@INPROCEEDINGS{NonnengartRockWeidenbach98,
AUTHOR = {Nonnengart, Andreas and Rock, Georg and Weidenbach, Christoph},
 EDITOR = {Kirchner, Claude and Kirchner, H{\'e}l{\`e}ne},
 TITLE = {On Generating Small Clause Normal Forms},
 BOOKTITLE = {Proceedings of the 15th International Conference on Automated Deduction (CADE-98)},
 PUBLISHER = {Springer},
 YEAR = {1998},
 VOLUME = {1421},
 PAGES = {397--411},
 SERIES = {Lecture Notes in Artificial Intelligence},
 ADDRESS = {Lindau, Germany},
 MONTH = {July},
 ISBN = {3-540-64675-2},
}

Entry last modified by Christoph Weidenbach, 05/12/2006
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)
Andreas Nonnengart		Created
05/12/2006 04:46:38 PM
Revisions
5.
4.
3.
2.
1.		Editor(s)
Christoph Weidenbach
Uwe Brahm
Christine Kiesel
Uwe Brahm
Uwe Brahm		Edit Dates
05/05/99 12:21:35
04/14/99 07:02:03 PM
30/03/99 16:20:53
29.03.99 19:21:39
29.03.99 19:21:09