Completion Is an Instance of Abstract Canonical System Inference
Identifieur interne : 005808 ( Main/Merge ); précédent : 005807; suivant : 005809Completion Is an Instance of Abstract Canonical System Inference
Auteurs : Guillaume Burel [France] ; Claude Kirchner [France]Source :
- Lecture notes in computer science [ 0302-9743 ] ; 2006.
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process. By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: 000332
- to stream PascalFrancis, to step Curation: 000693
- to stream PascalFrancis, to step Checkpoint: 000403
Links to Exploration step
Pascal:08-0088329Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Completion Is an Instance of Abstract Canonical System Inference</title><author><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Ecole Normale Supérieure de Lyon & LORIA</s1><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>Ecole Normale Supérieure de Lyon & LORIA</wicri:noRegion><wicri:noRegion>Ecole Normale Supérieure de Lyon & LORIA</wicri:noRegion></affiliation></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>INRIA & LORIA</s1><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>INRIA & LORIA</wicri:noRegion><wicri:noRegion>INRIA & LORIA</wicri:noRegion></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">INIST</idno><idno type="inist">08-0088329</idno><date when="2006">2006</date><idno type="stanalyst">PASCAL 08-0088329 INIST</idno><idno type="RBID">Pascal:08-0088329</idno><idno type="wicri:Area/PascalFrancis/Corpus">000332</idno><idno type="wicri:Area/PascalFrancis/Curation">000693</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000403</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000403</idno><idno type="wicri:doubleKey">0302-9743:2006:Burel G:completion:is:an</idno><idno type="wicri:Area/Main/Merge">005808</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Completion Is an Instance of Abstract Canonical System Inference</title><author><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name><affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Ecole Normale Supérieure de Lyon & LORIA</s1><s3>FRA</s3><sZ>1 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>Ecole Normale Supérieure de Lyon & LORIA</wicri:noRegion><wicri:noRegion>Ecole Normale Supérieure de Lyon & LORIA</wicri:noRegion></affiliation></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>INRIA & LORIA</s1><s3>FRA</s3><sZ>2 aut.</sZ></inist:fA14><country>France</country><wicri:noRegion>INRIA & LORIA</wicri:noRegion><wicri:noRegion>INRIA & LORIA</wicri:noRegion></affiliation></author></analytic><series><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno><imprint><date when="2006">2006</date></imprint></series></biblStruct></sourceDesc><seriesStmt><title level="j" type="main">Lecture notes in computer science</title><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Algebraic logic</term><term>Completeness</term><term>First order logic</term><term>Inference</term><term>Knuth Bendix</term><term>Ordering</term><term>Replacement</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Logique algébrique</term><term>Inférence</term><term>Logique ordre 1</term><term>Relation ordre</term><term>Remplacement</term><term>Complétude</term><term>Knuth Bendix</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract canonical systems and inference (ACSI) were introduced to formalize the intuitive notions of good proof and good inference appearing typically in first-order logic or in Knuth-Bendix like completion procedures. Since this abstract framework is intended to be generic, it is of fundamental interest to show its adequacy to represent the main systems of interest. This has been done for ground completion (where all equational axioms are ground) but was still an open question for the general completion process. By showing that the standard completion is an instance of the ACSI framework we close the question. For this purpose, two proof representations, proof terms and proofs by replacement, are compared to built a proof ordering that provides an instantiation adapted to the abstract canonical system framework.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Burel, Guillaume" sort="Burel, Guillaume" uniqKey="Burel G" first="Guillaume" last="Burel">Guillaume Burel</name></noRegion><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></country></tree></affiliations></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 005808 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005808 | 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é= Pascal:08-0088329
|texte= Completion Is an Instance of Abstract Canonical System Inference
}}
| This area was generated with Dilib version V0.6.33. |  |