Induction using term orderings
Identifieur interne : 00CD17 ( Main/Exploration ); précédent : 00CD16; suivant : 00CD18Induction using term orderings
Auteurs : Francois Bronsard [États-Unis, France] ; Uday S. Reddy [États-Unis] ; Robert W. Hasker [États-Unis]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use the lemmas. This feature has always been supported by induction procedures based on Knuth-Bendix completion, but these procedures are limited by the use of rewriting (or rewriting-like) inferences. Our procedure avoids this limitation by making explicit the implicit induction realized by these procedures. As a result, arbitrary deduction mechanisms can be used while still allowing mutual induction.
Url:
DOI: 10.1007/3-540-58156-1_8
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001B39
- to stream Istex, to step Curation: 001B19
- to stream Istex, to step Checkpoint: 002D06
- to stream Main, to step Merge: 00D585
- to stream Main, to step Curation: 00CD17
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Induction using term orderings</title><author><name sortKey="Bronsard, Francois" sort="Bronsard, Francois" uniqKey="Bronsard F" first="Francois" last="Bronsard">Francois Bronsard</name></author><author><name sortKey="Reddy, Uday S" sort="Reddy, Uday S" uniqKey="Reddy U" first="Uday S." last="Reddy">Uday S. Reddy</name></author><author><name sortKey="Hasker, Robert W" sort="Hasker, Robert W" uniqKey="Hasker R" first="Robert W." last="Hasker">Robert W. Hasker</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:76ACBA92C277BC49A6A3E505EA8C036A9B74303F</idno><date when="1994" year="1994">1994</date><idno type="doi">10.1007/3-540-58156-1_8</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-FR05F7PP-4/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001B39</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001B39</idno><idno type="wicri:Area/Istex/Curation">001B19</idno><idno type="wicri:Area/Istex/Checkpoint">002D06</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002D06</idno><idno type="wicri:doubleKey">0302-9743:1994:Bronsard F:induction:using:term</idno><idno type="wicri:Area/Main/Merge">00D585</idno><idno type="wicri:Area/Main/Curation">00CD17</idno><idno type="wicri:Area/Main/Exploration">00CD17</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Induction using term orderings</title><author><name sortKey="Bronsard, Francois" sort="Bronsard, Francois" uniqKey="Bronsard F" first="Francois" last="Bronsard">Francois Bronsard</name><affiliation wicri:level="1"><country xml:lang="fr">États-Unis</country><wicri:regionArea>The University of Illinois at Urbana-Champaign</wicri:regionArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Reddy, Uday S" sort="Reddy, Uday S" uniqKey="Reddy U" first="Uday S." last="Reddy">Uday S. Reddy</name><affiliation wicri:level="1"><country xml:lang="fr">États-Unis</country><wicri:regionArea>The University of Illinois at Urbana-Champaign</wicri:regionArea></affiliation></author><author><name sortKey="Hasker, Robert W" sort="Hasker, Robert W" uniqKey="Hasker R" first="Robert W." last="Hasker">Robert W. Hasker</name><affiliation wicri:level="1"><country xml:lang="fr">États-Unis</country><wicri:regionArea>The University of Illinois at Urbana-Champaign</wicri:regionArea></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use the lemmas. This feature has always been supported by induction procedures based on Knuth-Bendix completion, but these procedures are limited by the use of rewriting (or rewriting-like) inferences. Our procedure avoids this limitation by making explicit the implicit induction realized by these procedures. As a result, arbitrary deduction mechanisms can be used while still allowing mutual induction.</div></front></TEI><affiliations><list><country><li>France</li><li>États-Unis</li></country></list><tree><country name="États-Unis"><noRegion><name sortKey="Bronsard, Francois" sort="Bronsard, Francois" uniqKey="Bronsard F" first="Francois" last="Bronsard">Francois Bronsard</name></noRegion><name sortKey="Hasker, Robert W" sort="Hasker, Robert W" uniqKey="Hasker R" first="Robert W." last="Hasker">Robert W. Hasker</name><name sortKey="Reddy, Uday S" sort="Reddy, Uday S" uniqKey="Reddy U" first="Uday S." last="Reddy">Uday S. Reddy</name></country><country name="France"><noRegion><name sortKey="Bronsard, Francois" sort="Bronsard, Francois" uniqKey="Bronsard F" first="Francois" last="Bronsard">Francois Bronsard</name></noRegion></country></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 00CD17 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00CD17 | 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é= ISTEX:76ACBA92C277BC49A6A3E505EA8C036A9B74303F
|texte= Induction using term orderings
}}
| This area was generated with Dilib version V0.6.33. |  |