Proof Management and Retrieval
Thomas H. Kolbe, Christoph Walther, Fachbereich Informatik, Technische Universität Darmstadt · TUbilio (Technical University of Darmstadt) · 1995
. 1 Automated theorem provers might be improved if they reuse previously computed proofs. Our approach for reuse is based on so-called proof shells which are obtained from computed proofs by second-order generalization. Each proof shell represents a schematic proof of a schematic conjecture and applies for each instance of the schematic conjecture yielding (first-order) proof obligations justifying a successful proof reuse. But since there may be different proofs for different instances of a schematic conjecture, we have to select a reusable proof shell among the applicable proof shells for a new conjecture. For supporting such a retrieval efficiently, the set of computed proof shells is organized by so-called proof volumes and a proof dictionary. All applicable proof shells can be accessed by searching for the right proof volume in the proof dictionary, if the applicability of proof shells is determined by so-called simple second-order matchers. 1 Introduction Automated theorem p...