Automated reasoning contributes to mathematics and logic View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

1990

AUTHORS

L. Wos , S. Winker , W. McCune , R. Overbeek , E. Lusk , R. Stevens , R. Butler

ABSTRACT

In this article, we present some results of our research focusing on the use of our newest automated reasoning program OTTER to prove theorems from Robbins algebra, equivalential calculus, implicational calculus, combinatory logic, and finite semigroups. Included among the results are answers to open questions and new shorter and less complex proofs to known theorems. To obtain these results, we relied upon our usual paradigm, which heavily emphasizes the role of demodulation, subsumption, set of support, weighting, paramodulation, hyperresolution, and UR-resolution. Our position is that all of these components are essential, even though we can shed little light on the relative importance of each, the coupling of the various components, and the metarules for making the most effective choices. Indeed, without these components, a program will too often offer inadequate control over the redundancy and irrelevancy of deduced information. We include experimental evidence to support our position, examples producing success when the paradigm is employed, and examples producing failure when it is not. In addition to providing evidence that automated reasoning has made contributions to both mathematics and logic, the theorems we discuss also serve nicely as challenge problems for testing the merits of a new idea or a new program and provide interesting examples for comparing different paradigms. More... »

PAGES

485-499

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/3-540-52885-7_109

DOI

http://dx.doi.org/10.1007/3-540-52885-7_109

DIMENSIONS

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


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/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Wos", 
        "givenName": "L.", 
        "id": "sg:person.011307000351.36", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011307000351.36"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Winker", 
        "givenName": "S.", 
        "id": "sg:person.01224547554.09", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01224547554.09"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "McCune", 
        "givenName": "W.", 
        "id": "sg:person.014145037132.47", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014145037132.47"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Overbeek", 
        "givenName": "R.", 
        "id": "sg:person.01064013616.82", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01064013616.82"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Lusk", 
        "givenName": "E.", 
        "id": "sg:person.014177660636.93", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014177660636.93"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL", 
          "id": "http://www.grid.ac/institutes/grid.187073.a", 
          "name": [
            "Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Stevens", 
        "givenName": "R.", 
        "id": "sg:person.0707416220.12", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0707416220.12"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Division of Computer and Information Science, University of North Florida, 32216, Jacksonville, FL", 
          "id": "http://www.grid.ac/institutes/grid.266865.9", 
          "name": [
            "Division of Computer and Information Science, University of North Florida, 32216, Jacksonville, FL"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Butler", 
        "givenName": "R.", 
        "id": "sg:person.012533617424.53", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012533617424.53"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "1990", 
    "datePublishedReg": "1990-01-01", 
    "description": "In this article, we present some results of our research focusing on the use of our newest automated reasoning program OTTER to prove theorems from Robbins algebra, equivalential calculus, implicational calculus, combinatory logic, and finite semigroups. Included among the results are answers to open questions and new shorter and less complex proofs to known theorems. To obtain these results, we relied upon our usual paradigm, which heavily emphasizes the role of demodulation, subsumption, set of support, weighting, paramodulation, hyperresolution, and UR-resolution. Our position is that all of these components are essential, even though we can shed little light on the relative importance of each, the coupling of the various components, and the metarules for making the most effective choices. Indeed, without these components, a program will too often offer inadequate control over the redundancy and irrelevancy of deduced information. We include experimental evidence to support our position, examples producing success when the paradigm is employed, and examples producing failure when it is not. In addition to providing evidence that automated reasoning has made contributions to both mathematics and logic, the theorems we discuss also serve nicely as challenge problems for testing the merits of a new idea or a new program and provide interesting examples for comparing different paradigms.", 
    "editor": [
      {
        "familyName": "Stickel", 
        "givenName": "Mark E.", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/3-540-52885-7_109", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-3-540-52885-2", 
        "978-3-540-47171-4"
      ], 
      "name": "10th International Conference on Automated Deduction", 
      "type": "Book"
    }, 
    "keywords": [
      "UR-resolution", 
      "complex proofs", 
      "program OTTER", 
      "challenge problem", 
      "Robbins algebra", 
      "equivalential calculus", 
      "deduced information", 
      "logic", 
      "different paradigms", 
      "paradigm", 
      "set of supports", 
      "new ideas", 
      "usual paradigm", 
      "combinatory logic", 
      "metarules", 
      "subsumption", 
      "redundancy", 
      "reasoning", 
      "example", 
      "calculus", 
      "new program", 
      "effective choice", 
      "demodulation", 
      "information", 
      "set", 
      "paramodulation", 
      "mathematics", 
      "proof", 
      "irrelevancy", 
      "hyperresolution", 
      "weighting", 
      "idea", 
      "program", 
      "components", 
      "results", 
      "answers", 
      "theorem", 
      "support", 
      "position", 
      "merits", 
      "interesting example", 
      "algebra", 
      "research", 
      "use", 
      "success", 
      "control", 
      "choice", 
      "finite semigroups", 
      "contribution", 
      "article", 
      "questions", 
      "addition", 
      "importance", 
      "failure", 
      "relative importance", 
      "little light", 
      "experimental evidence", 
      "role", 
      "otters", 
      "coupling", 
      "light", 
      "contributes", 
      "inadequate control", 
      "semigroups", 
      "evidence", 
      "problem", 
      "implicational calculus", 
      "role of demodulation", 
      "reasoning contributes"
    ], 
    "name": "Automated reasoning contributes to mathematics and logic", 
    "pagination": "485-499", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1009874813"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/3-540-52885-7_109"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/3-540-52885-7_109", 
      "https://app.dimensions.ai/details/publication/pub.1009874813"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:09", 
    "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_404.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/3-540-52885-7_109"
  }
]
 

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/3-540-52885-7_109'

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/3-540-52885-7_109'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/3-540-52885-7_109'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/3-540-52885-7_109'


 

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

