Computational Aspects of an Order-Sorted Logic with Term Declarations

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.