# A Decomposition Rule for Decision Procedures by Resolution-Based Calculi

Ontology type: schema:Chapter

### Chapter Info

DATE

2005

AUTHORS ABSTRACT

Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{SHIQ}$\end{document}. In this paper, we present a new decomposition inference rule, which can be combined with any resolution-based calculus compatible with the standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: (i) for the description logic \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{SHIQ}$\end{document}, (ii) for the description logic \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{ALCHIQ}b$\end{document}, and (iii) for answering conjunctive queries over \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{SHIQ}$\end{document} knowledge bases. The first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage. More... »

PAGES

21-35

### Book

TITLE

Logic for Programming, Artificial Intelligence, and Reasoning

ISBN

978-3-540-25236-8
978-3-540-32275-7

### Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-540-32275-7_2

DOI

http://dx.doi.org/10.1007/978-3-540-32275-7_2

DIMENSIONS

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

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:

[
{
"@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json",
{
"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": "Department of Computer Science, University of Liverpool, Liverpool, UK",
"id": "http://www.grid.ac/institutes/grid.10025.36",
"name": [
"Department of Computer Science, University of Liverpool, Liverpool, UK"
],
"type": "Organization"
},
"givenName": "Ullrich",
"id": "sg:person.015632277175.38",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015632277175.38"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "FZI Research Center for Information Technologies at the University of Karlsruhe, Karlsruhe, Germany",
"id": "http://www.grid.ac/institutes/grid.7892.4",
"name": [
"FZI Research Center for Information Technologies at the University of Karlsruhe, Karlsruhe, Germany"
],
"type": "Organization"
},
"familyName": "Motik",
"givenName": "Boris",
"id": "sg:person.07401076267.36",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07401076267.36"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Department of Computer Science, University of Manchester, Manchester, UK",
"id": "http://www.grid.ac/institutes/grid.5379.8",
"name": [
"Department of Computer Science, University of Manchester, Manchester, UK"
],
"type": "Organization"
},
"familyName": "Sattler",
"givenName": "Ulrike",
"id": "sg:person.015322100453.31",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015322100453.31"
],
"type": "Person"
}
],
"datePublished": "2005",
"datePublishedReg": "2005-01-01",
"description": "Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$\\mathcal{SHIQ}$\\end{document}. In this paper, we present a new decomposition inference rule, which can be combined with any resolution-based calculus compatible with the standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: (i)\u00a0for the description logic \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$\\mathcal{SHIQ}$\\end{document}, (ii)\u00a0for the description logic \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$\\mathcal{ALCHIQ}b$\\end{document}, and (iii)\u00a0for answering conjunctive queries over \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$\\mathcal{SHIQ}$\\end{document} knowledge bases. The first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage.",
"editor": [
{
"givenName": "Franz",
"type": "Person"
},
{
"familyName": "Voronkov",
"givenName": "Andrei",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/978-3-540-32275-7_2",
"inLanguage": "en",
"isAccessibleForFree": false,
"isPartOf": {
"isbn": [
"978-3-540-25236-8",
"978-3-540-32275-7"
],
"name": "Logic for Programming, Artificial Intelligence, and Reasoning",
"type": "Book"
},
"keywords": [
"first-order logic",
"numerous refinements",
"decision procedure",
"logic",
"standard notion",
"complex logic",
"resolution-based calculus",
"theorem proving",
"description logics",
"equality",
"notion",
"efficient theorem provers",
"rules",
"conjunctive queries",
"knowledge bases",
"inference rules",
"vast experience",
"theorem provers",
"new decision procedure",
"practical usage",
"decomposition rules",
"calculus",
"proving",
"basic superposition",
"experience",
"queries",
"provers",
"inference",
"redundancy",
"basis",
"usage",
"paper",
"decomposition",
"refinement",
"resolution",
"procedure",
"superposition",
"new decomposition inference rule",
"decomposition inference rule"
],
"name": "A Decomposition Rule for Decision Procedures by Resolution-Based Calculi",
"pagination": "21-35",
"productId": [
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1000889893"
]
},
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/978-3-540-32275-7_2"
]
}
],
"publisher": {
"name": "Springer Nature",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/978-3-540-32275-7_2",
"https://app.dimensions.ai/details/publication/pub.1000889893"
],
"sdDataset": "chapters",
"sdDatePublished": "2022-01-01T19:12",
"sdPublisher": {
"name": "Springer Nature - SN SciGraph project",
"type": "Organization"
},
"sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_208.jsonl",
"type": "Chapter",
"url": "https://doi.org/10.1007/978-3-540-32275-7_2"
}
]

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/978-3-540-32275-7_2'

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/978-3-540-32275-7_2'

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-32275-7_2'

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

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

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

125 TRIPLES      23 PREDICATES      66 URIs      59 LITERALS      7 BLANK NODES

