Superposition in AC Theories : Proof of Completeness by Semantic Trees
Identifieur interne : 00D447 ( Main/Merge ); précédent : 00D446; suivant : 00D448Superposition 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: 001437
- to stream Crin, to step Curation: 001437
- to stream Crin, to step Checkpoint: 003149
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><idno type="wicri:Area/Crin/Checkpoint">003149</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Checkpoint">003149</idno><idno type="wicri:Area/Main/Merge">00D447</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></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 00D447 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 00D447 | 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:vigneron94a
|texte= Superposition in AC Theories : Proof of Completeness by Semantic Trees
}}
| This area was generated with Dilib version V0.6.33. |  |