An average case analysis of a resolution principle algorithm in mechanical theorem proving View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

1992-03

AUTHORS

T. H. Hu, C. Y. Tang, R. C. T. Lee

ABSTRACT

The satisfiability problem is a well known NP-complete problem. In artificial intelligence, solving the satisfiability problem is called mechanical theorem proving. One of those mechanical theorem proving methods is the resolution principle which was invented by J.R. Robinson. In this paper, we shall show how an algorithm based upon the resolution principle can be analyzed. Letn andr0 denote the numbers of variables and input clauses respectively. LetP0 denote the probability that a variable appears positively, or negatively, in a clause. Our analysis shows that the expected total number of clauses processed by our algorithm isO(n+r0) ifP0 is a constant,r0 is polynomially related withn, andn is large. More... »

PAGES

235-251

References to SciGraph publications

Identifiers

URI

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

DOI

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

DIMENSIONS

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


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/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/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "National Tsing Hua University", 
          "id": "https://www.grid.ac/institutes/grid.38348.34", 
          "name": [
            "Institute of Computer Science, National Tsing Hua University, 30043, Hsinchu, Taiwan, Republic of China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Hu", 
        "givenName": "T. H.", 
        "id": "sg:person.010634245333.21", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010634245333.21"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "National Tsing Hua University", 
          "id": "https://www.grid.ac/institutes/grid.38348.34", 
          "name": [
            "Institute of Computer Science, National Tsing Hua University, 30043, Hsinchu, Taiwan, Republic of China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Tang", 
        "givenName": "C. Y.", 
        "id": "sg:person.01312526135.27", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01312526135.27"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Academia Sinica", 
          "id": "https://www.grid.ac/institutes/grid.28665.3f", 
          "name": [
            "National Tsing Hua University, 30043, Hsinchu, Taiwan", 
            "Academia Sinica, Taipei, Taiwan, Republic of China"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Lee", 
        "givenName": "R. C. T.", 
        "id": "sg:person.07540250215.50", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07540250215.50"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "https://doi.org/10.1016/0020-0190(82)90110-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1000563391"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/368273.368557", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1002239284"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0304-3975(85)90144-6", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006154259"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0304-3975(85)90144-6", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006154259"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0166-218x(83)90017-3", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1007285462"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/321250.321253", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1009195371"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0020-0190(86)90051-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1013779407"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0020-0190(86)90051-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1013779407"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/321160.321166", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1015098050"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/s0004-3702(83)80007-1", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1027783001"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/321033.321034", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1028819080"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/48014.48016", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1033793319"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/7531.8928", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1040375593"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf01874393", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1042223059", 
          "https://doi.org/10.1007/bf01874393"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf01874393", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1042223059", 
          "https://doi.org/10.1007/bf01874393"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/361219.361224", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1044000109"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0304-3975(77)90054-8", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1050551316"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0210043", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062841596"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0212049", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062841729"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0214067", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062841856"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0215080", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062841942"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0218026", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062842125"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0218028", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062842127"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1137/0402046", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1062844586"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "1992-03", 
    "datePublishedReg": "1992-03-01", 
    "description": "The satisfiability problem is a well known NP-complete problem. In artificial intelligence, solving the satisfiability problem is called mechanical theorem proving. One of those mechanical theorem proving methods is the resolution principle which was invented by J.R. Robinson. In this paper, we shall show how an algorithm based upon the resolution principle can be analyzed. Letn andr0 denote the numbers of variables and input clauses respectively. LetP0 denote the probability that a variable appears positively, or negatively, in a clause. Our analysis shows that the expected total number of clauses processed by our algorithm isO(n+r0) ifP0 is a constant,r0 is polynomially related withn, andn is large.", 
    "genre": "research_article", 
    "id": "sg:pub.10.1007/bf01531030", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": false, 
    "isPartOf": [
      {
        "id": "sg:journal.1043955", 
        "issn": [
          "1012-2443", 
          "1573-7470"
        ], 
        "name": "Annals of Mathematics and Artificial Intelligence", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "1-3", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "6"
      }
    ], 
    "name": "An average case analysis of a resolution principle algorithm in mechanical theorem proving", 
    "pagination": "235-251", 
    "productId": [
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "526f96d35230c1bf398f156de0762a3f6a1918e56caa5895cbc7d3b95057f75d"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/bf01531030"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1017302452"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.1007/bf01531030", 
      "https://app.dimensions.ai/details/publication/pub.1017302452"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2019-04-10T16:39", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000001_0000000264/records_8669_00000499.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "http://link.springer.com/10.1007/BF01531030"
  }
]
 

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

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

Turtle is a human-readable linked data format.

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

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

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


 

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

143 TRIPLES      21 PREDICATES      48 URIs      19 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/bf01531030 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 schema:author N40a90df8d32949bcb3b390e75f361bd3
4 schema:citation sg:pub.10.1007/bf01874393
5 https://doi.org/10.1016/0020-0190(82)90110-7
6 https://doi.org/10.1016/0020-0190(86)90051-7
7 https://doi.org/10.1016/0166-218x(83)90017-3
8 https://doi.org/10.1016/0304-3975(77)90054-8
9 https://doi.org/10.1016/0304-3975(85)90144-6
10 https://doi.org/10.1016/s0004-3702(83)80007-1
11 https://doi.org/10.1137/0210043
12 https://doi.org/10.1137/0212049
13 https://doi.org/10.1137/0214067
14 https://doi.org/10.1137/0215080
15 https://doi.org/10.1137/0218026
16 https://doi.org/10.1137/0218028
17 https://doi.org/10.1137/0402046
18 https://doi.org/10.1145/321033.321034
19 https://doi.org/10.1145/321160.321166
20 https://doi.org/10.1145/321250.321253
21 https://doi.org/10.1145/361219.361224
22 https://doi.org/10.1145/368273.368557
23 https://doi.org/10.1145/48014.48016
24 https://doi.org/10.1145/7531.8928
25 schema:datePublished 1992-03
26 schema:datePublishedReg 1992-03-01
27 schema:description The satisfiability problem is a well known NP-complete problem. In artificial intelligence, solving the satisfiability problem is called mechanical theorem proving. One of those mechanical theorem proving methods is the resolution principle which was invented by J.R. Robinson. In this paper, we shall show how an algorithm based upon the resolution principle can be analyzed. Letn andr0 denote the numbers of variables and input clauses respectively. LetP0 denote the probability that a variable appears positively, or negatively, in a clause. Our analysis shows that the expected total number of clauses processed by our algorithm isO(n+r0) ifP0 is a constant,r0 is polynomially related withn, andn is large.
28 schema:genre research_article
29 schema:inLanguage en
30 schema:isAccessibleForFree false
31 schema:isPartOf N1734cf4e4ba548adb9a45ab7fa81c55e
32 Na338db7e2e2e47d9923bd954838642fd
33 sg:journal.1043955
34 schema:name An average case analysis of a resolution principle algorithm in mechanical theorem proving
35 schema:pagination 235-251
36 schema:productId N5fde92e65b1042239640610e758df0b2
37 Ncd4a560797214d8686c5c30cb54f3a6c
38 Nf46e7fa3197f4fa093e237be6b1faa63
39 schema:sameAs https://app.dimensions.ai/details/publication/pub.1017302452
40 https://doi.org/10.1007/bf01531030
41 schema:sdDatePublished 2019-04-10T16:39
42 schema:sdLicense https://scigraph.springernature.com/explorer/license/
43 schema:sdPublisher N8fe1bd36f2b0442ca4aa79799085e51e
44 schema:url http://link.springer.com/10.1007/BF01531030
45 sgo:license sg:explorer/license/
46 sgo:sdDataset articles
47 rdf:type schema:ScholarlyArticle
48 N1734cf4e4ba548adb9a45ab7fa81c55e schema:volumeNumber 6
49 rdf:type schema:PublicationVolume
50 N40a90df8d32949bcb3b390e75f361bd3 rdf:first sg:person.010634245333.21
51 rdf:rest N4a102c75d71246a08c030cc287152301
52 N4a102c75d71246a08c030cc287152301 rdf:first sg:person.01312526135.27
53 rdf:rest Nae895c5d778a454eaf16865ba64a03a0
54 N5fde92e65b1042239640610e758df0b2 schema:name doi
55 schema:value 10.1007/bf01531030
56 rdf:type schema:PropertyValue
57 N8fe1bd36f2b0442ca4aa79799085e51e schema:name Springer Nature - SN SciGraph project
58 rdf:type schema:Organization
59 Na338db7e2e2e47d9923bd954838642fd schema:issueNumber 1-3
60 rdf:type schema:PublicationIssue
61 Nae895c5d778a454eaf16865ba64a03a0 rdf:first sg:person.07540250215.50
62 rdf:rest rdf:nil
63 Ncd4a560797214d8686c5c30cb54f3a6c schema:name readcube_id
64 schema:value 526f96d35230c1bf398f156de0762a3f6a1918e56caa5895cbc7d3b95057f75d
65 rdf:type schema:PropertyValue
66 Nf46e7fa3197f4fa093e237be6b1faa63 schema:name dimensions_id
67 schema:value pub.1017302452
68 rdf:type schema:PropertyValue
69 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
70 schema:name Information and Computing Sciences
71 rdf:type schema:DefinedTerm
72 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
73 schema:name Artificial Intelligence and Image Processing
74 rdf:type schema:DefinedTerm
75 sg:journal.1043955 schema:issn 1012-2443
76 1573-7470
77 schema:name Annals of Mathematics and Artificial Intelligence
78 rdf:type schema:Periodical
79 sg:person.010634245333.21 schema:affiliation https://www.grid.ac/institutes/grid.38348.34
80 schema:familyName Hu
81 schema:givenName T. H.
82 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.010634245333.21
83 rdf:type schema:Person
84 sg:person.01312526135.27 schema:affiliation https://www.grid.ac/institutes/grid.38348.34
85 schema:familyName Tang
86 schema:givenName C. Y.
87 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01312526135.27
88 rdf:type schema:Person
89 sg:person.07540250215.50 schema:affiliation https://www.grid.ac/institutes/grid.28665.3f
90 schema:familyName Lee
91 schema:givenName R. C. T.
92 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07540250215.50
93 rdf:type schema:Person
94 sg:pub.10.1007/bf01874393 schema:sameAs https://app.dimensions.ai/details/publication/pub.1042223059
95 https://doi.org/10.1007/bf01874393
96 rdf:type schema:CreativeWork
97 https://doi.org/10.1016/0020-0190(82)90110-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1000563391
98 rdf:type schema:CreativeWork
99 https://doi.org/10.1016/0020-0190(86)90051-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013779407
100 rdf:type schema:CreativeWork
101 https://doi.org/10.1016/0166-218x(83)90017-3 schema:sameAs https://app.dimensions.ai/details/publication/pub.1007285462
102 rdf:type schema:CreativeWork
103 https://doi.org/10.1016/0304-3975(77)90054-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1050551316
104 rdf:type schema:CreativeWork
105 https://doi.org/10.1016/0304-3975(85)90144-6 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006154259
106 rdf:type schema:CreativeWork
107 https://doi.org/10.1016/s0004-3702(83)80007-1 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027783001
108 rdf:type schema:CreativeWork
109 https://doi.org/10.1137/0210043 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062841596
110 rdf:type schema:CreativeWork
111 https://doi.org/10.1137/0212049 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062841729
112 rdf:type schema:CreativeWork
113 https://doi.org/10.1137/0214067 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062841856
114 rdf:type schema:CreativeWork
115 https://doi.org/10.1137/0215080 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062841942
116 rdf:type schema:CreativeWork
117 https://doi.org/10.1137/0218026 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062842125
118 rdf:type schema:CreativeWork
119 https://doi.org/10.1137/0218028 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062842127
120 rdf:type schema:CreativeWork
121 https://doi.org/10.1137/0402046 schema:sameAs https://app.dimensions.ai/details/publication/pub.1062844586
122 rdf:type schema:CreativeWork
123 https://doi.org/10.1145/321033.321034 schema:sameAs https://app.dimensions.ai/details/publication/pub.1028819080
124 rdf:type schema:CreativeWork
125 https://doi.org/10.1145/321160.321166 schema:sameAs https://app.dimensions.ai/details/publication/pub.1015098050
126 rdf:type schema:CreativeWork
127 https://doi.org/10.1145/321250.321253 schema:sameAs https://app.dimensions.ai/details/publication/pub.1009195371
128 rdf:type schema:CreativeWork
129 https://doi.org/10.1145/361219.361224 schema:sameAs https://app.dimensions.ai/details/publication/pub.1044000109
130 rdf:type schema:CreativeWork
131 https://doi.org/10.1145/368273.368557 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002239284
132 rdf:type schema:CreativeWork
133 https://doi.org/10.1145/48014.48016 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033793319
134 rdf:type schema:CreativeWork
135 https://doi.org/10.1145/7531.8928 schema:sameAs https://app.dimensions.ai/details/publication/pub.1040375593
136 rdf:type schema:CreativeWork
137 https://www.grid.ac/institutes/grid.28665.3f schema:alternateName Academia Sinica
138 schema:name Academia Sinica, Taipei, Taiwan, Republic of China
139 National Tsing Hua University, 30043, Hsinchu, Taiwan
140 rdf:type schema:Organization
141 https://www.grid.ac/institutes/grid.38348.34 schema:alternateName National Tsing Hua University
142 schema:name Institute of Computer Science, National Tsing Hua University, 30043, Hsinchu, Taiwan, Republic of China
143 rdf:type schema:Organization
 




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


...