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": "2022-01-01T18:04", 
        "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
        "sdPublisher": {
          "name": "Springer Nature - SN SciGraph project", 
          "type": "Organization"
        }, 
        "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/article/article_204.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 N89e4a090e09d49c9a14775afd73ab87d
    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 Nb527275acdf64bbc9ad31847740faf8e
    15 Nd7543d101d7b495eb3fe92838426b335
    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 N1c34187699214b848858f18840f0b906
    39 N68fe9b19247d4eaa88ba96c4e3cd8aae
    40 schema:sameAs https://app.dimensions.ai/details/publication/pub.1032603112
    41 https://doi.org/10.1007/bf00243209
    42 schema:sdDatePublished 2022-01-01T18:04
    43 schema:sdLicense https://scigraph.springernature.com/explorer/license/
    44 schema:sdPublisher N9868f40c78f7467b9017c10dc48e3809
    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 N1c34187699214b848858f18840f0b906 schema:name dimensions_id
    50 schema:value pub.1032603112
    51 rdf:type schema:PropertyValue
    52 N68fe9b19247d4eaa88ba96c4e3cd8aae schema:name doi
    53 schema:value 10.1007/bf00243209
    54 rdf:type schema:PropertyValue
    55 N89e4a090e09d49c9a14775afd73ab87d rdf:first sg:person.0707416220.12
    56 rdf:rest rdf:nil
    57 N9868f40c78f7467b9017c10dc48e3809 schema:name Springer Nature - SN SciGraph project
    58 rdf:type schema:Organization
    59 Nb527275acdf64bbc9ad31847740faf8e schema:volumeNumber 3
    60 rdf:type schema:PublicationVolume
    61 Nd7543d101d7b495eb3fe92838426b335 schema:issueNumber 2
    62 rdf:type schema:PublicationIssue
    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)


    ...