Automated Theorem Proving by Test Set Induction
Identifieur interne : 00BA42 ( Main/Exploration ); précédent : 00BA41; suivant : 00BA43Automated 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.
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 001F73
- to stream Crin, to step Curation: 001F73
- to stream Crin, to step Checkpoint: 002765
- to stream Main, to step Merge: 00C219
- to stream Main, to step Curation: 00BA42
Le 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><idno type="wicri:Area/Main/Merge">00C219</idno><idno type="wicri:Area/Main/Curation">00BA42</idno><idno type="wicri:Area/Main/Exploration">00BA42</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><affiliations><list></list><tree><noCountry><name sortKey="Bouhoula, Adel" sort="Bouhoula, Adel" uniqKey="Bouhoula A" first="Adel" last="Bouhoula">Adel Bouhoula</name></noCountry></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00BA42 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00BA42 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= CRIN:bouhoula97a
|texte= Automated Theorem Proving by Test Set Induction
}}
| This area was generated with Dilib version V0.6.33. |  |