174 TRIPLES      23 PREDICATES      95 URIs      88 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/3-540-52885-7_109 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N79c1b55e8e9b4846b6e1162f977b29c1
4 schema:datePublished 1990
5 schema:datePublishedReg 1990-01-01
6 schema:description In this article, we present some results of our research focusing on the use of our newest automated reasoning program OTTER to prove theorems from Robbins algebra, equivalential calculus, implicational calculus, combinatory logic, and finite semigroups. Included among the results are answers to open questions and new shorter and less complex proofs to known theorems. To obtain these results, we relied upon our usual paradigm, which heavily emphasizes the role of demodulation, subsumption, set of support, weighting, paramodulation, hyperresolution, and UR-resolution. Our position is that all of these components are essential, even though we can shed little light on the relative importance of each, the coupling of the various components, and the metarules for making the most effective choices. Indeed, without these components, a program will too often offer inadequate control over the redundancy and irrelevancy of deduced information. We include experimental evidence to support our position, examples producing success when the paradigm is employed, and examples producing failure when it is not. In addition to providing evidence that automated reasoning has made contributions to both mathematics and logic, the theorems we discuss also serve nicely as challenge problems for testing the merits of a new idea or a new program and provide interesting examples for comparing different paradigms.
7 schema:editor N13cd40e3a61342e58e8eaf4e7580ca6a
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N1d69b02821c74f50bf4ad58cfafc83b4
12 schema:keywords Robbins algebra
13 UR-resolution
14 addition
15 algebra
16 answers
17 article
18 calculus
19 challenge problem
20 choice
21 combinatory logic
22 complex proofs
23 components
24 contributes
25 contribution
26 control
27 coupling
28 deduced information
29 demodulation
30 different paradigms
31 effective choice
32 equivalential calculus
33 evidence
34 example
35 experimental evidence
36 failure
37 finite semigroups
38 hyperresolution
39 idea
40 implicational calculus
41 importance
42 inadequate control
43 information
44 interesting example
45 irrelevancy
46 light
47 little light
48 logic
49 mathematics
50 merits
51 metarules
52 new ideas
53 new program
54 otters
55 paradigm
56 paramodulation
57 position
58 problem
59 program
60 program OTTER
61 proof
62 questions
63 reasoning
64 reasoning contributes
65 redundancy
66 relative importance
67 research
68 results
69 role
70 role of demodulation
71 semigroups
72 set
73 set of supports
74 subsumption
75 success
76 support
77 theorem
78 use
79 usual paradigm
80 weighting
81 schema:name Automated reasoning contributes to mathematics and logic
82 schema:pagination 485-499
83 schema:productId N159d7bc31c734d3796974313cd5933db
84 Nc51385f0df9b405896de74ac80fc9d86
85 schema:publisher N02ce85723a224051819cc9d0f5558e08
86 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009874813
87 https://doi.org/10.1007/3-540-52885-7_109
88 schema:sdDatePublished 2021-12-01T20:09
89 schema:sdLicense https://scigraph.springernature.com/explorer/license/
90 schema:sdPublisher N8602cfb815d0478a92f0e319b9610c8b
91 schema:url https://doi.org/10.1007/3-540-52885-7_109
92 sgo:license sg:explorer/license/
93 sgo:sdDataset chapters
94 rdf:type schema:Chapter
95 N02ce85723a224051819cc9d0f5558e08 schema:name Springer Nature
96 rdf:type schema:Organisation
97 N13cd40e3a61342e58e8eaf4e7580ca6a rdf:first N69d10df90333486c8017393908b15840
98 rdf:rest rdf:nil
99 N159d7bc31c734d3796974313cd5933db schema:name doi
100 schema:value 10.1007/3-540-52885-7_109
101 rdf:type schema:PropertyValue
102 N1d69b02821c74f50bf4ad58cfafc83b4 schema:isbn 978-3-540-47171-4
103 978-3-540-52885-2
104 schema:name 10th International Conference on Automated Deduction
105 rdf:type schema:Book
106 N573b8a8d03754084b81ebaaf80b50a7c rdf:first sg:person.01224547554.09
107 rdf:rest N8aae3765722b40bda85394421d67dcd5
108 N69d10df90333486c8017393908b15840 schema:familyName Stickel
109 schema:givenName Mark E.
110 rdf:type schema:Person
111 N79c1b55e8e9b4846b6e1162f977b29c1 rdf:first sg:person.011307000351.36
112 rdf:rest N573b8a8d03754084b81ebaaf80b50a7c
113 N7af0cc454c3b4c5b883e49b8a0ba3e4c rdf:first sg:person.01064013616.82
114 rdf:rest Nda10d789b0884613a7d5e59a99b86109
115 N8602cfb815d0478a92f0e319b9610c8b schema:name Springer Nature - SN SciGraph project
116 rdf:type schema:Organization
117 N8aae3765722b40bda85394421d67dcd5 rdf:first sg:person.014145037132.47
118 rdf:rest N7af0cc454c3b4c5b883e49b8a0ba3e4c
119 Nc51385f0df9b405896de74ac80fc9d86 schema:name dimensions_id
120 schema:value pub.1009874813
121 rdf:type schema:PropertyValue
122 Nda10d789b0884613a7d5e59a99b86109 rdf:first sg:person.014177660636.93
123 rdf:rest Nfc8aa42daeef4847b48a46b900b2e7c7
124 Nda8fe726d5d24d64adb23aad5b7126da rdf:first sg:person.012533617424.53
125 rdf:rest rdf:nil
126 Nfc8aa42daeef4847b48a46b900b2e7c7 rdf:first sg:person.0707416220.12
127 rdf:rest Nda8fe726d5d24d64adb23aad5b7126da
128 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
129 schema:name Information and Computing Sciences
130 rdf:type schema:DefinedTerm
131 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
132 schema:name Computation Theory and Mathematics
133 rdf:type schema:DefinedTerm
134 sg:person.01064013616.82 schema:affiliation grid-institutes:grid.187073.a
135 schema:familyName Overbeek
136 schema:givenName R.
137 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01064013616.82
138 rdf:type schema:Person
139 sg:person.011307000351.36 schema:affiliation grid-institutes:grid.187073.a
140 schema:familyName Wos
141 schema:givenName L.
142 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011307000351.36
143 rdf:type schema:Person
144 sg:person.01224547554.09 schema:affiliation grid-institutes:grid.187073.a
145 schema:familyName Winker
146 schema:givenName S.
147 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01224547554.09
148 rdf:type schema:Person
149 sg:person.012533617424.53 schema:affiliation grid-institutes:grid.266865.9
150 schema:familyName Butler
151 schema:givenName R.
152 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012533617424.53
153 rdf:type schema:Person
154 sg:person.014145037132.47 schema:affiliation grid-institutes:grid.187073.a
155 schema:familyName McCune
156 schema:givenName W.
157 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014145037132.47
158 rdf:type schema:Person
159 sg:person.014177660636.93 schema:affiliation grid-institutes:grid.187073.a
160 schema:familyName Lusk
161 schema:givenName E.
162 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014177660636.93
163 rdf:type schema:Person
164 sg:person.0707416220.12 schema:affiliation grid-institutes:grid.187073.a
165 schema:familyName Stevens
166 schema:givenName R.
167 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.0707416220.12
168 rdf:type schema:Person
169 grid-institutes:grid.187073.a schema:alternateName Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL
170 schema:name Mathematics and Computer Science Division, Argonne National Laboratory, 60439-4844, Argonne, IL
171 rdf:type schema:Organization
172 grid-institutes:grid.266865.9 schema:alternateName Division of Computer and Information Science, University of North Florida, 32216, Jacksonville, FL
173 schema:name Division of Computer and Information Science, University of North Florida, 32216, Jacksonville, FL
174 rdf:type schema:Organization
 




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


...