Superposition in AC Theories : Proof of Completeness by Semantic Trees
Identifieur interne : 001437 ( Crin/Curation ); précédent : 001436; suivant : 001438Superposition in AC Theories : Proof of Completeness by Semantic Trees
Auteurs : Laurent VigneronSource :
English descriptors
- KwdEn :
Abstract
We propose an inference system for automated deduction with equality and associative and commutative operators, based on the strategy of superposition. The associativity and commutativity axioms are handled by the AC-unification algorithm and the inference rules, and we prove the refutational completeness of this system by transfinite semantic trees, without needing the functional reflexive axioms. Moreover, we use all the power of the superposition strategy, i.e. we never superpose into the smallest side of an equation.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :001437
Links to Exploration step
CRIN:vigneron94aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="166">Superposition in AC Theories : Proof of Completeness by Semantic Trees</title>
</titleStmt>
<publicationStmt><idno type="RBID">CRIN:vigneron94a</idno>
<date when="1994" year="1994">1994</date>
<idno type="wicri:Area/Crin/Corpus">001437</idno>
<idno type="wicri:Area/Crin/Curation">001437</idno>
<idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">001437</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en">Superposition in AC Theories : Proof of Completeness by Semantic Trees</title>
<author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>associative and commutativee theories</term>
<term>automated deduction</term>
<term>resolution</term>
<term>semantic trees</term>
<term>superposition</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en" wicri:score="1390">We propose an inference system for automated deduction with equality and associative and commutative operators, based on the strategy of superposition. The associativity and commutativity axioms are handled by the AC-unification algorithm and the inference rules, and we prove the refutational completeness of this system by transfinite semantic trees, without needing the functional reflexive axioms. Moreover, we use all the power of the superposition strategy, i.e. we never superpose into the smallest side of an equation.</div>
</front>
</TEI>
<BibTex type="techreport"><ref>vigneron94a</ref>
<crinnumber>94-R-045</crinnumber>
<category>15</category>
<equipe>PROTHEO</equipe>
<author><e>Vigneron, Laurent</e>
</author>
<title>Superposition in AC Theories : Proof of Completeness by Semantic Trees</title>
<institution>Centre de Recherche en Informatique de Nancy</institution>
<year>1994</year>
<type>Rapport interne</type>
<address>Vandoeuvre-lès-Nancy</address>
<keywords><e>automated deduction</e>
<e>associative and commutativee theories</e>
<e>resolution</e>
<e>superposition</e>
<e>semantic trees</e>
</keywords>
<abstract>We propose an inference system for automated deduction with equality and associative and commutative operators, based on the strategy of superposition. The associativity and commutativity axioms are handled by the AC-unification algorithm and the inference rules, and we prove the refutational completeness of this system by transfinite semantic trees, without needing the functional reflexive axioms. Moreover, we use all the power of the superposition strategy, i.e. we never superpose into the smallest side of an equation.</abstract>
</BibTex>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001437 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 001437 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Crin |étape= Curation |type= RBID |clé= CRIN:vigneron94a |texte= Superposition in AC Theories : Proof of Completeness by Semantic Trees }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |