Completion for Multiple Reduction Orderings
Identifieur interne : 00AA30 ( Main/Exploration ); précédent : 00AA29; suivant : 00AA31Completion for Multiple Reduction Orderings
Auteurs : Masahito Kurihara [Japon] ; Hisashi Kondo [Japon]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 1999-07-01.
English descriptors
- KwdEn :
Abstract
Abstract: We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough. We also present an extension of this technique to the unfailing completion for multiple reduction orderings, which is useful in various areas of automated reasoning, including equational theorem proving.
Url:
DOI: 10.1023/A:1006129631807
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001573
- to stream Istex, to step Curation: 001555
- to stream Istex, to step Checkpoint: 002416
- to stream Main, to step Merge: 00B082
- to stream Main, to step Curation: 00AA30
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Completion for Multiple Reduction Orderings</title><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name></author><author><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5DAB26D298648FD1C6FFE57A9AF175C33E20A332</idno><date when="1999" year="1999">1999</date><idno type="doi">10.1023/A:1006129631807</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-NK57GPQD-K/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001573</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001573</idno><idno type="wicri:Area/Istex/Curation">001555</idno><idno type="wicri:Area/Istex/Checkpoint">002416</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002416</idno><idno type="wicri:doubleKey">0168-7433:1999:Kurihara M:completion:for:multiple</idno><idno type="wicri:Area/Main/Merge">00B082</idno><idno type="wicri:Area/Main/Curation">00AA30</idno><idno type="wicri:Area/Main/Exploration">00AA30</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Completion for Multiple Reduction Orderings</title><author><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><affiliation wicri:level="1"><country xml:lang="fr">Japon</country><wicri:regionArea>Department of Electrical Engineering, Hokkaido Institute of Technology, 006-8585, Sapporo</wicri:regionArea><wicri:noRegion>Sapporo</wicri:noRegion></affiliation></author><author><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name><affiliation wicri:level="1"><country xml:lang="fr">Japon</country><wicri:regionArea>Department of Electrical Engineering, Hokkaido Institute of Technology, 006-8585, Sapporo</wicri:regionArea><wicri:noRegion>Sapporo</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Japon</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="1999-07-01">1999-07-01</date><biblScope unit="volume">23</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="25">25</biblScope><biblScope unit="page" to="42">42</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>completion</term><term>equational reasoning</term><term>term rewriting</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s → t (or t → s) and which processes contain the equation s ↔ t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough. We also present an extension of this technique to the unfailing completion for multiple reduction orderings, which is useful in various areas of automated reasoning, including equational theorem proving.</div></front></TEI><affiliations><list><country><li>Japon</li></country></list><tree><country name="Japon"><noRegion><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name></noRegion><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</name><name sortKey="Kondo, Hisashi" sort="Kondo, Hisashi" uniqKey="Kondo H" first="Hisashi" last="Kondo">Hisashi Kondo</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 00AA30 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00AA30 | 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:5DAB26D298648FD1C6FFE57A9AF175C33E20A332
|texte= Completion for Multiple Reduction Orderings
}}
| This area was generated with Dilib version V0.6.33. |  |