Automated proofs of the moufang identities in alternative rings
Identifieur interne : 000058 ( Istex/Corpus ); précédent : 000057; suivant : 000059Automated proofs of the moufang identities in alternative rings
Auteurs : Siva Anantharaman ; Jieh HsiangSource :
- 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 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><affiliation><mods:affiliation>LIFO, Dépt. Math-Info., Université d'Orléans, 45067, Orléans Cedex 02, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: siva@univ-orleans.fr</mods:affiliation></affiliation></author><author><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name><affiliation><mods:affiliation>Department of Computer Science, National Taiwan University, Taipei, Taiwan, Republic of China</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: hsiang@sbcs.sunysb.edu</mods:affiliation></affiliation></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></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><mods:affiliation>LIFO, Dépt. Math-Info., Université d'Orléans, 45067, Orléans Cedex 02, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: siva@univ-orleans.fr</mods:affiliation></affiliation></author><author><name sortKey="Hsiang, Jieh" sort="Hsiang, Jieh" uniqKey="Hsiang J" first="Jieh" last="Hsiang">Jieh Hsiang</name><affiliation><mods:affiliation>Department of Computer Science, National Taiwan University, Taipei, Taiwan, Republic of China</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: hsiang@sbcs.sunysb.edu</mods:affiliation></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><istex><corpusName>springer-journals</corpusName><keywords><teeft><json:string>moufang</json:string><json:string>critical pair</json:string><json:string>simplification</json:string><json:string>moufang identities</json:string><json:string>ineqn</json:string><json:string>superposing</json:string><json:string>orientable</json:string><json:string>sbr2</json:string><json:string>critical pairs</json:string><json:string>anantharaman</json:string><json:string>orientable instance</json:string><json:string>prover</json:string><json:string>inequality</json:string><json:string>subterm</json:string><json:string>equational</json:string><json:string>siva</json:string><json:string>siva anantharaman</json:string><json:string>right hand side</json:string><json:string>runtime</json:string><json:string>alternative rings</json:string><json:string>hand side</json:string><json:string>inference mechanism</json:string><json:string>unfailing completion</json:string><json:string>cancellation</json:string><json:string>superposition</json:string><json:string>moufang identity</json:string><json:string>simplification steps</json:string><json:string>search space</json:string><json:string>alternative ring</json:string><json:string>symbolic computation</json:string><json:string>cancellation inferences</json:string><json:string>right hand sides</json:string><json:string>final step</json:string><json:string>cancellation laws</json:string><json:string>right moufang identity</json:string><json:string>right cancellable</json:string><json:string>search mechanism</json:string><json:string>term structure</json:string><json:string>input equations</json:string><json:string>auxiliary functions</json:string><json:string>equational theorem</json:string></teeft></keywords><author><json:item><name>Siva Anantharaman</name><affiliations><json:string>LIFO, Dépt. Math-Info., Université d'Orléans, 45067, Orléans Cedex 02, France</json:string><json:string>E-mail: siva@univ-orleans.fr</json:string></affiliations></json:item><json:item><name>Jieh Hsiang</name><affiliations><json:string>Department of Computer Science, National Taiwan University, Taipei, Taiwan, Republic of China</json:string><json:string>E-mail: hsiang@sbcs.sunysb.edu</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Automated theorem proving</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>equational logic</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Knuth-Bendix completion</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>term rewriting</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Moufang identities</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>alternative rings</value></json:item></subject><articleId><json:string>BF00302643</json:string><json:string>Art5</json:string></articleId><arkIstex>ark:/67375/1BB-9CGT8Z13-J</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><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.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>89</abstractWordCount><abstractCharCount>550</abstractCharCount><keywordCount>6</keywordCount><score>8.068</score><pdfWordCount>13835</pdfWordCount><pdfCharCount>48138</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>31</pdfPageCount><pdfPageSize>453.28 x 684 pts</pdfPageSize></qualityIndicators><title>Automated proofs of the moufang identities in alternative rings</title><genre><json:string>research-article</json:string></genre><host><title>Journal of Automated Reasoning</title><language><json:string>unknown</json:string></language><publicationDate>1990</publicationDate><copyrightDate>1990</copyrightDate><issn><json:string>0168-7433</json:string></issn><eissn><json:string>1573-0670</json:string></eissn><journalId><json:string>10817</json:string></journalId><volume>6</volume><issue>1</issue><pages><first>79</first><last>109</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Logic</value></json:item><json:item><value>Symbolic and Algebraic Manipulation</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Foundations</value></json:item></subject></host><namedEntities><unitex><date></date><geogName></geogName><orgName></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName></persName><placeName></placeName><ref_url></ref_url><ref_bibl></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/1BB-9CGT8Z13-J</json:string></ark><categories><wos><json:string>1 - science</json:string><json:string>2 - computer science, artificial intelligence</json:string></wos><scienceMetrix><json:string>1 - applied sciences</json:string><json:string>2 - information & communication technologies</json:string><json:string>3 - computation theory & mathematics</json:string></scienceMetrix><scopus><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Artificial Intelligence</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Computational Theory and Mathematics</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - Software</json:string></scopus><inist><json:string>1 - sciences appliquees, technologies et medecines</json:string><json:string>2 - sciences exactes et technologie</json:string><json:string>3 - sciences et techniques communes</json:string><json:string>4 - mathematiques</json:string></inist></categories><publicationDate>1990</publicationDate><copyrightDate>1990</copyrightDate><doi><json:string>10.1007/BF00302643</json:string></doi><id>02AEEAB2FC67FDA70AC4DE7925723D4B329FC699</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-9CGT8Z13-J/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-9CGT8Z13-J/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/1BB-9CGT8Z13-J/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Automated proofs of the moufang identities in alternative rings</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><availability><licence><p>Kluwer Academic Publishers, 1990</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>1989-11-21</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note><note>Problem Corner</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Automated proofs of the moufang identities in alternative rings</title><author xml:id="author-0000"><persName><forename type="first">Siva</forename><surname>Anantharaman</surname></persName><email>siva@univ-orleans.fr</email><affiliation>LIFO, Dépt. Math-Info., Université d'Orléans, 45067, Orléans Cedex 02, France</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Jieh</forename><surname>Hsiang</surname></persName><email>hsiang@sbcs.sunysb.edu</email><affiliation>Department of Computer Science, National Taiwan University, Taipei, Taiwan, Republic of China</affiliation></author><idno type="istex">02AEEAB2FC67FDA70AC4DE7925723D4B329FC699</idno><idno type="ark">ark:/67375/1BB-9CGT8Z13-J</idno><idno type="DOI">10.1007/BF00302643</idno><idno type="article-id">BF00302643</idno><idno type="article-id">Art5</idno></analytic><monogr><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">J Autom Reasoning</title><idno type="pISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">5</idno><idno type="volume-issue-count">4</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="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></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1989-11-21</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>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.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><head>Key words</head><item><term>Automated theorem proving</term></item><item><term>equational logic</term></item><item><term>Knuth-Bendix completion</term></item><item><term>term rewriting</term></item><item><term>Moufang identities</term></item><item><term>alternative rings</term></item></list></keywords></textClass><textClass><keywords scheme="Journal Subject"><list><head>Philosophy</head><item><term>Logic</term></item><item><term>Symbolic and Algebraic Manipulation</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item><item><term>Mathematical Logic and Foundations</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="1989-11-21">Created</change><change when="1990-03-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-9CGT8Z13-J/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Kluwer Academic Publishers</PublisherName><PublisherLocation>Dordrecht</PublisherLocation></PublisherInfo><Journal><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="Unnumbered"><JournalID>10817</JournalID><JournalPrintISSN>0168-7433</JournalPrintISSN><JournalElectronicISSN>1573-0670</JournalElectronicISSN><JournalTitle>Journal of Automated Reasoning</JournalTitle><JournalAbbreviatedTitle>J Autom Reasoning</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Philosophy</JournalSubject><JournalSubject Type="Secondary">Logic</JournalSubject><JournalSubject Type="Secondary">Symbolic and Algebraic Manipulation</JournalSubject><JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject><JournalSubject Type="Secondary">Mathematical Logic and Foundations</JournalSubject></JournalSubjectGroup></JournalInfo><Volume><VolumeInfo VolumeType="Regular" TocLevels="0"><VolumeIDStart>6</VolumeIDStart><VolumeIDEnd>6</VolumeIDEnd><VolumeIssueCount>4</VolumeIssueCount></VolumeInfo><Issue IssueType="Regular"><IssueInfo TocLevels="0"><IssueIDStart>1</IssueIDStart><IssueIDEnd>1</IssueIDEnd><IssueArticleCount>5</IssueArticleCount><IssueHistory><CoverDate><Year>1990</Year><Month>3</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>1990</CopyrightYear></IssueCopyright></IssueInfo><Article ID="Art5"><ArticleInfo Language="En" ArticleType="OriginalPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ArticleID>BF00302643</ArticleID><ArticleDOI>10.1007/BF00302643</ArticleDOI><ArticleSequenceNumber>5</ArticleSequenceNumber><ArticleTitle Language="En">Automated proofs of the moufang identities in alternative rings</ArticleTitle><ArticleCategory>Problem Corner</ArticleCategory><ArticleFirstPage>79</ArticleFirstPage><ArticleLastPage>109</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2004</Year><Month>8</Month><Day>3</Day></RegistrationDate><Received><Year>1989</Year><Month>11</Month><Day>21</Day></Received></ArticleHistory><ArticleCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>1990</CopyrightYear></ArticleCopyright><ArticleGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ArticleGrants><ArticleContext><JournalID>10817</JournalID><VolumeIDStart>6</VolumeIDStart><VolumeIDEnd>6</VolumeIDEnd><IssueIDStart>1</IssueIDStart><IssueIDEnd>1</IssueIDEnd></ArticleContext></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Siva</GivenName><FamilyName>Anantharaman</FamilyName></AuthorName><Contact><Email>siva@univ-orleans.fr</Email></Contact></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Jieh</GivenName><FamilyName>Hsiang</FamilyName></AuthorName><Contact><Email>hsiang@sbcs.sunysb.edu</Email></Contact></Author><Affiliation ID="Aff1"><OrgDivision>LIFO, Dépt. Math-Info.</OrgDivision><OrgName>Université d'Orléans</OrgName><OrgAddress><Postcode>45067</Postcode><City>Orléans Cedex 02</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>National Taiwan University</OrgName><OrgAddress><City>Taipei, Taiwan</City><Country>Republic of China</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>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 <Emphasis Type="Italic">direct</Emphasis> 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.</Para></Abstract><KeywordGroup Language="En"><Heading>Key words</Heading><Keyword>Automated theorem proving</Keyword><Keyword>equational logic</Keyword><Keyword>Knuth-Bendix completion</Keyword><Keyword>term rewriting</Keyword><Keyword>Moufang identities</Keyword><Keyword>alternative rings</Keyword></KeywordGroup><ArticleNote Type="Misc"><SimplePara>On leave from the Department of Computer Science, UNYY at Stony Brook, New York. Research supported in part by NSF grants CCR-8805734, INT-8715231, and CCR-8901322.</SimplePara></ArticleNote></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Automated proofs of the moufang identities in alternative rings</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Automated proofs of the moufang identities in alternative rings</title></titleInfo><name type="personal"><namePart type="given">Siva</namePart><namePart type="family">Anantharaman</namePart><affiliation>LIFO, Dépt. Math-Info., Université d'Orléans, 45067, Orléans Cedex 02, France</affiliation><affiliation>E-mail: siva@univ-orleans.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Jieh</namePart><namePart type="family">Hsiang</namePart><affiliation>Department of Computer Science, National Taiwan University, Taipei, Taiwan, Republic of China</affiliation><affiliation>E-mail: hsiang@sbcs.sunysb.edu</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>Kluwer Academic Publishers</publisher><place><placeTerm type="text">Dordrecht</placeTerm></place><dateCreated encoding="w3cdtf">1989-11-21</dateCreated><dateIssued encoding="w3cdtf">1990-03-01</dateIssued><copyrightDate encoding="w3cdtf">1990</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract 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.</abstract><note>Problem Corner</note><subject lang="en"><genre>Key words</genre><topic>Automated theorem proving</topic><topic>equational logic</topic><topic>Knuth-Bendix completion</topic><topic>term rewriting</topic><topic>Moufang identities</topic><topic>alternative rings</topic></subject><relatedItem type="host"><titleInfo><title>Journal of Automated Reasoning</title></titleInfo><titleInfo type="abbreviated"><title>J Autom Reasoning</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">1990-03-01</dateIssued><copyrightDate encoding="w3cdtf">1990</copyrightDate></originInfo><subject><genre>Philosophy</genre><topic>Logic</topic><topic>Symbolic and Algebraic Manipulation</topic><topic>Artificial Intelligence (incl. Robotics)</topic><topic>Mathematical Logic and Foundations</topic></subject><identifier type="ISSN">0168-7433</identifier><identifier type="eISSN">1573-0670</identifier><identifier type="JournalID">10817</identifier><identifier type="IssueArticleCount">5</identifier><identifier type="VolumeIssueCount">4</identifier><part><date>1990</date><detail type="volume"><number>6</number><caption>vol.</caption></detail><detail type="issue"><number>1</number><caption>no.</caption></detail><extent unit="pages"><start>79</start><end>109</end></extent></part><recordInfo><recordOrigin>Kluwer Academic Publishers, 1990</recordOrigin></recordInfo></relatedItem><identifier type="istex">02AEEAB2FC67FDA70AC4DE7925723D4B329FC699</identifier><identifier type="ark">ark:/67375/1BB-9CGT8Z13-J</identifier><identifier type="DOI">10.1007/BF00302643</identifier><identifier type="ArticleID">BF00302643</identifier><identifier type="ArticleID">Art5</identifier><accessCondition type="use and reproduction" contentType="copyright">Kluwer Academic Publishers, 1990</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>Kluwer Academic Publishers, 1990</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/1BB-9CGT8Z13-J/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000058 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000058 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|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. |  |