Constrained Equational Reasoning
Identifieur interne : 000805 ( Crin/Corpus ); précédent : 000804; suivant : 000806Constrained 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 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>
</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>
<BibTex type="inproceedings"><ref>kirchner89b</ref>
<crinnumber>89-r-094</crinnumber>
<category>3</category>
<equipe>EURECA</equipe>
<author><e>Kirchner, C.</e>
<e>Kirchner, H.</e>
</author>
<title>Constrained Equational Reasoning</title>
<booktitle>{Proceedings {ISSAC}'89 (International Symposium on Symbolic and Algebraic Computation), Portland (Oregon, USA)}</booktitle>
<year>1989</year>
<month>jul</month>
<keywords><e>automatic theorem proving</e>
<e>equational completion</e>
<e>equational unification</e>
<e>constrained reasoning</e>
<e>lazy constraints solving</e>
</keywords>
<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.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000805 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 000805 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Corpus |type= RBID |clé= CRIN:kirchner89b |texte= Constrained Equational Reasoning }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |