{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T05:09:35Z","timestamp":1742965775781,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642224379"},{"type":"electronic","value":"9783642224386"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22438-6_22","type":"book-chapter","created":{"date-parts":[[2011,7,18]],"date-time":"2011-07-18T22:21:44Z","timestamp":1311027704000},"page":"283-298","source":"Crossref","is-referenced-by-count":8,"title":["Automated Reasoning in $\\mathcal{ALCQ}$ via SMT"],"prefix":"10.1007","author":[{"given":"Volker","family":"Haarslev","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[]},{"given":"Michele","family":"Vescovi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications (2003)"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Hanna, Z., Nadel, A., Palti, A., Sebastiani, R.: MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 547\u2013560. Springer, Heidelberg (2008)","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-12002-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R., Stenico, C.: Satisfiability Modulo the Theory of Costs: Foundations and Applications. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 99\u2013113. Springer, Heidelberg (2010)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Faddoul, J., Haarslev, V.: Algebraic Tableau Reasoning for the Description Logic $\\ensuremath{\\mathcal{SHOQ}} $ . Journal of Applied Logic, Special Issue on Hybrid Logics\u00a08(4) (2010)","DOI":"10.1016\/j.jal.2010.10.001"},{"key":"22_CR5","unstructured":"Faddoul, J., Haarslev, V.: Optimizing Algebraic Tableau Reasoning for $\\mathcal{SHOQ}$ : First Experimental Results. In: Proc. of DL, Waterloo, Canada, May 4-7 (2010)"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Farsiniamarj, N., Haarslev, V.: Practical reasoning with qualified number restrictions: A hybrid abox calculus for the description logic $\\mathcal{SHQ}$ . J. AI Communications\u00a023(2-3) (2010)","DOI":"10.3233\/AIC-2010-0456"},{"key":"22_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/3-540-45744-5_59","volume-title":"Automated Reasoning","author":"V. Haarslev","year":"2001","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER System Description. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, p. 701. Springer, Heidelberg (2001)"},{"key":"22_CR8","unstructured":"Haarslev, V., Timmann, M., M\u00f6ller, R.: Combining Tableaux and Algebraic Methods for Reasoning with Qualified Number Restrictions. In: Proc. of DL 2001 (2001)"},{"key":"22_CR9","unstructured":"Hollunder, B., Baader, F.: Qualifying Number Restrictions in Concept Languages. In: Proc. of KR, Boston, USA (1991)"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Horrocks, I., Sattler, U., Tobies, S.: Practical reasoning for very expressive description logics. Logic Journal of the IGPL\u00a08(3) (2000)","DOI":"10.1093\/jigpal\/8.3.239"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Lutz, C., Areces, C., Horrocks, I., Sattler, U.: Keys, Nominals, and Concrete Domains. Journal of Artificial Intelligence Research, JAIR\u00a023(1) (2005)","DOI":"10.1613\/jair.1542"},{"key":"22_CR12","doi-asserted-by":"crossref","first-page":"141","DOI":"10.3233\/SAT190034","volume":"3","author":"R. Sebastiani","year":"2007","unstructured":"Sebastiani, R.: Lazy Satisfiability Modulo Theories. Journal on Satisfiability, Boolean Modeling and Computation, JSAT\u00a03, 141\u2013224 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation, JSAT"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Vescovi, M.: Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of $K(m)\/\\ensuremath{\\mathcal{ALC}} $ -satisfiability. JAIR\u00a035(1) (2009)","DOI":"10.1613\/jair.2675"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-02959-2_6","volume-title":"Automated Deduction \u2013 CADE-22","author":"R. Sebastiani","year":"2009","unstructured":"Sebastiani, R., Vescovi, M.: Axiom pinpointing in lightweight description logics via horn-SAT encoding and conflict analysis. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 84\u201399. Springer, Heidelberg (2009)"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Sirin, E., Parsia, B., Grau, B.C., Kalyanpur, A., Katz, Y.: Pellet: A practical OWL-DL reasoner. Journal of Web Semantics\u00a05(2) (2007)","DOI":"10.1016\/j.websem.2007.03.004"},{"key":"22_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D. Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: faCT++ description logic reasoner: System description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 292\u2013297. Springer, Heidelberg (2006)"},{"key":"22_CR17","unstructured":"Vescovi, M., Sebastiani, R., Haarslev, V.: Automated Reasoning on TBoxes with Qualified Number Restrictions via SMT. Tech. Rep. DISI-11-001, Universit\u00e0 di Trento (April 2011), http:\/\/disi.unitn.it\/~rseba\/cade11\/techrep.pdf"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-23"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22438-6_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,21]],"date-time":"2020-06-21T11:44:52Z","timestamp":1592739892000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22438-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642224379","9783642224386"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22438-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}