{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:12Z","timestamp":1725490092646},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_11","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"135-150","source":"Crossref","is-referenced-by-count":3,"title":["A Formally Verified Prover for the $\\mathcal{ALC\\,}$ Description Logic"],"prefix":"10.1007","author":[{"given":"Jos\u00e9-Antonio","family":"Alonso","sequence":"first","affiliation":[]},{"given":"Joaqu\u00edn","family":"Borrego-D\u00edaz","sequence":"additional","affiliation":[]},{"given":"Mar\u00eda-Jos\u00e9","family":"Hidalgo","sequence":"additional","affiliation":[]},{"given":"Francisco-Jesus","family":"Mart\u00edn-Mateos","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9-Luis","family":"Ruiz-Reina","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","volume-title":"Handbook of Mathematical Logic","author":"P. Aczel","year":"1977","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 739\u2013782. North\u2013Holland Publishing Company, Amsterdam (1977)"},{"issue":"1","key":"11_CR2","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/MIS.2006.7","volume":"21","author":"J.A. Alonso","year":"2006","unstructured":"Alonso, J.A., Borrego, J., Ch\u00e1vez, A.M., Mart\u00edn, F.J.: Foundational challenges in automated semantic web data and ontology cleaning. IEEE Intelligent Systems\u00a021(1), 45\u201352 (2006)","journal-title":"IEEE Intelligent Systems"},{"key":"11_CR3","first-page":"3","volume":"98","author":"J.A. Alonso","year":"2004","unstructured":"Alonso, J.A., Borrego, J., Hidalgo, M.J., Mart\u00edn, F.J., Ruiz, J.L.: Verification of the Formal Concept Analysis. RACSAM (Revista de la Real Academia de Ciencias), Serie A: Matem\u00e1ticas\u00a098, 3\u201316 (2004)","journal-title":"RACSAM (Revista de la Real Academia de Ciencias), Serie A: Matem\u00e1ticas"},{"key":"11_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1007\/978-3-540-32254-2_14","volume-title":"Mechanizing Mathematical Reasoning","author":"F. Baader","year":"2005","unstructured":"Baader, F., Horrocks, I., Sattler, U.: Description logics as ontology languages for the semantic web. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol.\u00a02605, pp. 228\u2013248. Springer, Heidelberg (2005)"},{"volume-title":"The Description Logic Handbook: Theory, Implementation and Applications","year":"2003","key":"11_CR5","unstructured":"Baader, F., McGuiness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press, Cambridge (2003)"},{"key":"11_CR6","unstructured":"Bechhofer, S., Harmelen, F.v., Hendler, J., McGuinness, I.H.D.L., Patel-Schneider, P.F., Stein, L.A.: OWL Web Ontology Language Reference (2004), available on the Web at \n                  \n                    http:\/\/www.w3.org\/TR\/owl-ref"},{"key":"11_CR7","unstructured":"Butler, R.W., Sjogren, J.: A PVS graph theory library. Technical report, NASA Langley (1998)"},{"issue":"6","key":"11_CR8","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s00200-006-0020-y","volume":"17","author":"S. Coupet-Grimal","year":"2006","unstructured":"Coupet-Grimal, S., Delobel, W.: An effective proof of the well\u2013foundedness of the multiset path ordering. Applicable Algebra in Engineering, Communication and Computing\u00a017(6), 453\u2013469 (2006)","journal-title":"Applicable Algebra in Engineering, Communication and Computing"},{"issue":"8","key":"11_CR9","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM\u00a022(8), 465\u2013476 (1979)","journal-title":"Communications of the ACM"},{"key":"11_CR10","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, pp. 701\u2013705. Springer, Heidelberg (2001)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1998","unstructured":"Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) Theorem Proving in Higher Order Logics. LNCS, vol.\u00a01479, Springer, Heidelberg (1998)"},{"issue":"4","key":"11_CR12","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1016\/j.websem.2004.06.003","volume":"1","author":"I. Horrocks","year":"2004","unstructured":"Horrocks, I., Patel-Schneider, P.: Reducing OWL entailment to description logic satisfiability. J. of Web Semantics\u00a01(4), 345\u2013357 (2004)","journal-title":"J. of Web Semantics"},{"issue":"1","key":"11_CR13","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/j.websem.2003.07.001","volume":"1","author":"I. Horrocks","year":"2003","unstructured":"Horrocks, I., Patel-Schneider, P.F., van Harmelen, F.: From \n                  \n                    \n                  \n                  $\\mathcal{SHIQ}$\n                 and RDF to OWL: The making of a Web Ontology Language. J. of Web Semantics\u00a01(1), 7\u201326 (2003)","journal-title":"J. of Web Semantics"},{"issue":"4","key":"11_CR14","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF03177742","volume":"32","author":"F.J. Mart\u00edn","year":"2004","unstructured":"Mart\u00edn, F.J., Alonso, J.A., Hidalgo, M.J., Ruiz, J.L.: Formal verification of a generic framework to synthesize SAT\u2013provers. Journal of Automated Reasoning\u00a032(4), 287\u2013313 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/3-540-44755-5_21","volume-title":"Theorem Proving in Higher Order Logics","author":"I. Medina","year":"2001","unstructured":"Medina, I., Palomo, F., Alonso, J.A.: A certified polynomial-based decision procedure for propositional logic. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 297\u2013312. Springer, Heidelberg (2001)"},{"key":"11_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-540-30210-0_15","volume-title":"Artificial Intelligence and Symbolic Computation","author":"I. Medina","year":"2004","unstructured":"Medina, I., Palomo, F., Alonso, J.A., Ruiz, J.L.: Verified computer algebra in ACL2. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 171\u2013184. Springer, Heidelberg (2004)"},{"key":"11_CR17","unstructured":"Nipkow, T.: An inductive proof of the wellfoundedness of the multiset order. A proof due to W. Buchholz (1998), available on the Web at \n                  \n                    http:\/\/www4.informatik.tu-muenchen.de\/~nipkow\/misc\/multiset.ps"},{"key":"11_CR18","unstructured":"Nutt, W.: Algorithms for constraint in deduction and knowledge representation. PhD thesis, Universit\u00e4t des Saarlandes (1993)"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"11_CR20","unstructured":"Owre, S., Shankar, N.: Abstract datatype in PVS. Technical report, Computer Science Laboratory, SRI International (1997)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/11541868_19","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 294\u2013309. Springer, Heidelberg (2005)"},{"issue":"3","key":"11_CR22","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1023\/A:1016003314081","volume":"36","author":"J.L. Ruiz","year":"2002","unstructured":"Ruiz, J.L., Alonso, J.A., Hidalgo, M.J., Mart\u00edn, F.J.: Formal proofs about rewriting using ACL2. Ann. Math. Artif. Intell.\u00a036(3), 239\u2013262 (2002)","journal-title":"Ann. Math. Artif. Intell."},{"key":"11_CR23","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-94-017-0253-9_9","volume-title":"Thirty Five Years of Automating Mathematics","author":"J.L. Ruiz","year":"2003","unstructured":"Ruiz, J.L., Alonso, J.A., Hidalgo, M.J., Mart\u00edn, F.J.: Termination in ACL2 using multiset relation. In: Kamareddine, F.D. (ed.) Thirty Five Years of Automating Mathematics, pp. 217\u2013245. Kluwer Academic Publishers, Dordrecht (2003)"},{"issue":"1","key":"11_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt\u2013Schau\u00df","year":"1991","unstructured":"Schmidt\u2013Schau\u00df, M., Smolka, G.: Attributive concept descriptions with complements. Artificial Intelligence\u00a048(1), 1\u201326 (1991)","journal-title":"Artificial Intelligence"},{"key":"11_CR25","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)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:28:05Z","timestamp":1619519285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}