Flexible Heuristic Control for Combining Automation and User-Interaction in Inductive Theorem Proving

  • The validity of formulas w.r.t. a specification over first-order logic with a semantics based on all models is semi-decidable. Therefore, we may implement a proof procedure which finds a proof for every valid formula fully automatically. But this semantics often lacks intuition: Some pathological models such as the trivial model may produce unexpected results w.r.t. validity. Instead, we may consider just a class of special models, for instance, the class of all data models. Proofs are then performed using induction. But, inductive validity is not semi-decidable -- even for first-order logic. This theoretical drawback manifests itself in practical limitations: There are theorems that cannot be proved by induction directly but only generalizations can be proved. For their definition, we may have to extend the specification. Therefore, we cannot expect to prove interesting theorems fully automatically. Instead, we have to support user-interaction in a suitable way. In this thesis, we aim at developing techniques that enhance automatic proof control of (inductive) theorem provers and that enable user-interaction in a suitable way. We integrate our new proof techniques into the inductive theorem prover QuodLibet and validate them with various case studies. Essentially, we introduce the following three proof techniques: -We integrate a decision procedure for linear arithmetic into QuodLibet in a close way by defining new inference rules that perform the elementary steps of the decision procedure. This allows us to implement well-known heuristics for automatic proof control. Furthermore, we are able to provide special purpose tactics that support the manual speculation of lemmas if a proof attempt gets stuck. The integration improves the ability of the theorem prover to prove theorems automatically as well as its efficiency. Our approach is competitive with other approaches regarding efficiency; it provides advantages regarding the speculation of lemmas. -The automatic proof control searches for a proof by applying inference rules. The search space is not only infinite, but grows dramatically with the depth of the search. In contrast to this, checking and analyzing performed proofs is very efficient. As the search space also has a high redundancy, it is reasonable to reuse subproofs found during proof search. We define new notions for the contribution of proof steps to a proof. These notions enable the derivation of pruned proofs and the identification of superfluous subformulas in theorems. A proof may be reused in two ways: upward propagation prunes a proof by eliminating superfluous proof steps; sideward reuse closes an open proof obligation by replaying an already found proof. -For interactive theorem provers, it is essential not only to prove automatically as many lemmas as possible but also to restrict proof search in such a way that the proof process stops within a reasonable amount of time. We introduce different markings in the goals to be proved and the lemmas to be applied to restrict proof search in a flexible way: With a forbidden marking, we can simulate well-known approaches for applying conditional lemmas. A mandatory marking provides a new heuristics which is inspired by local contribution of proof steps. With obligatory and generous markings, we can fine-tune the degree of efficiency and extent of proof search manually. With an elaborate case study, we show the benefits of the different techniques, in particular the synergetic effect of their combination.
  • Die Gültigkeit prädikatenlogischer Formeln erster Stufe ist semi-entscheidbar, sofern man bei der Semantik alle Modelle zugrundelegt. Daher ist es möglich ein Beweisverfahren zu implementieren, das für jede gültige Formel einen Beweis vollautomatisch findet. Aber eine Semantik, die alle Modelle berücksichtigt, entspricht oft nicht der Intuition: Einige pathologische Modelle, wie z.B. das triviale Modell, führen zu unerwarteten Resultaten bzgl. der Gültigkeit. In diesem Fall können wir die Klasse der betrachteten Modelle einschränken, z.B. auf die Klasse aller Datenmodelle. Beweise werden in dieser Klasse mit Hilfe von Induktion geführt. Die resultierende induktive Gültigkeit ist jedoch nicht mehr semi-entscheidbar -- nicht einmal für die Prädikatenlogik erster Stufe. Dies hat praktische Auswirkungen: Es gibt Theoreme, die sich nicht direkt durch Induktion zeigen lassen. Statt dessen müssen Generalisierungen betrachtet werden. Um diese definieren zu können, ist evtl. eine Erweiterung der Spezifikation nötig. Daher können wir nicht erwarten, interessante Theoreme vollautomatisch beweisen zu können. Statt dessen müssen wir manuelle Interaktionen in geeigneter Weise unterstützen. In dieser Arbeit entwickeln wir Techniken, die die automatisierte Beweissteuerung von (induktiven) Theorembeweisern verbessern und die manuelle Interaktionen in geeigneter Weise unterstützen. Wir integrieren unsere neuen Beweistechniken in den induktiven Theorembeweiser QuodLibet und validieren sie mit Hilfe diverser Fallstudien. Im Wesentlichen führen wir die folgenden drei neuen Beweistechniken ein: -Wir integrieren eine Entscheidungsprozedur für lineare Arithmetik in QuodLibet auf enge Weise, indem wir neue Inferenzregeln definieren, die den elementaren Schritten der Entscheidungsprozedur entsprechen. Auf diese Weise können wir alle Heuristiken implementieren, die für eine automatisierte Beweissteuerung bekannt sind. Außerdem können wir spezielle Taktiken zur Verfügung stellen, die im Fall erfolgloser Beweisversuche die manuelle Spekulation von Lemmata unterstützen. Die Integration verbessert sowohl die Effektivität als auch die Effizienz der automatisierten Beweissuche. Unser Ansatz ist bzgl. der Effizienz mit anderen Ansätzen vergleichbar; er bietet jedoch zusätzliche Vorteile beim Spekulieren von Lemmata. -Die automatisierte Beweissteuerung sucht Beweise durch Anwenden von Inferenzregeln. Der Suchraum ist nicht nur unendlich, sondern wächst dramatisch in Abhängigkeit von der Tiefe der Suche. Im Gegensatz zur Suche neuer Beweise kann die Analyse von gefundenden Beweise sehr effizient durchgeführt werden. Da der Suchraum eine hohe Redundanz aufweist, ist es sinnvoll gefundene Teilbeweise wiederzuverwenden. Wir führen neue Begriffe ein, die den Beitrag eines Beweisschritts zu einem Beweis festlegen. Diese Begriffe erlauben das Bereinigen von Beweisen und die Identifikation von unnötigen Teilformeln, die zum Beweis eines Theorems nichts beitragen. Ein Beweis kann auf zwei Arten wiederverwendet werden: Die Aufwärtspropagierung bereinigt einen Beweis, indem überflüssige Beweisschritte entfernt werden; die Seitwärtswiederverwendung überträgt einen alten Beweis auf ein offenes Beweisziel. -Für interaktive Beweiser ist es wichtig, nicht nur so viele Lemmata wie möglich automatisch zu beweisen, sondern auch die Beweissuche derart einzuschränken, dass sie in vernünftiger Zeit terminiert. Wir führen verschiedene Markierungen ein, um die Beweissuche in flexibler Weise zu steuern -- zum einen auf den Zielen, die bewiesen werden sollen, und zum anderen auf den Lemmata, die angewendet werden dürfen: Mit einer verbotenen Markierung können wir bekannte Ansätze simulieren, die die Anwendung von bedingten Lemmata steuern. Eine verpflichtende Markierung führt zu einer neuen Heuristik, die auf dem lokalen Beitrag von Beweisschritten beruht. Mit obligatorischen und großzügigen Markierungen schließlich können wir die Effizienz und den Umfang der Beweissuche manuell steuern. Anhand einer umfassenden Fallstudie zeigen wir die Vorteile unserer verschiedenen Techniken auf, insbesondere den synergetischen Effekt, der aus ihrer Kombination resultiert.

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Tobias Schmidt-Samoa
URN (permanent link):urn:nbn:de:hbz:386-kluedo-19687
Advisor:Jürgen Avenhaus
Document Type:Doctoral Thesis
Language of publication:English
Year of Completion:2006
Year of Publication:2006
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2006/06/16
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:004 Datenverarbeitung; Informatik

$Rev: 12793 $