{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T21:51:33Z","timestamp":1778277093448,"version":"3.51.4"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,7,7]],"date-time":"2013-07-07T00:00:00Z","timestamp":1373155200000},"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":[[2014,3]]},"DOI":"10.1007\/s10817-013-9291-8","type":"journal-article","created":{"date-parts":[[2013,7,6]],"date-time":"2013-07-06T04:52:33Z","timestamp":1373086353000},"page":"331-360","source":"Crossref","is-referenced-by-count":5,"title":["Formally Verified Tableau-Based Reasoners for a Description Logic"],"prefix":"10.1007","volume":"52","author":[{"given":"M. J.","family":"Hidalgo-Doblado","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. A.","family":"Alonso-Jim\u00e9nez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Borrego-D\u00edaz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F. J.","family":"Mart\u00edn-Mateos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J. L.","family":"Ruiz-Reina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,7,7]]},"reference":[{"key":"9291_CR1","doi-asserted-by":"crossref","unstructured":"Aczel, P.: An introduction to inductive definitions. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp.\u00a0739\u2013782. North\u2013Holland Publishing Company (1977)","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"9291_CR2","first-page":"3","volume":"98","author":"JA 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 98, 3\u201316 (2004)","journal-title":"RACSAM (Revista de la Real Academia de Ciencias), Serie A: Matem\u00e1ticas"},{"key":"9291_CR3","doi-asserted-by":"crossref","unstructured":"Alonso, J.A., Borrego, J., Hidalgo, M.J., Mart\u00edn, F.J., Ruiz, J.L.: A formally verified prover for the ALC description logic. In: Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol.\u00a04732, pp.\u00a0135\u2013150. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_11"},{"key":"9291_CR4","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Wener, B.: Verifying SAT and SMT in Coq for a fully automated decision. In: PSATTT\u201911: International Workshop on Proof-Search in Axiomatic Theories and Type Theories (2011)"},{"key":"9291_CR5","doi-asserted-by":"crossref","unstructured":"Baader, F., Hollunder, B.: A terminological knowledge representation system with complete inference algorithms. In: Proceedings of the First International Workshop on Processing Declarative Knowledge, pp.\u00a067\u201386 (1991)","DOI":"10.1007\/BFb0013522"},{"key":"9291_CR6","unstructured":"Baader, F., McGuiness, D., Nardi, D., Patel-Schneider, P. (eds.): The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press (2003)"},{"key":"9291_CR7","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press (1979)"},{"key":"9291_CR8","unstructured":"Butler, R.W., Sjogren, J.: A PVS graph theory library. Technical report, NASA Langley (1998)"},{"key":"9291_CR9","doi-asserted-by":"crossref","unstructured":"Caldwell, J.L.: Classical propositional decidability via Nuprl proof extraction. In: Theorem Proving in Higer Order Logics. Lecture Notes in Computer Science, vol.\u00a01479, pp.\u00a0105\u2013122. Springer (1998)","DOI":"10.1007\/BFb0055132"},{"issue":"1","key":"9291_CR10","first-page":"49","volume":"3","author":"MB Caminati","year":"2010","unstructured":"Caminati, M.B.: Basic first\u2013order model theory in Mizar. J. Formalized Reasoning 3(1), 49\u201377 (2010)","journal-title":"J. Formalized Reasoning"},{"issue":"8","key":"9291_CR11","doi-asserted-by":"crossref","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. Commun. ACM 22(8), 465\u2013476 (1979)","journal-title":"Commun. ACM"},{"key":"9291_CR12","doi-asserted-by":"crossref","unstructured":"Dold, A.: Formal software development using generic development steps. PhD thesis, Ulm University (2000)","DOI":"10.1007\/3-540-39953-4_12"},{"key":"9291_CR13","doi-asserted-by":"crossref","unstructured":"Haarslev, V., M\u00f6ller, R.: RACER system description. In: International Joint Conference on Automated Reasoning, IJCAR\u20192001. Lecture Notes in Computer Science, vol.\u00a02083, pp.\u00a0701\u2013705. Springer (2001)","DOI":"10.1007\/3-540-45744-5_59"},{"key":"9291_CR14","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Formalizing basic first order model theory. In: Theorem Proving in Higher Order Logics: 11th International Conference, TPHOLs\u201998. Lecture Notes in Computer Science, vol.\u00a01497. Springer (1998)","DOI":"10.1007\/BFb0055135"},{"key":"9291_CR15","doi-asserted-by":"crossref","unstructured":"Hidalgo, M.J., Alonso, J.A., Mart\u00edn, F.J., Ruiz, J.L.: Constructing formally verified reasoners for the description logic. In: Proceedings of the 3rd international workshop on automated specification and verification of web systems (WWV 2007). Electronic Notes in Theoretical Computer Science, vol.\u00a0200, pp.\u00a087\u2013102 (2008)","DOI":"10.1016\/j.entcs.2008.04.094"},{"key":"9291_CR16","unstructured":"Horrocks, I.: Implementation and optimization techniques. In: Baader, F., McGuiness, D., Nardi, D., Patel-Schneider, P. (eds.) The Description Logic Handbook: Theory, Implementation and Applications, pp.\u00a0306\u2013346. Cambridge University Press (2003)"},{"key":"9291_CR17","unstructured":"Jones, C.B.: Systematic Software Development using VDM. Prentice\u2013Hall International (1990)"},{"key":"9291_CR18","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/s10817-009-9127-8","volume":"43","author":"F Mari\u0107","year":"2009","unstructured":"Mari\u0107, F.: Formalization and implementation of modern SAT solvers. J. Autom. Reasoning 43, 81\u2013119 (2009)","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"9291_CR19","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF03177742","volume":"32","author":"FJ 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. J. Autom. Reasoning 32(4), 287\u2013313 (2004)","journal-title":"J. Autom. Reasoning"},{"key":"9291_CR20","unstructured":"Mu\u00f1oz, C.: PVSio reference manual version 2.b. Technical report, National Institute of Aerospace (2005)"},{"key":"9291_CR21","unstructured":"Nutt, W.: Algorithms for Constraint in Deduction and Knowledge Representation. PhD thesis, Universit\u00e4t des Saarlandes, 1993."},{"key":"9291_CR22","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol.\u00a0607, pp.\u00a0748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9291_CR23","unstructured":"Owre, S., Shankar, N.: Abstract datatype in PVS. Technical report, Computer Science Laboratory, SRI International (1997)"},{"key":"9291_CR24","unstructured":"Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS language reference. Technical report, Computer Science Laboratory, SRI International (1999)"},{"key":"9291_CR25","doi-asserted-by":"crossref","unstructured":"Rademaker, A.: A Proof Theory for Description Logics. Springer (2012)","DOI":"10.1007\/978-1-4471-4002-3"},{"key":"9291_CR26","doi-asserted-by":"crossref","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol.\u00a03603, pp.\u00a0249\u2013309. Springer (2005)","DOI":"10.1007\/11541868_19"},{"key":"9291_CR27","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/BF00244278","volume":"1","author":"N Shankar","year":"1985","unstructured":"Shankar, N.: Towards mechanical metamathematics. J. Autom. Reasoning 1, 407\u2013434 (1985)","journal-title":"J. Autom. Reasoning"},{"key":"9291_CR28","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2011.03.002","volume":"269","author":"N Shankar","year":"2011","unstructured":"Shankar, N., Vaucher, M.: The mechanical verification of a DPLL-Based satisfiability solver. Electronic Notes in Theoretical Computer Science 269, 3\u201317 (2011)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"9291_CR29","unstructured":"Sirin, E., Parsia, B.: Pellet system description. In: Proceedings of the 2006 International Workshop on Description Logics (DL2004). CEUR Workshop Proceedings, vol.\u00a0189 (2006)"},{"key":"9291_CR30","unstructured":"Tobies, S.: Complexity results and practical algorithms for logics in knowledge representation. PhD thesis, RWTH\u2013Aachen University (2001)"},{"key":"9291_CR31","doi-asserted-by":"crossref","unstructured":"Tsarkov, D., Horrocks, I.: FaCT+\u2009+ description logic reasoner: system description. In: Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR\u00a02006). Lecture Notes in Artificial Intelligence, vol.\u00a04130, pp.\u00a0292\u2013297. Springer (2006)","DOI":"10.1007\/11814771_26"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9291-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-013-9291-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-013-9291-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,17]],"date-time":"2019-07-17T09:15:28Z","timestamp":1563354928000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-013-9291-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7,7]]},"references-count":31,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,3]]}},"alternative-id":["9291"],"URL":"https:\/\/doi.org\/10.1007\/s10817-013-9291-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7,7]]}}}