A Model-Based Completeness Proof of Extended Narrowing and Resolution
Identifieur interne : 009397 ( Main/Exploration ); précédent : 009396; suivant : 009398A Model-Based Completeness Proof of Extended Narrowing and Resolution
Auteurs : Jürgen Stuber [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Abstract: We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.
Url:
DOI: 10.1007/3-540-45744-5_15
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003966
- to stream Istex, to step Curation: 003922
- to stream Istex, to step Checkpoint: 001F39
- to stream Main, to step Merge: 009919
- to stream PascalFrancis, to step Corpus: 000942
- to stream PascalFrancis, to step Curation: 000134
- to stream PascalFrancis, to step Checkpoint: 000925
- to stream Main, to step Merge: 009A08
- to stream Main, to step Curation: 009397
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A Model-Based Completeness Proof of Extended Narrowing and Resolution</title><author><name sortKey="Stuber, Jurgen" sort="Stuber, Jurgen" uniqKey="Stuber J" first="Jürgen" last="Stuber">Jürgen Stuber</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/3-540-45744-5_15</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-0496HD24-7/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003966</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003966</idno><idno type="wicri:Area/Istex/Curation">003922</idno><idno type="wicri:Area/Istex/Checkpoint">001F39</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001F39</idno><idno type="wicri:doubleKey">0302-9743:2001:Stuber J:a:model:based</idno><idno type="wicri:Area/Main/Merge">009919</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:01-0367139</idno><idno type="wicri:Area/PascalFrancis/Corpus">000942</idno><idno type="wicri:Area/PascalFrancis/Curation">000134</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000925</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000925</idno><idno type="wicri:doubleKey">0302-9743:2001:Stuber J:a:model:based</idno><idno type="wicri:Area/Main/Merge">009A08</idno><idno type="wicri:Area/Main/Curation">009397</idno><idno type="wicri:Area/Main/Exploration">009397</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A Model-Based Completeness Proof of Extended Narrowing and Resolution</title><author><name sortKey="Stuber, Jurgen" sort="Stuber, Jurgen" uniqKey="Stuber J" first="Jürgen" last="Stuber">Jürgen Stuber</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>INRIA LORIA, 615 Rue Jardin Botanique, 54600, Villers-les-Nancy</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Villers-les-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><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><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Completeness</term><term>Modeling</term><term>Ordering</term><term>Set theory</term><term>Theorem proving</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Complétude</term><term>Démonstration théorème</term><term>Modélisation</term><term>Relation ordre</term><term>Théorie ensemble</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We give a proof of refutational completeness for Extended Narrowing And Resolution (ENAR), a calculus introduced by Dowek, Hardin and Kirchner in the context of Theorem Proving Modulo. ENAR integrates narrowing with respect to a set of rewrite rules on propositions into automated first-order theorem proving by resolution. Our proof allows to impose ordering restrictions on ENAR and provides general redundancy criteria, which are crucial for finding nontrivial proofs. On the other hand, it requires confluence and termination of the rewrite system, and in addition the existence of a well-founded ordering on propositions that is compatible with rewriting, compatible with ground inferences, total on ground clauses, and has some additional technical properties. Such orderings exist for hierarchical definitions of predicates. As an example we provide such an ordering for a fragment of set theory.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Villers-les-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Stuber, Jurgen" sort="Stuber, Jurgen" uniqKey="Stuber J" first="Jürgen" last="Stuber">Jürgen Stuber</name></region><name sortKey="Stuber, Jurgen" sort="Stuber, Jurgen" uniqKey="Stuber J" first="Jürgen" last="Stuber">Jürgen Stuber</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 009397 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009397 | 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:F09656DA0E36C03C6A4BFC8804B6E4D3F19C3A36
|texte= A Model-Based Completeness Proof of Extended Narrowing and Resolution
}}
| This area was generated with Dilib version V0.6.33. |  |