Automated deduction with associative-commutative operators
Identifieur interne : 00C780 ( Main/Exploration ); précédent : 00C779; suivant : 00C781Automated deduction with associative-commutative operators
Auteurs : Michaël Rusinowitch [France] ; Laurent Vigneron [France]Source :
- Applicable Algebra in Engineering, Communication and Computing [ 0938-1279 ] ; 1995-01-01.
Descripteurs français
- Wicri :
- topic : Résolution.
English descriptors
- KwdEn :
- Teeft :
- Algorithm, Associative, Associative path, Axiom, Clause, Common head_subterms, Commutative, Commutative theories, Complete simplification, Completeness, Completeness theorem, Comput, Computer science, Contextual paramodulation, Different value, Empty clause, Empty interpretation, Empty theory, Equality predicate, Equational, Equational theories, Failure node, Failure nodes, Falsifies, Ground atoms, Ground clause, Ground clauses, Ground instance, Ground substitution, Ground term, Ground terms, Head_subterms, Heidelberg, Herbrand, Inference, Inference rules, Inference step, Inference system, International conference, Irreducible, Irreducible atom, Last clause, Last node, Lecture notes, Limit ordinal, Maximal occurrence, Maximal path, Modulo, Node, Ordinal, Para, Paramodulation, Paramodulation rule, Paramodulation rules, Paramodulation step, Persistent clause, Reducible, Refutational, Refutational completeness, Resp, Right extension, Right node, Rightmost path, Rusinowitch, Simple example, Simplification, Simplification rules, Smallest atom, Springer, Substitution, Subterm, Technical report, Transfinite, Unification algorithm, Vigneron.
Abstract
Abstract: We propose a new inference system for automated deduction with equality and associative commutative operators. This system is an extension of the ordered paramodulation strategy. However, rather than using associativity and commutativity as the other axioms, they are handled by the AC-unification algorithm and the inference rules. Moreover, we prove the refutational completeness of this system without needing the functional reflexive axioms or AC-axioms. Such a result is obtained by semantic tree techniques. We also show that the inference system is compatible with simplification rules.
Url:
DOI: 10.1007/BF01270929
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000399
- to stream Istex, to step Curation: 000397
- to stream Istex, to step Checkpoint: 002B95
- to stream Main, to step Merge: 00D037
- to stream Main, to step Curation: 00C780
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automated deduction with associative-commutative operators</title><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name></author><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:11C96BA8EB274E3CD640E2C0A6926876244579A6</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1007/BF01270929</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-T68FWK1S-H/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000399</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000399</idno><idno type="wicri:Area/Istex/Curation">000397</idno><idno type="wicri:Area/Istex/Checkpoint">002B95</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002B95</idno><idno type="wicri:doubleKey">0938-1279:1995:Rusinowitch M:automated:deduction:with</idno><idno type="wicri:Area/Main/Merge">00D037</idno><idno type="wicri:Area/Main/Curation">00C780</idno><idno type="wicri:Area/Main/Exploration">00C780</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automated deduction with associative-commutative operators</title><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>CRIN and INRIA-Lorraine, BP239, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country><wicri:regionArea>E-mail: Michael.Rusinowitch</wicri:regionArea></affiliation></author><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>CRIN and INRIA-Lorraine, BP239, 54506, Vandœuvre-lés-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Applicable Algebra in Engineering, Communication and Computing</title><title level="j" type="abbrev">AAECC</title><idno type="ISSN">0938-1279</idno><idno type="eISSN">1432-0622</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="1995-01-01">1995-01-01</date><biblScope unit="volume">6</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="23">23</biblScope><biblScope unit="page" to="56">56</biblScope></imprint><idno type="ISSN">0938-1279</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0938-1279</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Associative and Commutative Theories</term><term>Automated Deduction</term><term>Paramodulation</term><term>Resolution</term><term>Term Rewriting</term></keywords><keywords scheme="Teeft" xml:lang="en"><term>Algorithm</term><term>Associative</term><term>Associative path</term><term>Axiom</term><term>Clause</term><term>Common head_subterms</term><term>Commutative</term><term>Commutative theories</term><term>Complete simplification</term><term>Completeness</term><term>Completeness theorem</term><term>Comput</term><term>Computer science</term><term>Contextual paramodulation</term><term>Different value</term><term>Empty clause</term><term>Empty interpretation</term><term>Empty theory</term><term>Equality predicate</term><term>Equational</term><term>Equational theories</term><term>Failure node</term><term>Failure nodes</term><term>Falsifies</term><term>Ground atoms</term><term>Ground clause</term><term>Ground clauses</term><term>Ground instance</term><term>Ground substitution</term><term>Ground term</term><term>Ground terms</term><term>Head_subterms</term><term>Heidelberg</term><term>Herbrand</term><term>Inference</term><term>Inference rules</term><term>Inference step</term><term>Inference system</term><term>International conference</term><term>Irreducible</term><term>Irreducible atom</term><term>Last clause</term><term>Last node</term><term>Lecture notes</term><term>Limit ordinal</term><term>Maximal occurrence</term><term>Maximal path</term><term>Modulo</term><term>Node</term><term>Ordinal</term><term>Para</term><term>Paramodulation</term><term>Paramodulation rule</term><term>Paramodulation rules</term><term>Paramodulation step</term><term>Persistent clause</term><term>Reducible</term><term>Refutational</term><term>Refutational completeness</term><term>Resp</term><term>Right extension</term><term>Right node</term><term>Rightmost path</term><term>Rusinowitch</term><term>Simple example</term><term>Simplification</term><term>Simplification rules</term><term>Smallest atom</term><term>Springer</term><term>Substitution</term><term>Subterm</term><term>Technical report</term><term>Transfinite</term><term>Unification algorithm</term><term>Vigneron</term></keywords><keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Résolution</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We propose a new inference system for automated deduction with equality and associative commutative operators. This system is an extension of the ordered paramodulation strategy. However, rather than using associativity and commutativity as the other axioms, they are handled by the AC-unification algorithm and the inference rules. Moreover, we prove the refutational completeness of this system without needing the functional reflexive axioms or AC-axioms. Such a result is obtained by semantic tree techniques. We also show that the inference system is compatible with simplification rules.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name></region><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00C780 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00C780 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:11C96BA8EB274E3CD640E2C0A6926876244579A6
|texte= Automated deduction with associative-commutative operators
}}
| This area was generated with Dilib version V0.6.33. |  |