Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

 
 
DownloadE-Mail
  On Generating Small Clause Normal Forms

Nonnengart, A., Rock, G., & Weidenbach, C. (1998). On Generating Small Clause Normal Forms. In C. Kirchner, & H. Kirchner (Eds.), Proceedings of the 15th International Conference on Automated Deduction (CADE-98) (pp. 397-411). Berlin, Germany: Springer.

Item is

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Nonnengart, Andreas1, Autor           
Rock, Georg1, Autor           
Weidenbach, Christoph1, 2, Autor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Inhalt

einblenden:
ausblenden:
Schlagwörter: -
 Zusammenfassung: 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.

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2010-03-121998
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: -
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: eDoc: 519904
Anderer: Local-ID: C1256104005ECAFC-F90CA2B7700E75AD412566FD00528EB0-NonnengartRockWeidenbach98
 Art des Abschluß: -

Veranstaltung

einblenden:
ausblenden:
Titel: Untitled Event
Veranstaltungsort: Lindau, Germany
Start-/Enddatum: 1998

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle 1

einblenden:
ausblenden:
Titel: Proceedings of the 15th International Conference on Automated Deduction (CADE-98)
Genre der Quelle: Konferenzband
 Urheber:
Kirchner, Claude, Herausgeber
Kirchner, Hélène, Herausgeber
Affiliations:
-
Ort, Verlag, Ausgabe: Berlin, Germany : Springer
Seiten: - Band / Heft: - Artikelnummer: - Start- / Endseite: 397 - 411 Identifikator: ISBN: 3-540-64675-2

Quelle 2

einblenden:
ausblenden:
Titel: Lecture Notes in Artificial Intelligence
Genre der Quelle: Reihe
 Urheber:
Affiliations:
Ort, Verlag, Ausgabe: -
Seiten: - Band / Heft: 1421 Artikelnummer: - Start- / Endseite: - Identifikator: -