Automatically assigned DDC number: 006333

Manually assigned DDC number: 006333

Number of references: 4

Title: Termination of Theorem Proving by Reuse

Author:

Author:

Author:

Author:

Subject: Thomas Kolbe,Christoph Walther,Fachbereich Informatik,Technische Hochschule Darmstadt Termination of Theorem Proving by Reuse

Description: . We investigate the improvement of theorem provers by reusing previously computed proofs. We formulate our method for reusing proofs as an instance of the problem reduction paradigm and then develop a termination requirement for our reuse procedure. We prove the soundness of our proposal and show that reusability of proofs is not spoiled by the termination requirement imposed on the reuse procedure. We also give evidence for the general usefulness of our termination requirement for lemma speculation in induction theorem proving. 1 Introduction We investigate the improvement of theorem provers by reusing previously computed proofs, cf. [12, 13]. Our work has similarities with the methodologies of explanation-based learning [7], analogical reasoning [9], and abstraction [8], cf. [14] for a more detailed comparison. Consider the following general architecture: Some problem solver PS is augmented with a facility for storing and retrieving solutions of problems solved during the system's...

Contributor: The Pennsylvania State University CiteSeer Archives

Publisher: unknown

Date: 1996-04-23

Pubyear: 1996

Format: ps

Identifier: http://citeseer.ist.psu.edu/140702.html

Source: http://kirmes.inferenzsysteme.informatik.th-darmstadt.de/~kolbe/cade96.ps.Z

Language: en

Relation:

Relation:

Relation:

Relation:

Rights: unrestricted

Graph

<?xml   version="1.0"   encoding="UTF-8"?>

