Abstract
We analyze the complexity of finite model reasoning in the description logic script A sign ℒ script C sign script Q sign script I sign, i.e. script A sign ℒ script C sign augmented with qualifying number restrictions, inverse roles, and general TBoxes. It turns out that all relevant reasoning tasks such as concept satisfiability and ABox consistency are ExpTIME-complete, regardless of whether the numbers in number restrictions are coded unarily or binarily. Thus, finite model reasoning with script A sign ℒ script C sign script Q sign script I sign is not harder than standard reasoning with script A sign ℒ script C sign script Q sign script I sign.
| Original language | English |
|---|---|
| Title of host publication | Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell |
| Editors | F. Baader |
| Publisher | Springer Nature |
| Pages | 60-74 |
| Number of pages | 14 |
| Volume | 2741 |
| Publication status | Published - 2003 |
| Event | 19th International Conference on Automated Deduction - Miami Beach, FL Duration: 1 Jul 2003 → … http://dblp.uni-trier.de/db/conf/cade/cade2003.html#RiazanovV03http://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV03.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV03 |
Publication series
| Name | Lecture Notes in Artificial Intelligence |
|---|
Conference
| Conference | 19th International Conference on Automated Deduction |
|---|---|
| City | Miami Beach, FL |
| Period | 1/07/03 → … |
| Internet address |