Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-39467
Titel: Theory Unification in Abstract Clause Graphs
VerfasserIn: Ohlbach, Hans Jürgen
Sprache: Englisch
Erscheinungsjahr: 1985
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: Clause Graphs, as they were defined in the 1970s, are graphs representing first order formulas in conjunctive normal form together with the resolution possibilities. The nodes are labelled with literals and the edges (links) connect complementary unifiable literals. This report describes a generalization of this concept, called abstract clause graphs. The nodes of abstract clause graphs are still labelled with literals, the links however connect literals that are "unifiable" relative to a given relation between literals. This relation is not explicitely defined; only certain "abstract" properties are required. for instance the existence of a special purpose unification algorithm is assumed which computes substitutions, the application of which makes the relation hold for two literals. When instances of already existing literals are added to the graph (e.g. due to resolution or factoring), the links to the new literals are derived from the links of their ancestors. An inheritance mechanism for such links is presented which operates only on the attached substitutions and does not have to unify the literals. This solves a long standing open problem of connection graph calculi: how to inherit links (with several unifiers attached) such that no unifier has to be computed more than once.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-394675
hdl:20.500.11880/35657
http://dx.doi.org/10.22028/D291-39467
Schriftenreihe: Memo SEKI : SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI
Band: 85,1 KL
Datum des Eintrags: 17-Apr-2023
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-MEMO-85-01-KL_Ohlbach_Theory-Unification-in-Abstract-Clause-Graphs.pdf21,63 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.