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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-87-13_Socher_An-Optimized-Transformation-into-Conjunctive-(or-Disjunctive)-Normal-Form.pdf | 1,46 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.