Completion for multiple reduction orderings
Identifieur interne : 00C776 ( Main/Exploration ); précédent : 00C775; suivant : 00C777Completion for multiple reduction orderings
Auteurs : Masahito Kurihara [Japon] ; Hisashi Kondo [Japon] ; Azuma Ohuchi [Japon]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We present a completion procedure (called MKB) which works with 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 Kuuth-Bendix 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 structure 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 of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes 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.
Url:
DOI: 10.1007/3-540-59200-8_48
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000565
- to stream Istex, to step Curation: 000561
- to stream Istex, to step Checkpoint: 002B91
- to stream Main, to step Merge: 00D033
- to stream Main, to step Curation: 00C776
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><author><name sortKey="Ohuchi, Azuma" sort="Ohuchi, Azuma" uniqKey="Ohuchi A" first="Azuma" last="Ohuchi">Azuma Ohuchi</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:197B9AB55250430EA80D66CCF5A77337B0A3BC6D</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1007/3-540-59200-8_48</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-F56CR514-2/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000565</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000565</idno><idno type="wicri:Area/Istex/Curation">000561</idno><idno type="wicri:Area/Istex/Checkpoint">002B91</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002B91</idno><idno type="wicri:doubleKey">0302-9743:1995:Kurihara M:completion:for:multiple</idno><idno type="wicri:Area/Main/Merge">00D033</idno><idno type="wicri:Area/Main/Curation">00C776</idno><idno type="wicri:Area/Main/Exploration">00C776</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 Information Engineering, Hokkaido University, 060, Sapporo</wicri:regionArea><wicri:noRegion>Sapporo</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Japon</country></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 Systems Engineering, Ibaraki University, 316, Hitachi</wicri:regionArea><wicri:noRegion>Hitachi</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Japon</country></affiliation></author><author><name sortKey="Ohuchi, Azuma" sort="Ohuchi, Azuma" uniqKey="Ohuchi A" first="Azuma" last="Ohuchi">Azuma Ohuchi</name><affiliation wicri:level="1"><country xml:lang="fr">Japon</country><wicri:regionArea>Department of Information Engineering, Hokkaido University, 060, 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="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 present a completion procedure (called MKB) which works with 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 Kuuth-Bendix 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 structure 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 of the inferences made in the processes are closely related, so we can design inference rules that simulate multiple KB inferences in several processes 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.</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><name sortKey="Kurihara, Masahito" sort="Kurihara, Masahito" uniqKey="Kurihara M" first="Masahito" last="Kurihara">Masahito Kurihara</name><name sortKey="Ohuchi, Azuma" sort="Ohuchi, Azuma" uniqKey="Ohuchi A" first="Azuma" last="Ohuchi">Azuma Ohuchi</name><name sortKey="Ohuchi, Azuma" sort="Ohuchi, Azuma" uniqKey="Ohuchi A" first="Azuma" last="Ohuchi">Azuma Ohuchi</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 00C776 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00C776 | 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:197B9AB55250430EA80D66CCF5A77337B0A3BC6D
|texte= Completion for multiple reduction orderings
}}
| This area was generated with Dilib version V0.6.33. |  |