Abstract
In this paper we propose a procedure for encoding the \(\mathcal{ALCN}\) Description Logic concept satisfiability into SAT problem. In particular, a concept description is translated into the set of propositions, which is satisfiable iff the description is satisfiable, as well. The satisfiability of the resulting propositions is tested by SAT solving tools based on the DPLL procedure and widely known for their efficiency. We describe and analyse the results of preliminary experiments aimed at evaluating the performance of the presented approach.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, implementation, and applications. Cambridge University Press, Cambridge (2003)
Brand, S., Gennari, R., de Rijke, M.: Constraint Methods for Modal Satisfiability. In: Apt, K.R., Fages, F., Rossi, F., Szeredi, P., Váncza, J. (eds.) CSCLP 2003. LNCS (LNAI), vol. 3010, pp. 66–86. Springer, Heidelberg (2004)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem-Proving. Commun. ACM 5(7), 394–397 (1962)
Giunchiglia, F., Sebastiani, R.: Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m). Inform. Comput. 162(1/2), 158–178 (2000)
Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-Based Decision Procedures for Classical Modal Logics. J. Autom. Reasoning 28(2), 143–171 (2002)
Hoos, H.H., Stützle, T.: SATLIB: An Online Resource for Research on SAT. In: Gent, I.P., et al. (eds.) SAT 2000, pp. 283–292. IOS Press, Amsterdam (2000)
Nadel, A.: Understanding and Improving a Modern SAT Solver. PhD thesis, Tel Aviv University (2009)
Sebastiani, R., Vescovi, M.: Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/\(\mathcal{ALC}\). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 130–135. Springer, Heidelberg (2006)
Sebastiani, R., Vescovi, M.: Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of \(K_{m}/\mathcal{ALC}\)-Satisfiability. J. Artif. Intell. Res. 35, 343–389 (2009)
TONES Ontology Repository, http://owl.cs.manchester.ac.uk/repository/
World Wide Web Consortium, Semantic Web, http://www.w3.org/2001/sw/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Meissner, A. (2011). The \(\mathcal{ALCN}\) Description Logic Concept Satisfiability as a SAT Problem. In: Katarzyniak, R., Chiu, TF., Hong, CF., Nguyen, N.T. (eds) Semantic Methods for Knowledge Management and Communication. Studies in Computational Intelligence, vol 381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23418-7_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-23418-7_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23417-0
Online ISBN: 978-3-642-23418-7
eBook Packages: EngineeringEngineering (R0)