Automated proofs of the moufang identities in alternative rings
Identifieur interne : 00DE52 ( Main/Exploration ); précédent : 00DE51; suivant : 00DE53Automated proofs of the moufang identities in alternative rings
Auteurs : Siva Anantharaman [France] ; Jieh Hsiang [République populaire de Chine, États-Unis]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 1990-03-01.
English descriptors
- KwdEn :
- Teeft :
- Alternative ring, Alternative rings, Anantharaman, Auxiliary functions, Cancellation, Cancellation inferences, Cancellation laws, Critical pair, Critical pairs, Equational, Equational theorem, Final step, Hand side, Ineqn, Inequality, Inference mechanism, Input equations, Moufang, Moufang identities, Moufang identity, Orientable, Orientable instance, Prover, Right cancellable, Right hand side, Right hand sides, Right moufang identity, Runtime, Sbr2, Search mechanism, Search space, Simplification, Simplification steps, Siva, Siva anantharaman, Subterm, Superposing, Superposition, Symbolic computation, Term structure, Unfailing completion.
Abstract
Abstract: In this paper we present automatic proofs of the Moufang identities in alternative rings. Our approach is based on the term rewriting (Knuth-Bendix completion) method, enforced with various features. Our proofs seem to be the first computer proofs of these problems done by a general purpose theorem prover. We also present a direct proof of a certain property of alternative rings without employing any auxiliary functions. To our knowledge our computer proof seems to be the first direct proof of this property, by human or by a computer.
Url:
DOI: 10.1007/BF00302643
Affiliations:
- France, République populaire de Chine, États-Unis
- Centre-Val de Loire, Région Centre
- Orléans
- Université d'Orléans
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000058
- to stream Istex, to step Curation: 000058
- to stream Istex, to step Checkpoint: 003258
- to stream Main, to step Merge: 00E732
- to stream Main, to step Curation: 00DE52
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Automated proofs of the moufang identities in alternative rings</title><author><name sortKey="Anantharaman, Siva" sort="Anantharaman, Siva" uniqKey="Anantharaman S" first="Siva" last="Anantharaman">Siva Anantharaman</name></author><author><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:02AEEAB2FC67FDA70AC4DE7925723D4B329FC699</idno><date when="1990" year="1990">1990</date><idno type="doi">10.1007/BF00302643</idno><idno type="url">https://api.istex.fr/ark:/67375/1BB-9CGT8Z13-J/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000058</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000058</idno><idno type="wicri:Area/Istex/Curation">000058</idno><idno type="wicri:Area/Istex/Checkpoint">003258</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003258</idno><idno type="wicri:doubleKey">0168-7433:1990:Anantharaman S:automated:proofs:of</idno><idno type="wicri:Area/Main/Merge">00E732</idno><idno type="wicri:Area/Main/Curation">00DE52</idno><idno type="wicri:Area/Main/Exploration">00DE52</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Automated proofs of the moufang identities in alternative rings</title><author><name sortKey="Anantharaman, Siva" sort="Anantharaman, Siva" uniqKey="Anantharaman S" first="Siva" last="Anantharaman">Siva Anantharaman</name><affiliation wicri:level="4"><country xml:lang="fr">France</country><wicri:regionArea>LIFO, Dépt. Math-Info., Université d'Orléans, 45067, Orléans Cedex 02</wicri:regionArea><placeName><region type="region" nuts="2">Centre-Val de Loire</region><region type="old region" nuts="2">Région Centre</region><settlement type="city">Orléans</settlement></placeName><orgName type="university">Université d'Orléans</orgName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name><affiliation wicri:level="1"><country xml:lang="fr">République populaire de Chine</country><wicri:regionArea>Department of Computer Science, National Taiwan University, Taipei, Taiwan</wicri:regionArea><wicri:noRegion>Taiwan</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom 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="1990-03-01">1990-03-01</date><biblScope unit="volume">6</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="79">79</biblScope><biblScope unit="page" to="109">109</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>Automated theorem proving</term><term>Knuth-Bendix completion</term><term>Moufang identities</term><term>alternative rings</term><term>equational logic</term><term>term rewriting</term></keywords><keywords scheme="Teeft" xml:lang="en"><term>Alternative ring</term><term>Alternative rings</term><term>Anantharaman</term><term>Auxiliary functions</term><term>Cancellation</term><term>Cancellation inferences</term><term>Cancellation laws</term><term>Critical pair</term><term>Critical pairs</term><term>Equational</term><term>Equational theorem</term><term>Final step</term><term>Hand side</term><term>Ineqn</term><term>Inequality</term><term>Inference mechanism</term><term>Input equations</term><term>Moufang</term><term>Moufang identities</term><term>Moufang identity</term><term>Orientable</term><term>Orientable instance</term><term>Prover</term><term>Right cancellable</term><term>Right hand side</term><term>Right hand sides</term><term>Right moufang identity</term><term>Runtime</term><term>Sbr2</term><term>Search mechanism</term><term>Search space</term><term>Simplification</term><term>Simplification steps</term><term>Siva</term><term>Siva anantharaman</term><term>Subterm</term><term>Superposing</term><term>Superposition</term><term>Symbolic computation</term><term>Term structure</term><term>Unfailing completion</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this paper we present automatic proofs of the Moufang identities in alternative rings. Our approach is based on the term rewriting (Knuth-Bendix completion) method, enforced with various features. Our proofs seem to be the first computer proofs of these problems done by a general purpose theorem prover. We also present a direct proof of a certain property of alternative rings without employing any auxiliary functions. To our knowledge our computer proof seems to be the first direct proof of this property, by human or by a computer.</div></front></TEI><affiliations><list><country><li>France</li><li>République populaire de Chine</li><li>États-Unis</li></country><region><li>Centre-Val de Loire</li><li>Région Centre</li></region><settlement><li>Orléans</li></settlement><orgName><li>Université d'Orléans</li></orgName></list><tree><country name="France"><region name="Centre-Val de Loire"><name sortKey="Anantharaman, Siva" sort="Anantharaman, Siva" uniqKey="Anantharaman S" first="Siva" last="Anantharaman">Siva Anantharaman</name></region><name sortKey="Anantharaman, Siva" sort="Anantharaman, Siva" uniqKey="Anantharaman S" first="Siva" last="Anantharaman">Siva Anantharaman</name></country><country name="République populaire de Chine"><noRegion><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name></noRegion></country><country name="États-Unis"><noRegion><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name></noRegion></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 00DE52 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00DE52 | 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:02AEEAB2FC67FDA70AC4DE7925723D4B329FC699
|texte= Automated proofs of the moufang identities in alternative rings
}}
| This area was generated with Dilib version V0.6.33. |  |