Subject Predicate Object
2 anzsrc-for:0802
3 schema:author N2056990369e14f99ba70db178c6c1107
4 schema:datePublished 2005
5 schema:datePublishedReg 2005-01-01
6 schema:description Resolution-based calculi are among the most widely used calculi for theorem proving in first-order logic. Numerous refinements of resolution are nowadays available, such as e.g. basic superposition, a calculus highly optimized for theorem proving with equality. However, even such an advanced calculus does not restrict inferences enough to obtain decision procedures for complex logics, such as \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{SHIQ}$\end{document}. In this paper, we present a new decomposition inference rule, which can be combined with any resolution-based calculus compatible with the standard notion of redundancy. We combine decomposition with basic superposition to obtain three new decision procedures: (i) for the description logic \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{SHIQ}$\end{document}, (ii) for the description logic \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{ALCHIQ}b$\end{document}, and (iii) for answering conjunctive queries over \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\mathcal{SHIQ}$\end{document} knowledge bases. The first two procedures are worst-case optimal and, based on the vast experience in building efficient theorem provers, we expect them to be suitable for practical usage.
7 schema:editor N6cd4812330294fc7af15e1720e2d3621
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf N1827503a1c6341b2a5599d493ce9140c
13 basic superposition
14 basis
15 calculus
16 complex logic
17 conjunctive queries
18 decision procedure
19 decomposition
20 decomposition inference rule
21 decomposition rules
22 description logics
23 efficient theorem provers
24 equality
25 experience
26 first-order logic
27 inference
28 inference rules
29 knowledge bases
30 logic
31 new decision procedure
32 new decomposition inference rule
33 notion
34 numerous refinements
35 paper
36 practical usage
37 procedure
38 provers
39 proving
40 queries
41 redundancy
42 refinement
43 resolution
44 resolution-based calculus
45 rules
46 standard notion
47 superposition
48 theorem provers
49 theorem proving
50 usage
51 vast experience
52 schema:name A Decomposition Rule for Decision Procedures by Resolution-Based Calculi
53 schema:pagination 21-35
54 schema:productId N4eb7f0605a3147d1b6c7a76dc67d39c9
55 Nae7bc62ea35b485ebfce578f6aea503d
56 schema:publisher N3a7ec2a0b49240fc9dd7f4b4315a8608
57 schema:sameAs https://app.dimensions.ai/details/publication/pub.1000889893
58 https://doi.org/10.1007/978-3-540-32275-7_2
59 schema:sdDatePublished 2022-01-01T19:12
62 schema:url https://doi.org/10.1007/978-3-540-32275-7_2
64 sgo:sdDataset chapters
65 rdf:type schema:Chapter
66 N1827503a1c6341b2a5599d493ce9140c schema:isbn 978-3-540-25236-8
67 978-3-540-32275-7
68 schema:name Logic for Programming, Artificial Intelligence, and Reasoning
69 rdf:type schema:Book
70 N2056990369e14f99ba70db178c6c1107 rdf:first sg:person.015632277175.38
72 N35feb640608044629b7cd6d2fdc68a16 rdf:first Nae4f7bbec638431ab2b80ba6bedc708b
73 rdf:rest rdf:nil
74 N3a7ec2a0b49240fc9dd7f4b4315a8608 schema:name Springer Nature
75 rdf:type schema:Organisation
76 N3e2db15fff704ff7bcf5af0362d8dddd rdf:first sg:person.015322100453.31
77 rdf:rest rdf:nil
78 N4eb7f0605a3147d1b6c7a76dc67d39c9 schema:name dimensions_id
79 schema:value pub.1000889893
80 rdf:type schema:PropertyValue
82 rdf:rest N35feb640608044629b7cd6d2fdc68a16
84 schema:givenName Franz
85 rdf:type schema:Person
86 Nae4f7bbec638431ab2b80ba6bedc708b schema:familyName Voronkov
87 schema:givenName Andrei
88 rdf:type schema:Person
89 Nae7bc62ea35b485ebfce578f6aea503d schema:name doi
90 schema:value 10.1007/978-3-540-32275-7_2
91 rdf:type schema:PropertyValue
92 Nbb63cdc7a7d449a3adb2ec2b1c6c5812 schema:name Springer Nature - SN SciGraph project
93 rdf:type schema:Organization
95 rdf:rest N3e2db15fff704ff7bcf5af0362d8dddd
96 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
97 schema:name Information and Computing Sciences
98 rdf:type schema:DefinedTerm
99 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
100 schema:name Computation Theory and Mathematics
101 rdf:type schema:DefinedTerm
102 sg:person.015322100453.31 schema:affiliation grid-institutes:grid.5379.8
103 schema:familyName Sattler
104 schema:givenName Ulrike
105 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015322100453.31
106 rdf:type schema:Person
107 sg:person.015632277175.38 schema:affiliation grid-institutes:grid.10025.36
109 schema:givenName Ullrich
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.015632277175.38
111 rdf:type schema:Person
112 sg:person.07401076267.36 schema:affiliation grid-institutes:grid.7892.4
113 schema:familyName Motik
114 schema:givenName Boris
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07401076267.36
116 rdf:type schema:Person
117 grid-institutes:grid.10025.36 schema:alternateName Department of Computer Science, University of Liverpool, Liverpool, UK
118 schema:name Department of Computer Science, University of Liverpool, Liverpool, UK
119 rdf:type schema:Organization
120 grid-institutes:grid.5379.8 schema:alternateName Department of Computer Science, University of Manchester, Manchester, UK
121 schema:name Department of Computer Science, University of Manchester, Manchester, UK
122 rdf:type schema:Organization
123 grid-institutes:grid.7892.4 schema:alternateName FZI Research Center for Information Technologies at the University of Karlsruhe, Karlsruhe, Germany
124 schema:name FZI Research Center for Information Technologies at the University of Karlsruhe, Karlsruhe, Germany
125 rdf:type schema:Organization