<references_metadata>

      <rec   ID="/517606.html"   Type="article"   CiteSeer_Book="Journal   of   Automated   Reasoning"   CiteSeer_Volume="16"   Title="Productive   Use   of   Failure   in   Inductive   Proof,">

            <identifier   Org="ISBN:038720170X"   Paper_ID="/517606.html"   Extracted="038720170X"   DDC="005.1/2"   Normalized_DDC="00512"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:052183449X"   Paper_ID="/517606.html"   Extracted="052183449X"   DDC="006.3/33"   Normalized_DDC="006333"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:0792362616"   Paper_ID="/517606.html"   Extracted="0792362616"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:1402007124"   Paper_ID="/517606.html"   Extracted="1402007124"   DDC="501"   Normalized_DDC="501"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:1402007493"   Paper_ID="/517606.html"   Extracted="1402007493"   DDC="530.13/8"   Normalized_DDC="530138"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:1402007914"   Paper_ID="/517606.html"   Extracted="1402007914"   DDC="501"   Normalized_DDC="501"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:1402016565"   Paper_ID="/517606.html"   Extracted="1402016565"   DDC="511.3"   Normalized_DDC="5113"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540213775"   Paper_ID="/517606.html"   Extracted="3540213775"   DDC="004.0151"   Normalized_DDC="0040151"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540214593"   Paper_ID="/517606.html"   Extracted="3540214593"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540230173"   Paper_ID="/517606.html"   Extracted="3540230173"   DDC="511.36028563"   Normalized_DDC="51136028563"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540232125"   Paper_ID="/517606.html"   Extracted="3540232125"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:354031430X"   Paper_ID="/517606.html"   Extracted="354031430X"   DDC="510/.285"   Normalized_DDC="510285"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540405593"   Paper_ID="/517606.html"   Extracted="3540405593"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540439609"   Paper_ID="/517606.html"   Extracted="3540439609"   DDC="005.1/15"   Normalized_DDC="005115"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540615113"   Paper_ID="/517606.html"   Extracted="3540615113"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540664289"   Paper_ID="/517606.html"   Extracted="3540664289"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540664920"   Paper_ID="/517606.html"   Extracted="3540664920"   DDC="005.1/15"   Normalized_DDC="005115"   Normalized_Weight="0.05555555555555555"   />

            <identifier   Org="ISBN:3540677976"   Paper_ID="/517606.html"   Extracted="3540677976"   DDC="004/.01/5113"   Normalized_DDC="004015113"   Normalized_Weight="0.05555555555555555"   />

      </rec>

      <rec   ID="/91086.html"   Type="inproceedings"   CiteSeer_Book="European   Conference   on   Artificial   Intelligence"   CiteSeer_Volume=""   Title="Reusing   Proofs,">

            <identifier   Org="ISBN:0818620307"   Paper_ID="/91086.html"   Extracted="0818620307"   />

            <identifier   Org="ISBN:1402007493"   Paper_ID="/91086.html"   Extracted="1402007493"   DDC="530.13/8"   Normalized_DDC="530138"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540223819"   Paper_ID="/91086.html"   Extracted="3540223819"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540230173"   Paper_ID="/91086.html"   Extracted="3540230173"   DDC="511.36028563"   Normalized_DDC="51136028563"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:354023635X"   Paper_ID="/91086.html"   Extracted="354023635X"   DDC="005.8"   Normalized_DDC="0058"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:354056733X"   Paper_ID="/91086.html"   Extracted="354056733X"   />

            <identifier   Org="ISBN:3540581561"   Paper_ID="/91086.html"   Extracted="3540581561"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540592865"   Paper_ID="/91086.html"   Extracted="3540592865"   DDC="006.3/1"   Normalized_DDC="00631"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540609733"   Paper_ID="/91086.html"   Extracted="3540609733"   DDC="005.1/01/5113"   Normalized_DDC="0051015113"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540615113"   Paper_ID="/91086.html"   Extracted="3540615113"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540616306"   Paper_ID="/91086.html"   Extracted="3540616306"   DDC="006.3/01/5113"   Normalized_DDC="0063015113"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540631046"   Paper_ID="/91086.html"   Extracted="3540631046"   DDC="006.3/33"   Normalized_DDC="006333"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540635866"   Paper_ID="/91086.html"   Extracted="3540635866"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540649905"   Paper_ID="/91086.html"   Extracted="3540649905"   />

            <identifier   Org="ISBN:3540662375"   Paper_ID="/91086.html"   Extracted="3540662375"   DDC="006.3/33"   Normalized_DDC="006333"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540787380"   Paper_ID="/91086.html"   Extracted="3540787380"   DDC="005.1"   Normalized_DDC="0051"   Normalized_Weight="0.07142857142857142"   />

            <identifier   Org="ISBN:3540797068"   Paper_ID="/91086.html"   Extracted="3540797068"   />

            <identifier   Org="ISBN:427490525X"   Paper_ID="/91086.html"   Extracted="427490525X"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.07142857142857142"   />

      </rec>

      <rec   ID="/189908.html"   Type="article"   CiteSeer_Book="Lecture   Notes   in   Computer   Science"   CiteSeer_Volume="912"   Title="Patching   Proofs   for   Reuse,">

            <identifier   Org="ISBN:0262510987"   Paper_ID="/189908.html"   Extracted="0262510987"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.16666666666666666"   />

            <identifier   Org="ISBN:1402007493"   Paper_ID="/189908.html"   Extracted="1402007493"   DDC="530.13/8"   Normalized_DDC="530138"   Normalized_Weight="0.16666666666666666"   />

            <identifier   Org="ISBN:3540432876"   Paper_ID="/189908.html"   Extracted="3540432876"   DDC="006.3/33"   Normalized_DDC="006333"   Normalized_Weight="0.16666666666666666"   />

            <identifier   Org="ISBN:3540592865"   Paper_ID="/189908.html"   Extracted="3540592865"   DDC="006.3/1"   Normalized_DDC="00631"   Normalized_Weight="0.16666666666666666"   />

            <identifier   Org="ISBN:3540604286"   Paper_ID="/189908.html"   Extracted="3540604286"   DDC="006.3"   Normalized_DDC="0063"   Normalized_Weight="0.16666666666666666"   />

            <identifier   Org="ISBN:3540615113"   Paper_ID="/189908.html"   Extracted="3540615113"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.16666666666666666"   />

      </rec>

      <rec   ID="/29968.html"   Type="misc"   CiteSeer_Book=""   CiteSeer_Volume=""   Title="Proof   Management   and   Retrieval,">

            <identifier   Org="ISBN:1402007493"   Paper_ID="/29968.html"   Extracted="1402007493"   DDC="530.13/8"   Normalized_DDC="530138"   Normalized_Weight="0.25"   />

            <identifier   Org="ISBN:1411611721"   Paper_ID="/29968.html"   Extracted="1411611721"   />

            <identifier   Org="ISBN:3540415173"   Paper_ID="/29968.html"   Extracted="3540415173"   DDC="005.13/1"   Normalized_DDC="005131"   Normalized_Weight="0.25"   />

            <identifier   Org="ISBN:3540615113"   Paper_ID="/29968.html"   Extracted="3540615113"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.25"   />

            <identifier   Org="ISBN:3540631046"   Paper_ID="/29968.html"   Extracted="3540631046"   DDC="006.3/33"   Normalized_DDC="006333"   Normalized_Weight="0.25"   />

      </rec>

      <rec   ID="SELF"   Type="SELF"   CiteSeer_Book="SELF"   CiteSeer_Volume="SELF"   Title="Termination   of   Theorem   Proving   by   Reuse">

            <identifier   Org="ISBN:1402007493"   Paper_ID="SELF"   Extracted="1402007493"   DDC="530.13/8"   Normalized_DDC="530138"   Normalized_Weight="0.3333333333333333"   />

            <identifier   Org="ISBN:1586031503"   Paper_ID="SELF"   Extracted="1586031503"   />

            <identifier   Org="ISBN:3540615113"   Paper_ID="SELF"   Extracted="3540615113"   DDC="006.3/3"   Normalized_DDC="00633"   Normalized_Weight="0.3333333333333333"   />

            <identifier   Org="ISBN:3540631046"   Paper_ID="SELF"   Extracted="3540631046"   DDC="006.3/33"   Normalized_DDC="006333"   Normalized_Weight="0.3333333333333333"   />

      </rec>

</references_metadata>