Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








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

URL of the conference:


URL for downloading the paper:


Event Address*:

Lindau, Germany

Language:

English

Event Date*
(no longer used):

July, 5-10 1998

Organization:


Event Start Date:

22 September 2019

Event End Date:

22 September 2019

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:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

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, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
01/18/1999 04:01:44 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