Automated Theorem Proving by Test Set Induction
Identifieur interne : 002765 ( Crin/Checkpoint ); précédent : 002764; suivant : 002766Automated Theorem Proving by Test Set Induction
Auteurs : Adel BouhoulaSource :
- Journal of Symbolic Computation ; 1997.
English descriptors
- KwdEn :
Abstract
Test set induction is a goal-directed proof technique which combines the full power of explicit induction and proof by consistency. It works by computing an appropriate explicit induction scheme called {\em a test set}, to trigger the induction proof, and then applies a refutation principle using proof by consistency techniques. We present a general scheme for test set induction together with a simple soundness proof. Our method is based on new notions of test sets, {\em induction variables}, and {\em provable inconsistency}, which allow us to refute false conjectures even in the case where the functions are not completely defined. We show how test sets can be computed when the constructors are not free, and give an algorithm for computing induction variables. Finally, we present a procedure for proof by test set induction which is refutationally complete for a larger class of specifications than has been shown in previous work. The method has been implemented in the prover {\tt SPIKE}. Based on computer experiments dealing with mutual induction, {\tt SPIKE} appears to be more practical and efficient than explicit induction based systems.
Links toward previous steps (curation, corpus...)
Links to Exploration step
CRIN:bouhoula97aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="218">Automated Theorem Proving by Test Set Induction</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:bouhoula97a</idno>
<date when="1997" year="1997">1997</date>
<idno type="wicri:Area/Crin/Corpus">001F73</idno>
<idno type="wicri:Area/Crin/Curation">001F73</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001F73</idno>
<idno type="wicri:Area/Crin/Checkpoint">002765</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">002765</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Automated Theorem Proving by Test Set Induction</title>
<author><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name>
</author>
</analytic>
<series><title level="j">Journal of Symbolic Computation</title>
<imprint><date when="1997" type="published">1997</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Automated Reasoning</term>
<term>Mutual Induction</term>
<term>Term Rewriting Systems</term>
<term>Test Set Induction</term>
<term>Theorem Proving</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="3588">Test set induction is a goal-directed proof technique which combines the full power of explicit induction and proof by consistency. It works by computing an appropriate explicit induction scheme called {\em a test set}, to trigger the induction proof, and then applies a refutation principle using proof by consistency techniques. We present a general scheme for test set induction together with a simple soundness proof. Our method is based on new notions of test sets, {\em induction variables}, and {\em provable inconsistency}, which allow us to refute false conjectures even in the case where the functions are not completely defined. We show how test sets can be computed when the constructors are not free, and give an algorithm for computing induction variables. Finally, we present a procedure for proof by test set induction which is refutationally complete for a larger class of specifications than has been shown in previous work. The method has been implemented in the prover {\tt SPIKE}. Based on computer experiments dealing with mutual induction, {\tt SPIKE} appears to be more practical and efficient than explicit induction based systems.</div>
</front>
</TEI>
<BibTex type="article"><ref>bouhoula97a</ref>
<crinnumber>97-R-282</crinnumber>
<category>1</category>
<equipe>PROTHEO</equipe>
<author><e>Bouhoula, Adel</e>
</author>
<title>Automated Theorem Proving by Test Set Induction</title>
<journal>Journal of Symbolic Computation</journal>
<year>1997</year>
<volume>23</volume>
<number>1</number>
<pages>47-77</pages>
<month>Jan</month>
<keywords><e>Automated Reasoning</e>
<e>Theorem Proving</e>
<e>Test Set Induction</e>
<e>Mutual Induction</e>
<e>Term Rewriting Systems</e>
</keywords>
<abstract>Test set induction is a goal-directed proof technique which combines the full power of explicit induction and proof by consistency. It works by computing an appropriate explicit induction scheme called {\em a test set}, to trigger the induction proof, and then applies a refutation principle using proof by consistency techniques. We present a general scheme for test set induction together with a simple soundness proof. Our method is based on new notions of test sets, {\em induction variables}, and {\em provable inconsistency}, which allow us to refute false conjectures even in the case where the functions are not completely defined. We show how test sets can be computed when the constructors are not free, and give an algorithm for computing induction variables. Finally, we present a procedure for proof by test set induction which is refutationally complete for a larger class of specifications than has been shown in previous work. The method has been implemented in the prover {\tt SPIKE}. Based on computer experiments dealing with mutual induction, {\tt SPIKE} appears to be more practical and efficient than explicit induction based systems.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002765 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Checkpoint/biblio.hfd -nk 002765 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Checkpoint |type= RBID |clé= CRIN:bouhoula97a |texte= Automated Theorem Proving by Test Set Induction }}
This area was generated with Dilib version V0.6.33. |