Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-40155
Titel: An Optimized Transformation into Conjunctive (or Disjunctive) Normal Form
VerfasserIn: Socher, Rolf
Sprache: Englisch
Erscheinungsjahr: 1987
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: Resolution based theorem proving systems require the conversion of predicate logic formulae into clausal normal form. One step of all procedures performing this transformation is the multiplication into conjunctive normal form. In general this is a critical step, since it can result in an exponential increase in the size of the original formula. In general the resulting clausal normal form even contains many redundant clauses. This paper presents a multiplication algorithm that avoids the generation of these redundant clauses. It is shown that the set of clauses generated by this algorithm is the set of prime implicants (in the sense of Quine) of the original formula. Especially in those cases where the usual multiplication algorithm produces a contradictory set of ground clauses the improved algorithm generates the empty clause.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-401555
hdl:20.500.11880/37667
http://dx.doi.org/10.22028/D291-40155
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 87,13
Datum des Eintrags: 17-Mai-2024
Fakultät: SE - Sonstige Einrichtungen
Fachrichtung: SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz
Professur: SE - Sonstige
Sammlung:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Dateien zu diesem Datensatz:
Datei Beschreibung GrößeFormat 
SEKI-Report-SR-87-13_Socher_An-Optimized-Transformation-into-Conjunctive-(or-Disjunctive)-Normal-Form.pdf1,46 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.