 Authors
 Tobias SchmidtSamoa
 Title
 Flexible Heuristic Control for Combining Automation and UserInteraction in Inductive Theorem Proving
 In
 Ph.D. Thesis, Univ. Kaiserslautern, 2006.
Bibtex Entry
 Copyright Owner
 Tobias SchmidtSamoa
 Abstract
 The validity of formulas w.r.t. a specification over firstorder logic with a semantics based on all models is semidecidable. 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 semidecidable  even for firstorder 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 userinteraction in a suitable way.
In this thesis, we aim at developing techniques that enhance automatic proof control of (inductive) theorem provers and that enable userinteraction 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 wellknown 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 wellknown 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 finetune 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.
 Full paper

 Format
 ps.gz
 Size
 1 Mbytes

 Format
 dvi.gz
 Size
 .5 Mbytes
 The fonts of the following pdf version differ from the original,
some originally identical fonts are different in this version,
but the whole file can be searched!
 Format
 pdf.gz
 Size
 2 Mbytes

 Get pdf and djvu from the Official Site
 http://kluedo.ub.unikl.de/volltexte/2006/1968/