Abstract
We present a resolution-based decision procedure for the description logic \(\mathcal{SHOIQ}\) – the logic underlying the Semantic Web ontology language OWLDL. Our procedure is goal-oriented, and it naturally extends a similar procedure for \(\mathcal{SHIQ}\), which has proven itself in practice. Extending this procedure to \(\mathcal{SHOIQ}\) using existing techniques is not straightforward because of nominals, number restrictions, and inverse roles – a combination known to cause termination problems. We overcome this difficulty by using basic superposition calculus extended with custom simplification rules.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision procedures by superposition. In: Proceedings of the 15th International Workshop on Computer Science Logic (CSL’ 01). LNCS, vol. 2142, pp. 549–563. Paris, France (2001)
Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press (2003)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, Chapt. 2, pp. 19–99. Elsevier Science (2001)
Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation. Inf. Comput. 121(2), 172–192 (1995)
Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a decision procedure for the monadic class with equality. In: Proceedings of the Third Kurt Gödel Colloquium on Computational Logic and Proof Theory (KGC ’93). LNCS, vol. 713, pp. 83–96. Brno, Czech Republic (1993)
Baumgartner, P., Schmidt, R.A.: Blocking and other enhancements for bottom-Up model generation methods. In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR 2006), LNCS, vol. 4130, pp. 125–139. Seattle, WA (2006)
Bergamaschi, S., Castano, S., Vincini, M., Beneventano, D.: Semantic integration of heterogeneous information sources. Data Knowl. Eng. 36(3), 215–249 (2001)
Borgida, A.: On the relative expressiveness of description logics and predicate logics. Artif. Intell. 82(1–2), 353–367 (1996)
Calvanese, D., Lenzerini, M., Nardi, D.: Unifying class-based representation formalisms. J. Artif. Intell. Res. (JAIR) 11, 199–240 (1999)
de Nivelle, H.: Ordering Refinements of Resolution. Ph.D. thesis, Technische Universiteit Delft (1995)
de Nivelle, H.: Deciding the E-plus class by an a posteriori, liftable order. Ann. Pure Appl. Logic 88(1), 219–232 (2000)
de Nivelle, H., de Rijke, M.: Deciding the guarded fragments by resolution. J. Symb. Comput. 35, 21–58 (2003).
de Nivelle, H., Pratt-Hartmann, I.: A resolution-based decision procedure for the two-variable fragment with equality. In: Proceedings of the 1st International Joint Conference on Automated Reasoning (IJCAR 2001). LNAI, vol. 2083, pp. 211–225. Siena, Italy (2001)
Fermüller, C., Tammet, T., Zamov, N., Leitsch, A.: Resolution Methods for the Decision Problem. LNAI, vol. 679. Springer (1993)
Fermüller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, Chapt. 25, pp. 1791–1849. Elsevier Science (2001)
Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: Proceedings of the 14th IEEE Symposium on Logic in Computer Science (LICS ’99), pp. 295–305. Trento, Italy (1999)
Goasdoué, F., Rousset, M.-C.: Answering queries using views: a KRDB perspective for the semantic web. ACM Trans. Internet Technology 4(3), 255–288 (2004)
Haarslev, V., Timmann, M., Möller, R.: Combining tableaux and algebraic methods for reasoning with qualified number restrictions. In: Proceedings of the 2001 International Workshop on Description Logics (DL 2001). CEUR Workshop Proceedings, vol. 49. Stanford, CA (2001)
Haken, A.: The intractability of resolution. Theor. Comp. Sci. 39, 297–308 (1985)
Horrocks, I., Sattler, U.: Ontology reasoning in the \(\mathcal{SHOQ}\)(D) description logic. In: Nebel, B. (ed.) Proceedings of the 7th International Joint Conference on Artificial Intelligence (IJCAI 2001), pp. 199–204. Seattle, WA (2001)
Horrocks, I., Sattler, U.: A tableaux decision procedure for \(\mathcal{SHOIQ}\). In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI 2005), pp. 448–453. Edinburgh, UK (2005)
Horrocks, I., Sattler, U., Tobies, S.: Reasoning with individuals for the description logic \(\mathcal{SHIQ}\). In: Proceedings of the 17th International Conference on Automated Deduction (CADE-17). LNAI, vol. 1831, pp. 482–496. Pittsburgh (2000)
Hustadt, U., Motik, B., Sattler, U.: Reducing \(\mathcal{SHIQ}^-\) Description logic to disjunctive datalog programs. In: Proceedings of the 9th International Conference on the Principles of Knowledge Representation and Reasoning (KR 2004), pp. 152–162. Whistler, Canada, (2004)
Hustadt, U., Motik, B., Sattler, U.: A decomposition rule for decision procedures by resolution-based calculi. In: Proceedings of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2004). LNAI, vol. 3452, pp. 21–35. Montevideo, Uruguay (2005)
Hustadt, U., Schmidt, R.A.: Maslov’s class K revisited. In: Proceedings of the 16th International Conference on Automated Deduction (CADE-16), LNAI, vol. 1632, pp. 172–186 . Trento, Italy (1999)
Joyner, W.H.: Resolution strategies as decision procedures. J. ACM 23(3), 398–417 (1976)
Kazakov, Y.: Saturation-Based Decision Procedures for Extensions of the Guarded Fragment. Ph.D. thesis, Univesität des Saarlandes, Germany (2006)
Kazakov, Y., de Nivelle, H.: A resolution decision procedure for the guarded fragment with transitive guards. In: Proceedings of 2nd International Joint Conference on Automated Reasoning (IJCAR 2004). LNAI, vol. 3097, pp. 122–136. Cork, Ireland (2004)
Kazakov, Y., Motik, B.: A resolution-based decision procedure for \(\mathcal{SHOIQ}\). In: Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR 2006), vol. 4130 of LNCS, pp. 662–667. Seattle, WA (2006)
Leitsch, A.: Deciding clause classes by semantic clash resolution. Fundam. Inform. 18, 163–182 (1993)
Levy, A.Y., Srivastava, D., Kirk, T.: Data model and query evaluation in global information systems. J. Intell. Inform. Syst. 5(2), 121–143 (1995)
Motik, B.: Reasoning in Description Logics using Resolution and Deductive Databases. Ph.D. thesis, Univesität Karlsruhe, Germany (2006)
Motik, B., Sattler, U.: A comparison of reasoning techniques for querying large description logic ABoxes. In: Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2006), LNCS, vol. 4246, pp. 227–241. Phnom Penh, Cambodia (2006)
Nieuwenhuis, R., Rubio, A.: Theorem proving with ordering and equality constrained clauses. J. Symb. Comput. 19(4), 312–351 (1995)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 1, Chapt. 7, pp. 371–443. Elsevier Science (2001)
Nivelle, H.D., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Log. J. IGPL 8(3), 265–292 (2000)
Pacholski, L., Szwast, W., Tendera, L.: Complexity results for first-order two-variable logic with counting. SIAM J. Comput. 29(4), 1083–1117 (2000)
Patel-Schneider, P.F., Hayes, P., Horrocks, I.: OWL Web Ontology Language: Semantics and Abstract Syntax, W3C Recommendation. http://www.w3.org/TR/owl-semantics/ (2004)
Peltier, N.: On the decidability of the PVD class with equality. Log. J. IGPL 9(4), 601–624 (2001)
Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput. 2(3), 293–304 (1986)
Pratt-Hartmann, I.: Complexity of the two-variable fragment with counting quantifiers. J. Logic, Lang. Inf. 14(3), 369–395 (2005)
Schmidt, R.A., Hustadt, U.: A principle for incorporating axioms into the first-order translation of modal formulae. In: Proc. of the 19th Int. Conf. on Automated Deduction (CADE-19). LNAI, vol. 2741, pp. 412–426. Miami Beach, FL (2003)
Tammet, T.: Resolution Methods for Decision Problems and Finite-Model Building. Ph.D. thesis, Göteborg University, Sweden (1992)
Tobies, S.: Complexity Results and Practical Algorithms for Logics in Knowledge Representation. Ph.D. thesis, RWTH Aachen, Germany (2001)
Vardi, M.Y.: Why is modal logic so robustly decidable? In: Immerman, N., Kolaitis, P. (eds.) Proc. of a DIMACS Workshop on Descriptive Complexity and Finite Models, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 31, pp. 149–184. Princeton University, Princeton, NJ (1996)
Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, Chapt. 27, pp. 1965–2013. Elsevier Science (2001)
Author information
Authors and Affiliations
Corresponding author
Additional information
This paper is an extended version of [31]. Our work was partially funded by the EPSRC project REOL.
An erratum to this article can be found at http://dx.doi.org/10.1007/s10817-008-9100-y
Rights and permissions
About this article
Cite this article
Kazakov, Y., Motik, B. A Resolution-Based Decision Procedure for \(\boldsymbol{\mathcal{SHOIQ}}\) . J Autom Reasoning 40, 89–116 (2008). https://doi.org/10.1007/s10817-007-9090-1
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-007-9090-1