Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-39689
Titel: Computational Aspects of an Order-Sorted Logic with Term Declarations
VerfasserIn: Schmidt-Schauß, Manfred
Sprache: Englisch
Erscheinungsjahr: 1988
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: In this thesis I investigate the logical foundations of a very general order-sorted logic. This sorted logic extends usual first order logic by a partially ordered set of sorts, such that every term is of a particular sort or type, in addition there is a mechanism to define the sort of terms using term declarations. Syntax and semantics of this order-sorted logic with declarations are defined in a natural way. Unification in order-sorted logics with term declarations is undecidable and infinitary, i.e., minimal complete sets of unifiers may be infinite. However, under the restriction that declarations are only of the form f:S1x. . .xSn—>S and that the signature is regular, unification is decidable and minimal complete sets “of unifiers exist and are always finite. Furthermore there exists a signature of this form such that unification is NP-complete. If there is no equality predicate in the logic we use resolution and factoring as inference rules, where the unification algorithm is adapted to the sort-structure. The corresponding calculus is refutation complete. If there is an equality predicate and all equational literals are in unit clauses, we use a special E-unification algorithm and show that under some restrictions such an algorithm can be constructed from an unsorted unification algorithm by postprocessing the set of unifiers. If arbitrary equations are admissible, we use paramodulation as additional inference rule or replace resolution by the E-resolution rule. An algorithm for transforming unary predicates into sorts is presented. It is shown that this algorithm is correct and complete under sensible restrictions. Usually, the algorithm may require exponential time, however, in the special case of Horn clauses the algorithm can be performed in polynomial time. We also investigate term rewriting systems in an order-sorted logic and extend the confluence criterion that is based on critical pairs by critical sort relations.
In dieser Arbeit untersuche ich die logischen Grundlagen einer sehr allgemeinen ordnungssortierten Logik. Diese sortierte Logik erweitert die übliche Logik erster Stufe um eine partiell geordnete Menge von Sorten, so daß jeder Term eine bestimmte Sorte (Typ) hat. Zusätzlich gibt es einen Mechanismus zum Definieren von Termsorten mittels Termdeklarationen. Syntax und Semantik dieser sortierten Logik Werden auf natürliche Weise definiert. Unifikation in ordnungssortierten Logiken mit Termdeklarationen ist unentscheidbar und infinitär, d.h., minimale und vollständige Mengen von Unifikatoren können unendlich sein. Unter der Einschränkung, daß Deklarationen nur von der Form f:S1x.. .xSn—>S sein dürfen und die Signatur regulär ist, erhält man daß Unifikation entscheidbar ist und daß minimale Mengen von Unifikatoren immer endlich sind. Weiterhin gibt es eine solche Signatur, in der Unifikation NP-vollständig ist. Wenn kein Gleichheitsprädikat in der Logik ist, kann man Resolution und Faktorisierung als Ableitungsregeln benutzen, wobei der Unifikationsalgorithmus an die Sortenstruktur angepasst ist. Der zugehörige Kalkül ist widerspruchsvollständig. Wenn ein Gleichheitsprädikat vorhanden ist und alle Gleichungen in Unitklauseln vorkommen, kann man einen speziellen E-Unifikationsalgorithmus benutzen. Wir zeigen, daß man unter gewissen Bedingungen einen Algorithmus aus einem unsortierten Unifikationsalgorithmus und einer Nachbearbeitung der Menge der Unifikatoren konstruieren kann. Wenn beliebige Gleichungen erlaubt sind, benutzt man Paramodulation als zusätzliche Ableitungsregel oder man ersetzt Resolution durch die E-Resolution. Es wird ein Algorithmus zum Transformieren einstelliger Prädikate in Sorten vorgestellt. Von diesem Algorithmus wird gezeigt daß er unter gewissen sinnvollen Einschränkungen korrekt und vollständig ist. Der Algorithmus hat normalerweise exponentielle Zeitkomplexität, aber im Spezailfall von Hornklauseln kann der Algorithmus in polynomialer Zeit ausgeführt werden. Wir untersuchen auch Termersetzungssysteme in einer ordnungssortierten Logik und erweitern das auf kritischen Paaren beruhende Konfluenzkriterium um kritische Sortenrelationen.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-396895
hdl:20.500.11880/35789
http://dx.doi.org/10.22028/D291-39689
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 88,10
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



Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.