Constrained Equational Reasoning
Identifieur interne : 00E820 ( Main/Merge ); précédent : 00E819; suivant : 00E821Constrained Equational Reasoning
Auteurs : C. Kirchner ; H. KirchnerSource :
English descriptors
- KwdEn :
Abstract
We describe and give the foundation for constrained equational reasoning. Equational reasoning is based on replacement of equal by equal and these replacements use substitutions determined as solutions of equations. Constrained equational reasoning takes advantage from the information contained into the equation itself to develop equational reasoning, avoids instantiations as much as possible and solve constraints as late as possible. For theories like associativity-commutativity this can lead to a considerable reduction of the substitution computation overhead, bringing some problems, untractable in practice, to the realm of computational reality.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: 000805
- to stream Crin, to step Curation: 000805
- to stream Crin, to step Checkpoint: 003D68
Links to Exploration step
CRIN:kirchner89bLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="342">Constrained Equational Reasoning</title></titleStmt><publicationStmt><idno type="RBID">CRIN:kirchner89b</idno><date when="1989" year="1989">1989</date><idno type="wicri:Area/Crin/Corpus">000805</idno><idno type="wicri:Area/Crin/Curation">000805</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">000805</idno><idno type="wicri:Area/Crin/Checkpoint">003D68</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003D68</idno><idno type="wicri:Area/Main/Merge">00E820</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Constrained Equational Reasoning</title><author><name sortKey="Kirchner, C" sort="Kirchner, C" uniqKey="Kirchner C" first="C." last="Kirchner">C. Kirchner</name></author><author><name sortKey="Kirchner, H" sort="Kirchner, H" uniqKey="Kirchner H" first="H." last="Kirchner">H. Kirchner</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automatic theorem proving</term><term>constrained reasoning</term><term>equational completion</term><term>equational unification</term><term>lazy constraints solving</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2972">We describe and give the foundation for constrained equational reasoning. Equational reasoning is based on replacement of equal by equal and these replacements use substitutions determined as solutions of equations. Constrained equational reasoning takes advantage from the information contained into the equation itself to develop equational reasoning, avoids instantiations as much as possible and solve constraints as late as possible. For theories like associativity-commutativity this can lead to a considerable reduction of the substitution computation overhead, bringing some problems, untractable in practice, to the realm of computational reality.</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 00E820 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00E820 | 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:kirchner89b
|texte= Constrained Equational Reasoning
}}
| This area was generated with Dilib version V0.6.33. |  |