Proofs by induction in equational theories without constructors
Identifieur interne : 00F024 ( Main/Merge ); précédent : 00F023; suivant : 00F025Proofs by induction in equational theories without constructors
Auteurs : J.-P. Jouannaud ; E. KounalisSource :
English descriptors
- KwdEn :
Abstract
Inductionless Induction consists of using pure equational reasoning for proving validity of an equation in the initial algebra of a set of equational axioms, which would normally require some kind of induction. Under given hypotheses, the equation is valid if adding it to the set of axioms does not result in an inconsistency. This inconsistency can be found by the Knuth-Bendix completion algorithm, provided that the signature of the algebra is split into free constructors and defined symbols, which must be completely defined in terms of constructors. This is the base of the so-called Inductive Completion algorithm of Huet and Hullot. A key new concept, quasi-reducibility, allows us to extend these techniques in various directions\, : incomplete specifications, non free constructors, no constructors specified, equational term rewriting systems. In addition, we get for free a simple algorithm to exhibit a set of constructors of a specification. Finally, we modify our algorithm for proving the consistency property of an enrichment of a specification by new operators and new equations.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 000251
- to stream Crin, to step Curation: 000251
- to stream Crin, to step Checkpoint: 004241
Links to Exploration step
CRIN:jouannaud86aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="337">Proofs by induction in equational theories without constructors</title></titleStmt><publicationStmt><idno type="RBID">CRIN:jouannaud86a</idno><date when="1986" year="1986">1986</date><idno type="wicri:Area/Crin/Corpus">000251</idno><idno type="wicri:Area/Crin/Curation">000251</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">000251</idno><idno type="wicri:Area/Crin/Checkpoint">004241</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">004241</idno><idno type="wicri:Area/Main/Merge">00F024</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Proofs by induction in equational theories without constructors</title><author><name sortKey="Jouannaud, J P" sort="Jouannaud, J P" uniqKey="Jouannaud J" first="J.-P." last="Jouannaud">J.-P. Jouannaud</name></author><author><name sortKey="Kounalis, E" sort="Kounalis, E" uniqKey="Kounalis E" first="E." last="Kounalis">E. Kounalis</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>induction</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="4593">Inductionless Induction consists of using pure equational reasoning for proving validity of an equation in the initial algebra of a set of equational axioms, which would normally require some kind of induction. Under given hypotheses, the equation is valid if adding it to the set of axioms does not result in an inconsistency. This inconsistency can be found by the Knuth-Bendix completion algorithm, provided that the signature of the algebra is split into free constructors and defined symbols, which must be completely defined in terms of constructors. This is the base of the so-called Inductive Completion algorithm of Huet and Hullot. A key new concept, quasi-reducibility, allows us to extend these techniques in various directions\, : incomplete specifications, non free constructors, no constructors specified, equational term rewriting systems. In addition, we get for free a simple algorithm to exhibit a set of constructors of a specification. Finally, we modify our algorithm for proving the consistency property of an enrichment of a specification by new operators and new equations.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00F024 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00F024 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= CRIN:jouannaud86a
|texte= Proofs by induction in equational theories without constructors
}}
| This area was generated with Dilib version V0.6.33. |  |