Soft typing for clausal inference systems

Abstract

The purpose of this thesis is to study methods for the semantical control of automated theorem proving systems for first-order logic (with equality) based on certain effective abstraction techniques. We propose a general framework called soft typing for clausal inference systems to incorporate the validity/satisfiability of clauses with respect to certain model hypotheses into the control of inference systems. The effectiveness of the method is obtained by inferring automatically abstractions that result in approximations of validity/satisfiability of clauses with respect to these models. For an effective use of soft typing for ordered resolution and superposition, we propose the use of sets of Horn clauses (with equality) to represent approximations of model hypotheses for sets of clauses. We show that certain decidable fragments of first-order logic without equality can be generalized to non-trivial decidable equational theories. Our abstraction techniques, applied to arbitrary sets of clauses (with equality), result exactly in the decidable (equational) fragments. The satisfiability of clauses with respect to the approximations implies the satisfiability in the original model hypotheses.

Wir untersuchen Methoden zur semantischen Steuerung von automatischen Beweissystemen für Logik erster Stufe(mit Gleichheit) mit Hilfe von bestimmten berechenbaren Abstraktionstechniken. Wir schlagen ein allgemeines Konzept vor, das die Berücksichtigung der Gültigkeit beziehungsweise der Erfüllbarkeit von Klauseln bezüglich bestimmter Modellhypothesen in der Steuerung von Inferenzsystemen ermöglicht.Dieses Konzept nennen wir soft typing for clausal inference systems.Die Berechenbarkeit dieser Methoden wird durch automatische Abstraktionstechniken zur Approximation von Gültigkeit beziehungsweise von Erfüllbarkeit von Klauseln gewährleistet. Zur Darstellung der Approximationen von Modellhypothesen über Klauselmengen schlagen wir die Verwendung von Mengen von Hornklauseln (mit Gleichheit)vor, um Soft Typing von geordneter Resolution beziehungsweise Superposition zu ermöglichen. Wir zeigen, dass bestimmte entscheidbare Fragmente von Logik erster Stufe ohne Gleichheit zu nicht-trivialen entscheidbaren Gleichheitstheorien verallgemeinert werden können. Die Anwendung unserer Abstraktionstechniken auf beliebige Klauselmengen (mit Gleichheit) resultiert in diesen entscheidbaren Fragmenten (Gleichheitstheorien)wobei die Erfüllbarkeit von Klauseln bezüglich der Approximationen die Erfüllbarkeit in den ursprünglichen Modellhypothesen impliziert.