Some experiments in nonassociative ring theory with an automated theorem prover View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1987-06

AUTHORS

Rick L. Stevens

ABSTRACT

This paper presents some experiments using an automated theorem proving program (ATP) to prove theorems in nonassociative ring theory of varying difficulty. Several simple theorems proved by the program are discussed and other more difficult theorems that have been attempted are presented with some commentary as to why the program failed to find certain proofs. We also give some open problems that might be suitable for investigation with an ATP. More... »

PAGES

211-221

References to SciGraph publications

  • 1970. Paramodulation and set of support in SYMPOSIUM ON AUTOMATIC DEMONSTRATION
  • Identifiers

    URI

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

    DOI

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

    DIMENSIONS

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


    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/08", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Information and Computing Sciences", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/17", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Psychology and Cognitive Sciences", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Artificial Intelligence and Image Processing", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Computation Theory and Mathematics", 
            "type": "DefinedTerm"
          }, 
          {
            "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/1702", 
            "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
            "name": "Cognitive Sciences", 
            "type": "DefinedTerm"
          }
        ], 
        "author": [
          {
            "affiliation": {
              "alternateName": "Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL, USA", 
              "id": "http://www.grid.ac/institutes/grid.187073.a", 
              "name": [
                "Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL, USA"
              ], 
              "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"
          }
        ], 
        "citation": [
          {
            "id": "sg:pub.10.1007/bfb0060637", 
            "sameAs": [
              "https://app.dimensions.ai/details/publication/pub.1000583910", 
              "https://doi.org/10.1007/bfb0060637"
            ], 
            "type": "CreativeWork"
          }
        ], 
        "datePublished": "1987-06", 
        "datePublishedReg": "1987-06-01", 
        "description": "This paper presents some experiments using an automated theorem proving program (ATP) to prove theorems in nonassociative ring theory of varying difficulty. Several simple theorems proved by the program are discussed and other more difficult theorems that have been attempted are presented with some commentary as to why the program failed to find certain proofs. We also give some open problems that might be suitable for investigation with an ATP.", 
        "genre": "article", 
        "id": "sg:pub.10.1007/bf00243209", 
        "inLanguage": "en", 
        "isAccessibleForFree": false, 
        "isPartOf": [
          {
            "id": "sg:journal.1136522", 
            "issn": [
              "0168-7433", 
              "1573-0670"
            ], 
            "name": "Journal of Automated Reasoning", 
            "publisher": "Springer Nature", 
            "type": "Periodical"
          }, 
          {
            "issueNumber": "2", 
            "type": "PublicationIssue"
          }, 
          {
            "type": "PublicationVolume", 
            "volumeNumber": "3"
          }
        ], 
        "keywords": [
          "theorem proving programs", 
          "proving programs", 
          "open problem", 
          "difficult theorems", 
          "certain proofs", 
          "experiments", 
          "proof", 
          "program", 
          "simple theorem", 
          "theorem", 
          "difficulties", 
          "theory", 
          "ring theory", 
          "investigation", 
          "commentary", 
          "ATP", 
          "problem", 
          "paper", 
          "nonassociative ring theory"
        ], 
        "name": "Some experiments in nonassociative ring theory with an automated theorem prover", 
        "pagination": "211-221", 
        "productId": [
          {
            "name": "dimensions_id", 
            "type": "PropertyValue", 
            "value": [
              "pub.1032603112"
            ]
          }, 
          {
            "name": "doi", 
            "type": "PropertyValue", 
            "value": [
              "10.1007/bf00243209"
            ]
          }
        ], 
        "sameAs": [
          "https://doi.org/10.1007/bf00243209", 
          "https://app.dimensions.ai/details/publication/pub.1032603112"
        ], 
        "sdDataset": "articles", 
        "sdDatePublished": "2021-11-01T17:57", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20211101/entities/gbq_results/article/article_182.jsonl", 
        "type": "ScholarlyArticle", 
        "url": "https://doi.org/10.1007/bf00243209"
      }
    ]
     

    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/bf00243209'

    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/bf00243209'

    Turtle is a human-readable linked data format.

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

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

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


     

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

    93 TRIPLES      22 PREDICATES      49 URIs      37 LITERALS      6 BLANK NODES

    Subject Predicate Object
    1 sg:pub.10.1007/bf00243209 schema:about anzsrc-for:08
    2 anzsrc-for:0801
    3 anzsrc-for:0802
    4 anzsrc-for:17
    5 anzsrc-for:1702
    6 schema:author Nfed1d53ecf1e4ed583cb3ed01cf16483
    7 schema:citation sg:pub.10.1007/bfb0060637
    8 schema:datePublished 1987-06
    9 schema:datePublishedReg 1987-06-01
    10 schema:description This paper presents some experiments using an automated theorem proving program (ATP) to prove theorems in nonassociative ring theory of varying difficulty. Several simple theorems proved by the program are discussed and other more difficult theorems that have been attempted are presented with some commentary as to why the program failed to find certain proofs. We also give some open problems that might be suitable for investigation with an ATP.
    11 schema:genre article
    12 schema:inLanguage en
    13 schema:isAccessibleForFree false
    14 schema:isPartOf N3d831c2fd9cc426ba997da6d7bba4111
    15 Nfd37d570b02546079bcf2a26237fe509
    16 sg:journal.1136522
    17 schema:keywords ATP
    18 certain proofs
    19 commentary
    20 difficult theorems
    21 difficulties
    22 experiments
    23 investigation
    24 nonassociative ring theory
    25 open problem
    26 paper
    27 problem
    28 program
    29 proof
    30 proving programs
    31 ring theory
    32 simple theorem
    33 theorem
    34 theorem proving programs
    35 theory
    36 schema:name Some experiments in nonassociative ring theory with an automated theorem prover
    37 schema:pagination 211-221
    38 schema:productId N28499d84eade456889bda1e34664e8a5
    39 Nadce7e74b6ec42258147c5693df181cc
    40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032603112
    41 https://doi.org/10.1007/bf00243209
    42 schema:sdDatePublished 2021-11-01T17:57
    43 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    44 schema:sdPublisher Na4b2b2dba4bc42bcbded94015c2ee68b
    45 schema:url https://doi.org/10.1007/bf00243209
    46 sgo:license sg:explorer/license/
    47 sgo:sdDataset articles
    48 rdf:type schema:ScholarlyArticle
    49 N28499d84eade456889bda1e34664e8a5 schema:name doi
    50 schema:value 10.1007/bf00243209
    51 rdf:type schema:PropertyValue
    52 N3d831c2fd9cc426ba997da6d7bba4111 schema:volumeNumber 3
    53 rdf:type schema:PublicationVolume
    54 Na4b2b2dba4bc42bcbded94015c2ee68b schema:name Springer Nature - SN SciGraph project
    55 rdf:type schema:Organization
    56 Nadce7e74b6ec42258147c5693df181cc schema:name dimensions_id
    57 schema:value pub.1032603112
    58 rdf:type schema:PropertyValue
    59 Nfd37d570b02546079bcf2a26237fe509 schema:issueNumber 2
    60 rdf:type schema:PublicationIssue
    61 Nfed1d53ecf1e4ed583cb3ed01cf16483 rdf:first sg:person.0707416220.12
    62 rdf:rest rdf:nil
    63 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
    64 schema:name Information and Computing Sciences
    65 rdf:type schema:DefinedTerm
    66 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
    67 schema:name Artificial Intelligence and Image Processing
    68 rdf:type schema:DefinedTerm
    69 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
    70 schema:name Computation Theory and Mathematics
    71 rdf:type schema:DefinedTerm
    72 anzsrc-for:17 schema:inDefinedTermSet anzsrc-for:
    73 schema:name Psychology and Cognitive Sciences
    74 rdf:type schema:DefinedTerm
    75 anzsrc-for:1702 schema:inDefinedTermSet anzsrc-for:
    76 schema:name Cognitive Sciences
    77 rdf:type schema:DefinedTerm
    78 sg:journal.1136522 schema:issn 0168-7433
    79 1573-0670
    80 schema:name Journal of Automated Reasoning
    81 schema:publisher Springer Nature
    82 rdf:type schema:Periodical
    83 sg:person.0707416220.12 schema:affiliation grid-institutes:grid.187073.a
    84 schema:familyName Stevens
    85 schema:givenName Rick L.
    86 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0707416220.12
    87 rdf:type schema:Person
    88 sg:pub.10.1007/bfb0060637 schema:sameAs https://app.dimensions.ai/details/publication/pub.1000583910
    89 https://doi.org/10.1007/bfb0060637
    90 rdf:type schema:CreativeWork
    91 grid-institutes:grid.187073.a schema:alternateName Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL, USA
    92 schema:name Argonne National Laboratory, 9700 South Cass Avenue, 60439, Argonne, IL, USA
    93 rdf:type schema:Organization
     




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


    ...