Automated proofs of the moufang identities in alternative rings
Identifieur interne : 00DE52 ( Main/Curation ); 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
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000058
- to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :000058
- to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :003258
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00E732
Links to Exploration step
ISTEX:02AEEAB2FC67FDA70AC4DE7925723D4B329FC699Le 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>
</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>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00DE52 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/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= Curation |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. | ![]() |