{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T23:01:50Z","timestamp":1752102110704},"publisher-location":"Cham","reference-count":47,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030221010"},{"type":"electronic","value":"9783030221027"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-22102-7_27","type":"book-chapter","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T12:21:26Z","timestamp":1561465286000},"page":"573-587","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["15 Years of Consequence-Based Reasoning"],"prefix":"10.1007","author":[{"given":"David","family":"Tena Cucala","sequence":"first","affiliation":[]},{"given":"Bernardo","family":"Cuenca Grau","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Horrocks","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,6,1]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1613\/jair.4898","volume":"55","author":"A Armas Romero","year":"2016","unstructured":"Armas Romero, A., Kaminski, M., Cuenca Grau, B., Horrocks, I.: Module extraction in expressive ontology languages via datalog reasoning. J. Artif. Intell. Res. 55, 499\u2013564 (2016)","journal-title":"J. Artif. Intell. Res."},{"key":"27_CR2","unstructured":"Baader, F., Brandt, S., Lutz, C.: Pushing the $$\\cal{EL}$$ envelope. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, pp. 364\u2013369. Morgan Kaufmann Publishers, Edinburgh (2005)"},{"volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2003","key":"27_CR3","unstructured":"Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"27_CR4","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1013882326814","volume":"69","author":"F Baader","year":"2001","unstructured":"Baader, F., Sattler, U.: An overview of tableau algorithms for description logics. Studia Logica 69, 5\u201340 (2001)","journal-title":"Studia Logica"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F.: Terminological cycles in a description logic with existential restrictions. In: Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, pp. 325\u2013330. Morgan Kaufmann Publishers, Acapulco (2003)","DOI":"10.25368\/2022.120"},{"key":"27_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/9781139025355","volume-title":"An Introduction to Description Logic","author":"F Baader","year":"2017","unstructured":"Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press, Cambridge (2017)"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"Baader, F., K\u00fcsters, R., Molitor, R.: Computing least common subsumers in description logics with existential restrictions. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, pp. 96\u2013103 (1999)","DOI":"10.25368\/2022.85"},{"key":"27_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11814771_25","volume-title":"Automated Reasoning","author":"F Baader","year":"2006","unstructured":"Baader, F., Lutz, C., Suntisrivaraporn, B.: CEL\u2014a polynomial-time reasoner for life science ontologies. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 287\u2013291. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_25"},{"key":"27_CR9","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 19\u201399. Elsevier Science, London (2001)"},{"key":"27_CR10","unstructured":"Bate, A., Motik, B., Cuenca Grau, B., Simancik, F., Horrocks, I.: Extending consequence-based reasoning to SRIQ. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, pp. 187\u2013196. AAAI Press, Cape Town (2016)"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1613\/jair.1.11257","volume":"63","author":"A Bate","year":"2018","unstructured":"Bate, A., Motik, B., Cuenca Grau, B., Tena Cucala, D., Simancik, F., Horrocks, I.: Consequence-based reasoning for description logics with disjunctions and number restrictions. J. Artif. Intell. Res. 63, 625\u2013690 (2018)","journal-title":"J. Artif. Intell. Res."},{"key":"27_CR12","unstructured":"Brandt, S.: Polynomial time reasoning in a description Logic with existential restrictions, GCI axioms, and\u2014what else? In: Proceedings of the 16th European Conference on Artificial Intelligence, Valencia, Spain, pp. 298\u2013302 (2004)"},{"key":"27_CR13","unstructured":"Carral, D., Dragoste, I., Kr\u00f6tzsch, M.: The combined approach to query answering in horn-ALCHOIQ. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, pp. 339\u2013348. AAAI Press, Tempe (2018)"},{"key":"27_CR14","unstructured":"Feier, C., Carral, D., Stefanoni, G., Grau, B.C., Horrocks, I.: The combined approach to query answering beyond the OWL 2 profiles. In: Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, pp. 2971\u20132977. AAAI Press, Buenos Aires (2015)"},{"key":"27_CR15","unstructured":"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, pp. 295\u2013305. IEEE Computer Society, Trento (1999)"},{"issue":"1\u20132","key":"27_CR16","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/S0747-7171(03)00034-8","volume":"36","author":"L Georgieva","year":"2003","unstructured":"Georgieva, L., Hustadt, U., Schmidt, R.A.: Hyperresolution for guarded formulae. J. Symb. Comput. 36(1\u20132), 163\u2013192 (2003)","journal-title":"J. Symb. Comput."},{"issue":"3","key":"27_CR17","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-014-9305-1","volume":"53","author":"B Glimm","year":"2014","unstructured":"Glimm, B., Horrocks, I., Motik, B., Stoilos, G., Wang, Z.: HermiT: an OWL 2 reasoner. J. Autom. Reason. 53(3), 245\u2013269 (2014)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"27_CR18","doi-asserted-by":"crossref","first-page":"267","DOI":"10.3233\/SW-2011-0032","volume":"3","author":"V Haarslev","year":"2012","unstructured":"Haarslev, V., Hidde, K., M\u00f6ller, R., Wessel, M.: The RacerPro knowledge representation and reasoning system. Semant. Web 3(3), 267\u2013277 (2012)","journal-title":"Semant. Web"},{"key":"27_CR19","unstructured":"Horrocks, I., Sattler, U.: A tableaux decision procedure for $$\\cal{SHOIQ}$$ . In: Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, Edinburgh, UK, pp. 448\u2013453 (2005)"},{"key":"27_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-46508-1_13","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"U Hustadt","year":"2000","unstructured":"Hustadt, U., Schmidt, R.A.: Issues of decidability for description logics in the framework of resolution. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol. 1761, pp. 191\u2013205. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46508-1_13"},{"issue":"5","key":"27_CR21","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1016\/j.ic.2007.11.006","volume":"206","author":"U Hustadt","year":"2008","unstructured":"Hustadt, U., Motik, B., Sattler, U.: Deciding expressive description logics in the framework of resolution. Inf. Comput. 206(5), 579\u2013601 (2008)","journal-title":"Inf. Comput."},{"issue":"2","key":"27_CR22","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1015067300005","volume":"28","author":"U Hustadt","year":"2002","unstructured":"Hustadt, U., Schmidt, R.A.: Using resolution for testing modal satisfiability and building models. J. Autom. Reason. 28(2), 205\u2013232 (2002)","journal-title":"J. Autom. Reason."},{"key":"27_CR23","unstructured":"Karahroodi, N.Z., Haarslev, V.: A consequence-based algebraic calculus for $$\\cal{SHOQ}$$ . In: Proceedings of the 30th International Workshop on Description Logics. CEUR Workshop Proceedings, Montpellier, France, vol. 1879 (2017)"},{"key":"27_CR24","unstructured":"Kazakov, Y.: Consequence-driven reasoning for horn $$\\cal{SHIQ}$$ ontologies. In: Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, CA, USA, pp. 2040\u20132045 (2009)"},{"key":"27_CR25","unstructured":"Kazakov, Y., Klinov, P.: Bridging the gap between tableau and consequence-based reasoning. In: Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, pp. 579\u2013590 (2014)"},{"key":"27_CR26","unstructured":"Kazakov, Y., Kr\u00f6tzsch, M., Siman\u010d\u00edk, F.: Practical reasoning with nominals in the EL family of description logics. In: Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (2012)"},{"issue":"1","key":"27_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-013-9296-3","volume":"53","author":"Y Kazakov","year":"2014","unstructured":"Kazakov, Y., Kr\u00f6tzsch, M., Siman\u010d\u00edk, F.: The incredible ELK\u2014from polynomial procedures to efficient reasoning with $$\\cal{EL}$$ ontologies. J. Autom. Reason. 53(1), 1\u201361 (2014)","journal-title":"J. Autom. Reason."},{"issue":"2\u20133","key":"27_CR28","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10817-007-9090-1","volume":"40","author":"Y Kazakov","year":"2008","unstructured":"Kazakov, Y., Motik, B.: A resolution-based decision procedure for $$\\cal{SHOIQ}$$ . J. Autom. Reason. 40(2\u20133), 89\u2013116 (2008)","journal-title":"J. Autom. Reason."},{"key":"27_CR29","unstructured":"Kontchakov, R., Lutz, C., Toman, D., Wolter, F., Zakharyaschev, M.: The combined approach to query answering in DL-Lite. In: Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference. AAAI Press, Toronto (2010)"},{"key":"27_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-48242-3_12","volume-title":"Logic for Programming and Automated Reasoning","author":"C Lutz","year":"1999","unstructured":"Lutz, C.: Complexity of terminological reasoning revisited. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol. 1705, pp. 181\u2013200. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48242-3_12"},{"key":"27_CR31","unstructured":"Metke-Jimenez, A., Lawley, M.: Snorocket 2.0: concrete domains and concurrent classification. In: Informal Proceedings of the 2nd International Workshop on OWL Reasoner Evaluation, Ulm, Germany, vol. 1015, pp. 32\u201338 (2013)"},{"issue":"72","key":"27_CR32","first-page":"19","volume":"2008","author":"B Motik","year":"2008","unstructured":"Motik, B.: KAON2 - scalable reasoning over ontologies with large data sets. ERCIM News 2008(72), 19\u201320 (2008)","journal-title":"ERCIM News"},{"key":"27_CR33","unstructured":"Motik, B., Cuenca Grau, B., Horrocks, I., Wu, Z., Fokoue, A., Lutz, C.: OWL 2 Web Ontology Language Profiles. http:\/\/www.w3.org\/TR\/owl2-profiles\/"},{"issue":"3","key":"27_CR34","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H Nivelle de","year":"2000","unstructured":"de Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Log. J. IGPL 8(3), 265\u2013292 (2000)","journal-title":"Log. J. IGPL"},{"key":"27_CR35","unstructured":"Ortiz, M., Rudolph, S., Simkus, M.: Worst-case optimal reasoning for the horn-DL fragments of OWL 1 and 2. In: Proceedings of the Twelfth International Conference on the Principles of Knowledge Representation and Reasoning, Toronto, Canada. AAAI Press (2010)"},{"volume-title":"Handbook of Automated Reasoning","year":"2001","key":"27_CR36","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier, Amsterdam (2001)"},{"key":"27_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-37651-1_15","volume-title":"Programming Logics","author":"RA Schmidt","year":"2013","unstructured":"Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 345\u2013391. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_15"},{"key":"27_CR38","unstructured":"Siman\u010d\u00edk, F., Kazakov, Y., Horrocks, I.: Consequence-based reasoning beyond Horn ontologies. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence, pp. 1093\u20131098. IJCAI\/AAAI, Barcelona (2011)"},{"key":"27_CR39","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.artint.2014.01.002","volume":"209","author":"F Siman\u010d\u00edk","year":"2014","unstructured":"Siman\u010d\u00edk, F., Motik, B., Horrocks, I.: Consequence-based and fixed-parameter tractable reasoning in description logics. Artif. Intell. 209, 29\u201377 (2014)","journal-title":"Artif. Intell."},{"issue":"2","key":"27_CR40","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.websem.2007.03.004","volume":"5","author":"E Sirin","year":"2007","unstructured":"Sirin, E., Parsia, B., Cuenca Grau, B., Kalyanpur, A., Katz, Y.: Pellet: a practical OWL-DL reasoner. J. Web Semant. 5(2), 51\u201353 (2007)","journal-title":"J. Web Semant."},{"issue":"1","key":"27_CR41","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1016\/j.websem.2014.06.003","volume":"27","author":"A Steigmiller","year":"2014","unstructured":"Steigmiller, A., Liebig, T., Glimm, B.: Konclude: system description. J. Web Semant. 27(1), 78\u201385 (2014)","journal-title":"J. Web Semant."},{"key":"27_CR42","doi-asserted-by":"crossref","unstructured":"Tena Cucala, D., Cuenca Grau, B., Horrocks, I.: Consequence-based reasoning for description logics with disjunction, inverse roles, and nominals. In: Proceedings of the 30th International Workshop on Description Logics. CEUR-WS.org, Montpelier (2017)","DOI":"10.24963\/ijcai.2018\/272"},{"key":"27_CR43","doi-asserted-by":"crossref","unstructured":"Tena Cucala, D., Cuenca Grau, B., Horrocks, I.: Consequence-based reasoning for description logics with disjunction, inverse roles, number restrictions, and nominals. In: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, pp. 1970\u20131976. ijcai.org, Stockholm (2018)","DOI":"10.24963\/ijcai.2018\/272"},{"key":"27_CR44","series-title":"Lecture Notes in Computer Science (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. 4130, pp. 292\u2013297. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11814771_26"},{"key":"27_CR45","unstructured":"Vlasenko, J., Daryalal, M., Haarslev, V., Jaumard, B.: A saturation-based algebraic reasoner for ELQ. In: Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning, Coimbra, Portugal, pp. 110\u2013124 (2016)"},{"key":"27_CR46","unstructured":"W3C OWL Working Group: OWL 2 Web Ontology Language Overview. http:\/\/www.w3.org\/TR\/owl2-overview\/"},{"key":"27_CR47","unstructured":"Wos, L., Robinson, G.: Paramodulation and theorem-proving in first-order theories with equality. In: Michie, D., Meltzer, B. (eds.) Proceedings of the 4th Annual Machine Intelligence Workshop. Edinburgh University Press, Edinburgh (1969)"}],"container-title":["Lecture Notes in Computer Science","Description Logic, Theory Combination, and All That"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-22102-7_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,21]],"date-time":"2022-09-21T20:30:48Z","timestamp":1663792248000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-22102-7_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030221010","9783030221027"],"references-count":47,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-22102-7_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"1 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}