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öße | Format | |
---|---|---|---|---|
SEKI-MEMO-85-01-KL_Ohlbach_Theory-Unification-in-Abstract-Clause-Graphs.pdf | 21,63 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.