{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T07:40:17Z","timestamp":1710747617442},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,12,17]],"date-time":"2009-12-17T00:00:00Z","timestamp":1261008000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s10817-009-9160-7","type":"journal-article","created":{"date-parts":[[2009,12,16]],"date-time":"2009-12-16T07:31:10Z","timestamp":1260948670000},"page":"371-399","source":"Crossref","is-referenced-by-count":6,"title":["$\\boldsymbol {\\cal BC\\!D\\!L}$ : Basic Constructive Description Logic"],"prefix":"10.1007","volume":"44","author":[{"given":"Mauro","family":"Ferrari","sequence":"first","affiliation":[]},{"given":"Camillo","family":"Fiorentini","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Fiorino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,12,17]]},"reference":[{"key":"9160_CR1","unstructured":"Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F. (eds.): The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"9160_CR2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.3233\/FI-2009-178","volume":"96","author":"L Bozzato","year":"2009","unstructured":"Bozzato, L., Ferrari, M., Villa, P.: Actions over a constructive semantics for description logics. Fundam. Inform. 96, 1\u201317 (2009)","journal-title":"Fundam. Inform."},{"key":"9160_CR3","doi-asserted-by":"crossref","unstructured":"Brachman, R.J., Mcguinness, D.L., Patel-Schneider, P.F., Resnick, L.A., Borgida, A.: Living with CLASSIC: When and How to Use a KL-ONE-like Language (1991)","DOI":"10.1016\/B978-1-4832-0771-1.50022-9"},{"key":"9160_CR4","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","author":"A Chagrov","year":"1997","unstructured":"Chagrov, A., Zakharyaschev, M.: Modal Logic. Oxford University Press, Oxford (1997)"},{"key":"9160_CR5","unstructured":"de Paiva, V.: Constructive description logics: what, why and how. Technical report, Xerox Parc (2003)"},{"key":"9160_CR6","doi-asserted-by":"crossref","unstructured":"Ferrari, M., Fiorentini, C., Momigliano, A., Ornaghi, M.: Snapshot generation in a constructive object-oriented modeling language. In: King, A. (ed.) Logic Based Program Synthesis and Transformation, LOPSTR 2007, Selected Papers. Lecture Notes in Computer Science, vol. 4915, pp.\u00a0169\u2013184. Springer, New York (2008)","DOI":"10.1007\/978-3-540-78769-3_12"},{"key":"9160_CR7","doi-asserted-by":"crossref","unstructured":"Ferrari, M., Fiorentini, C., Ornaghi, M.: Extracting exact time bounds from logical proofs. In: Petterossi, A. (ed.) Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Selected Papers. Lecture Notes in Computer Science, vol. 2372, pp. 245\u2013265. Springer, New York (2002)","DOI":"10.1007\/3-540-45607-4_14"},{"key":"9160_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2977-2","volume-title":"Semantical Investigations in Heyting\u2019s Intuitionistic Logic","author":"DM Gabbay","year":"1981","unstructured":"Gabbay, D.M.: Semantical Investigations in Heyting\u2019s Intuitionistic Logic. Reidel, Dordrecht (1981)"},{"key":"9160_CR9","first-page":"66","volume-title":"Proceedings of the 13th International Conference on Conceptual Structures (ICCS \u201905)","author":"K Kaneiwa","year":"2005","unstructured":"Kaneiwa, K.: Negations in description logic - contraries, contradictories, and subcontraries. In: Proceedings of the 13th International Conference on Conceptual Structures (ICCS \u201905), pp. 66\u201379. Kassel University Press, Kassel (2005)"},{"key":"9160_CR10","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/0168-0072(96)00002-4","volume":"81","author":"JMJ Lipton","year":"1996","unstructured":"Lipton, J., M.J. O\u2019Donnel: Some intuitions behind realizability semantics for constructive logic: Tableaux and L\u00e4unchli countermodels. Ann. Pure Appl. Logic 81, 187\u2013239 (1996)","journal-title":"Ann. Pure Appl. Logic"},{"key":"9160_CR11","first-page":"143","volume-title":"Foundations of Logic and Functional Programming. Lecture Notes in Computer Science, vol. 306","author":"P Miglioli","year":"1986","unstructured":"Miglioli, P., Moscato, U., Ornaghi, M.: Pap: a logic programming system based on a constructive logic. In: Foundations of Logic and Functional Programming. Lecture Notes in Computer Science, vol. 306, pp. 143\u2013156. Springer, New York (1986)"},{"key":"9160_CR12","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1006\/jsco.1994.1036","volume":"18","author":"P Miglioli","year":"1994","unstructured":"Miglioli, P., Moscato, U., Ornaghi, M.: Abstract parametric classes and abstract data types defined by classical and constructive logical methods. J. Symb. Comput. 18, 41\u201381 (1994)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"9160_CR13","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1305\/ndjfl\/1093634996","volume":"30","author":"P Miglioli","year":"1989","unstructured":"Miglioli, P., Moscato, U., Ornaghi, M., Usberti, G.: A constructivism based on classical truth. Notre Dame J. Form. Log. 30(1), 67\u201390 (1989)","journal-title":"Notre Dame J. Form. Log."},{"key":"9160_CR14","doi-asserted-by":"crossref","first-page":"16","DOI":"10.2307\/2268973","volume":"14","author":"D Nelson","year":"1949","unstructured":"Nelson, D.: Constructible falsity. J. Symb. Log. 14, 16\u201326 (1949)","journal-title":"J. Symb. Log."},{"key":"9160_CR15","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/978-94-017-3598-8_11","volume-title":"Trends in Logic. 50 Years of Studia Logica","author":"SP Odintsov","year":"2003","unstructured":"Odintsov, S.P., Wansing, H.: Inconsistency-tolerant description logic. Motivation and basic systems. In: Hendricks, V., Malinowski, J. (eds.) Trends in Logic. 50 Years of Studia Logica, pp. 301\u2013335. Kluwer Academic, Dordrecht (2003)"},{"issue":"3","key":"9160_CR16","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/j.jal.2007.06.001","volume":"6","author":"SP Odintsov","year":"2008","unstructured":"Odintsov, S.P., Wansing, H.: Inconsistency-tolerant description logic. Part II: a tableau algorithm for ${{\\cal CACL}}^{\\mbox{c}}$ . Journal of Applied Logic 6(3), 343\u2013360 (2008)","journal-title":"Journal of Applied Logic"},{"key":"9160_CR17","volume-title":"Natural Deduction","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D.: Natural Deduction. Almquist and Wiksell, Stockholm (1965)"},{"key":"9160_CR18","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A.,. Tishkovsky, D.: Using tableau to decide expressive description logics with role negation. In: ISWC\/ASWC 2007. Lecture Notes in Computer Science, vol. 4825, pp. 438\u2013451 (2007)","DOI":"10.1007\/978-3-540-76298-0_32"},{"issue":"1","key":"9160_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M Schmidt-Schau\u00df","year":"1991","unstructured":"Schmidt-Schau\u00df, M., Smolka, G.: Attributive concept descriptions with complements. Artif. Intell. 48(1), 1\u201326 (1991)","journal-title":"Artif. Intell."},{"key":"9160_CR20","doi-asserted-by":"crossref","unstructured":"Smorynski, C.A.: Applications of Kripke semantics. In: Troelstra, A.S. (ed.) Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344, pp. 324\u2013391. Springer, New York (1973)","DOI":"10.1007\/BFb0066744"},{"key":"9160_CR21","doi-asserted-by":"crossref","unstructured":"Troelstra, A.S. (ed.): Metamathematical Investigation of intuitionistic arithmetic and analysis. In: Lecture Notes in Mathematics, vol. 344. Springer, New York (1973)","DOI":"10.1007\/BFb0066739"},{"issue":"1\u20132","key":"9160_CR22","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1016\/S0304-3975(97)00172-2","volume":"211","author":"AS Troelstra","year":"1999","unstructured":"Troelstra, A.S.: From constructivism to computer science. Theor. Comp. Sci. 211(1\u20132), 233\u2013252 (1999)","journal-title":"Theor. Comp. Sci."},{"key":"9160_CR23","volume-title":"Cambridge Tracts in Theoretical Computer Science, vol. 43","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic proof theory. In: Cambridge Tracts in Theoretical Computer Science, vol. 43. Cambridge University Press, Cambridge (1996)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9160-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9160-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9160-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,18]],"date-time":"2024-03-18T07:14:57Z","timestamp":1710746097000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9160-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,12,17]]},"references-count":23,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["9160"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9160-7","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,12,17]]}}}