Challenge problems from nonassociative rings for theorem provers View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

1988

AUTHORS

Rick L. Stevens

ABSTRACT

The Moufang Identities are proving to be a challenging set of problems for automated theorem proving programs. Aside from one program that uses a new technique that has the axioms of nonassociative ring theorem built in, I know of no other program able to prove these identities. In this short paper I include the axioms for nonassociative rings, statements of the five moufang identities, a natural hand proof of one of the left identities and a human guided paramodulation proof of the same identity. I hope that this paper will provide a starting point for others to attack these interesting problems. More... »

PAGES

730-734

Book

TITLE

9th International Conference on Automated Deduction

ISBN

3-540-19343-X

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/bfb0012871

DOI

http://dx.doi.org/10.1007/bfb0012871

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1009367670


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/21", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "History and Archaeology", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/2103", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Historical Studies", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Stevens", 
        "givenName": "Rick L.", 
        "id": "sg:person.0707416220.12", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0707416220.12"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "1988", 
    "datePublishedReg": "1988-01-01", 
    "description": "The Moufang Identities are proving to be a challenging set of problems for automated theorem proving programs. Aside from one program that uses a new technique that has the axioms of nonassociative ring theorem built in, I know of no other program able to prove these identities. In this short paper I include the axioms for nonassociative rings, statements of the five moufang identities, a natural hand proof of one of the left identities and a human guided paramodulation proof of the same identity. I hope that this paper will provide a starting point for others to attack these interesting problems.", 
    "editor": [
      {
        "familyName": "Lusk", 
        "givenName": "Ewing", 
        "type": "Person"
      }, 
      {
        "familyName": "Overbeek", 
        "givenName": "Ross", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/bfb0012871", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "3-540-19343-X"
      ], 
      "name": "9th International Conference on Automated Deduction", 
      "type": "Book"
    }, 
    "keywords": [
      "theorem proving programs", 
      "hand proofs", 
      "theorem provers", 
      "challenging set", 
      "proving programs", 
      "same identity", 
      "interesting problem", 
      "challenge problem", 
      "Moufang identities", 
      "provers", 
      "new technique", 
      "axioms", 
      "proof", 
      "set", 
      "program", 
      "technique", 
      "starting point", 
      "identity", 
      "short paper I", 
      "paper I", 
      "point", 
      "theorem", 
      "statements", 
      "problem", 
      "ring", 
      "paper", 
      "nonassociative ring theorem", 
      "ring theorem", 
      "nonassociative ring", 
      "natural hand proof", 
      "left identity", 
      "paramodulation proof"
    ], 
    "name": "Challenge problems from nonassociative rings for theorem provers", 
    "pagination": "730-734", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1009367670"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bfb0012871"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/bfb0012871", 
      "https://app.dimensions.ai/details/publication/pub.1009367670"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:03", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_259.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/bfb0012871"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/bfb0012871'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/bfb0012871'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/bfb0012871'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/bfb0012871'


 

This table displays all metadata directly associated to this object as RDF triples.

96 TRIPLES      23 PREDICATES      58 URIs      51 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bfb0012871 schema:about anzsrc-for:21
2 anzsrc-for:2103
3 schema:author N9a6a1b402ae04736b92779221e57a22b
4 schema:datePublished 1988
5 schema:datePublishedReg 1988-01-01
6 schema:description The Moufang Identities are proving to be a challenging set of problems for automated theorem proving programs. Aside from one program that uses a new technique that has the axioms of nonassociative ring theorem built in, I know of no other program able to prove these identities. In this short paper I include the axioms for nonassociative rings, statements of the five moufang identities, a natural hand proof of one of the left identities and a human guided paramodulation proof of the same identity. I hope that this paper will provide a starting point for others to attack these interesting problems.
7 schema:editor N5040ab30b4bf47e98bebaf030cedcf56
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N81fdcc3a792747229f33d33cc997e745
12 schema:keywords Moufang identities
13 axioms
14 challenge problem
15 challenging set
16 hand proofs
17 identity
18 interesting problem
19 left identity
20 natural hand proof
21 new technique
22 nonassociative ring
23 nonassociative ring theorem
24 paper
25 paper I
26 paramodulation proof
27 point
28 problem
29 program
30 proof
31 provers
32 proving programs
33 ring
34 ring theorem
35 same identity
36 set
37 short paper I
38 starting point
39 statements
40 technique
41 theorem
42 theorem provers
43 theorem proving programs
44 schema:name Challenge problems from nonassociative rings for theorem provers
45 schema:pagination 730-734
46 schema:productId N9fb8dc515d3e41d3ac0a919d48a2c015
47 Nf54dc096a6c94e43affacf5116c34a5f
48 schema:publisher N6c3d8de8566549f1900a5dd984baf020
49 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009367670
50 https://doi.org/10.1007/bfb0012871
51 schema:sdDatePublished 2021-12-01T20:03
52 schema:sdLicense https://scigraph.springernature.com/explorer/license/
53 schema:sdPublisher Ne90d46ed9e054b13863e2743c2b4ca1d
54 schema:url https://doi.org/10.1007/bfb0012871
55 sgo:license sg:explorer/license/
56 sgo:sdDataset chapters
57 rdf:type schema:Chapter
58 N290a7493ac824c5c803731bf2acbd0f3 rdf:first Nfd2dc2a08cba4d0da15ec32fe786a62d
59 rdf:rest rdf:nil
60 N3a00756bafa7413fae52df5b4d9ce782 schema:familyName Lusk
61 schema:givenName Ewing
62 rdf:type schema:Person
63 N5040ab30b4bf47e98bebaf030cedcf56 rdf:first N3a00756bafa7413fae52df5b4d9ce782
64 rdf:rest N290a7493ac824c5c803731bf2acbd0f3
65 N6c3d8de8566549f1900a5dd984baf020 schema:name Springer Nature
66 rdf:type schema:Organisation
67 N81fdcc3a792747229f33d33cc997e745 schema:isbn 3-540-19343-X
68 schema:name 9th International Conference on Automated Deduction
69 rdf:type schema:Book
70 N9a6a1b402ae04736b92779221e57a22b rdf:first sg:person.0707416220.12
71 rdf:rest rdf:nil
72 N9fb8dc515d3e41d3ac0a919d48a2c015 schema:name doi
73 schema:value 10.1007/bfb0012871
74 rdf:type schema:PropertyValue
75 Ne90d46ed9e054b13863e2743c2b4ca1d schema:name Springer Nature - SN SciGraph project
76 rdf:type schema:Organization
77 Nf54dc096a6c94e43affacf5116c34a5f schema:name dimensions_id
78 schema:value pub.1009367670
79 rdf:type schema:PropertyValue
80 Nfd2dc2a08cba4d0da15ec32fe786a62d schema:familyName Overbeek
81 schema:givenName Ross
82 rdf:type schema:Person
83 anzsrc-for:21 schema:inDefinedTermSet anzsrc-for:
84 schema:name History and Archaeology
85 rdf:type schema:DefinedTerm
86 anzsrc-for:2103 schema:inDefinedTermSet anzsrc-for:
87 schema:name Historical Studies
88 rdf:type schema:DefinedTerm
89 sg:person.0707416220.12 schema:affiliation grid-institutes:grid.187073.a
90 schema:familyName Stevens
91 schema:givenName Rick L.
92 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0707416220.12
93 rdf:type schema:Person
94 grid-institutes:grid.187073.a schema:alternateName Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL
95 schema:name Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL
96 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...