Positive deduction modulo regular theories
Identifieur interne : 000E63 ( Istex/Curation ); précédent : 000E62; suivant : 000E64Positive deduction modulo regular theories
Auteurs : Laurent Vigneron [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We propose a new technique for dealing with an equational theory ɛ in the clausal framework. This consists of the definition of two inference rules called contextual superposition and extended superposition, and of an algorithm for computing the only needed applications of these last inference rules only by examining the axioms of ɛ. We prove the refutational completeness of this technique for a class of theories ɛ that include all the regular theories, i.e. any theory whose axioms preserve variables. This generalizes the results of Wertz [31] and Paul [17] who could not prove the refutational completeness of their superposition-based systems for any regular theory. We also combine a collection of strategies that decrease the number of possible deductions, without loss of completeness: the superposition strategy, the positive ordering strategy, and a simplification strategy. These results have been implemented in a theorem prover called DATAC, for the case of commutative, and associative and commutative theories. It is an interesting tool for comparing the efficiency of strategies, and practical results will follow.
Url:
DOI: 10.1007/3-540-61377-3_54
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000E75
Links to Exploration step
ISTEX:3EA41A9EC73C454FEB4BA39E6A0DC456C2924921Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Positive deduction modulo regular theories</title><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation wicri:level="1"><mods:affiliation>CRIN-CNRS & INRIA Lorraine, B.P.239, 54506, Vandœuvre-lès-Nancy Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>CRIN-CNRS & INRIA Lorraine, B.P.239, 54506, Vandœuvre-lès-Nancy Cedex</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: Vigneron@Loria.Fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:3EA41A9EC73C454FEB4BA39E6A0DC456C2924921</idno><date when="1996" year="1996">1996</date><idno type="doi">10.1007/3-540-61377-3_54</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-7WH1PHZ9-C/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000E75</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000E75</idno><idno type="wicri:Area/Istex/Curation">000E63</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Positive deduction modulo regular theories</title><author><name sortKey="Vigneron, Laurent" sort="Vigneron, Laurent" uniqKey="Vigneron L" first="Laurent" last="Vigneron">Laurent Vigneron</name><affiliation wicri:level="1"><mods:affiliation>CRIN-CNRS & INRIA Lorraine, B.P.239, 54506, Vandœuvre-lès-Nancy Cedex, France</mods:affiliation><country xml:lang="fr">France</country><wicri:regionArea>CRIN-CNRS & INRIA Lorraine, B.P.239, 54506, Vandœuvre-lès-Nancy Cedex</wicri:regionArea></affiliation><affiliation wicri:level="1"><mods:affiliation>E-mail: Vigneron@Loria.Fr</mods:affiliation><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We propose a new technique for dealing with an equational theory ɛ in the clausal framework. This consists of the definition of two inference rules called contextual superposition and extended superposition, and of an algorithm for computing the only needed applications of these last inference rules only by examining the axioms of ɛ. We prove the refutational completeness of this technique for a class of theories ɛ that include all the regular theories, i.e. any theory whose axioms preserve variables. This generalizes the results of Wertz [31] and Paul [17] who could not prove the refutational completeness of their superposition-based systems for any regular theory. We also combine a collection of strategies that decrease the number of possible deductions, without loss of completeness: the superposition strategy, the positive ordering strategy, and a simplification strategy. These results have been implemented in a theorem prover called DATAC, for the case of commutative, and associative and commutative theories. It is an interesting tool for comparing the efficiency of strategies, and practical results will follow.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000E63 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Curation/biblio.hfd -nk 000E63 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Curation
|type= RBID
|clé= ISTEX:3EA41A9EC73C454FEB4BA39E6A0DC456C2924921
|texte= Positive deduction modulo regular theories
}}
| This area was generated with Dilib version V0.6.33. |  |