Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-39588
Titel: | Mechanical Generation of Sorts in Clause Sets |
VerfasserIn: | Schmidt-Schauß, Manfred |
Sprache: | Englisch |
Erscheinungsjahr: | 1985 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | The algorithm SOGEN is described, which transforms a SIG-sorted clause set CS into a SIG'-sorted clause set CS', where the output clause set is smaller, but the sort structure is more sophisticated. This produced clause set is the input for our Theorem Prover. which has ΣRP* , an extension of ΣRP as its basic deductive calculus. Both calculi have resolution and paramodulation as their basic Operations. We prove that the transformation induced by SOGEN does not affect unsatisfiability, respectively satisfiability, of the clause set. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-395885 hdl:20.500.11880/35790 http://dx.doi.org/10.22028/D291-39588 |
Schriftenreihe: | Memo SEKI : SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI |
Band: | 85,6 KL |
Datum des Eintrags: | 9-Mai-2023 |
Bemerkung/Hinweis: | In der GND existiert kein Normdatensatz für die Person, die sie eindeutig als solche identifiziert. Alternative oder damit in Verbindung stehende Schreibweise(n): Schmidt-Schauss, Manfred. |
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-MEMO-85-06-KL_Schmidt-Schauss_Mechanical-Generation-of-Sorts-in-Clause-Sets.pdf | 24,98 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.