{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:25Z","timestamp":1761611305708},"reference-count":41,"publisher":"Informa UK Limited","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[2000,1]]},"DOI":"10.1080\/11663081.2000.10510994","type":"journal-article","created":{"date-parts":[[2012,5,30]],"date-time":"2012-05-30T08:15:58Z","timestamp":1338365758000},"page":"145-172","source":"Crossref","is-referenced-by-count":12,"title":["SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation"],"prefix":"10.1080","volume":"10","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"301","reference":[{"key":"CIT0001","unstructured":"Buro, M. and Buning, H. 1992. \u201cReport on a SAT competition. Technical Report 110, University of Paderborn, Germany, November\u201d."},{"key":"CIT0002","first-page":"109","volume":"4","author":"Baader F.","year":"1994","journal-title":"Applied Artificial Intelligence. Special Issue on Knowledge Base Management"},{"key":"CIT0003","volume-title":"Proc. International Workshop on Description Logics","author":"Bresciani P.","year":"1995"},{"key":"CIT0004","first-page":"67","volume-title":"Proceedings of the First International Workshop on Processing Declarative Knowledge volume 572 of Lecture Notes in Computer Science","author":"Baader F.","year":"1991"},{"key":"CIT0005","first-page":"21","volume-title":"Proc. of the 11th National Conference on Artificial Intelligence","author":"Crawford J.","year":"1993"},{"key":"CIT0006","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic\u2014an Introduction.","author":"Chellas B. F.","year":"1980"},{"key":"CIT0007","volume-title":"Computation and Proof Theory: proceedings of the Logic Colloquium, Lecture Notes in Mathematics, 1104, Aachen","author":"Denenberg L.","year":"1983"},{"issue":"7","key":"CIT0008","volume":"5","author":"Davis M.","year":"1962","journal-title":"Journal of the ACM"},{"key":"CIT0009","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"Davis M.","year":"1960","journal-title":"Journal of the ACM"},{"key":"CIT0010","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-69778-0","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'98, number 1397 in Lecture Notes in Artificial Intelligence. Springer-Verlag","author":"de Swart H.","year":"1998"},{"key":"CIT0011","first-page":"995","volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E. A.","year":"1990"},{"key":"CIT0012","volume-title":"Collected Papers from the International Description Logics Workshop (DL'98). CEUR","author":"Franconi E.","year":"1998"},{"key":"CIT0013","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics.","author":"Fitting M.","year":"1983"},{"key":"CIT0014","volume-title":"Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98)","author":"Giunchiglia E.","year":"1998"},{"key":"CIT0015","volume-title":"Proc. of the 13th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, New Brunswick, NJ, USA","author":"Giunchiglia F.","year":"1996"},{"key":"CIT0016","volume-title":"Information and Computation.","author":"Giunchiglia F.","year":"1996"},{"key":"CIT0017","volume-title":"Proc. of the 5th International Conference on Principles of Knowledge Representation and Reasoning\u2014KR'96, Cambridge, MA, USA","author":"Giunchiglia F.","year":"1996"},{"issue":"3","key":"CIT0018","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/0004-3702(95)00018-A","volume":"75","author":"Halpern J. Y.","year":"1995","journal-title":"Artificial Intelligence"},{"issue":"1","key":"CIT0019","first-page":"177","volume":"2","author":"Heuerding A.","year":"1996","journal-title":"Euromath Bulletin"},{"issue":"3","key":"CIT0020","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"Halpern J. Y.","year":"1992","journal-title":"Artificial Intelligence"},{"key":"CIT0021","doi-asserted-by":"crossref","unstructured":"Horrocks, I.The FaCT system. In de Swart [dS98]307\u2013312.","DOI":"10.1007\/3-540-69778-0_30"},{"key":"CIT0022","first-page":"636","volume-title":"Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98)","author":"Horrocks I.","year":"1998"},{"key":"CIT0023","volume-title":"Proc. of the 15th International Joint Conference on Artificial Intelligence","author":"Hustadt U.","year":"1997"},{"key":"CIT0024","unstructured":"Hustadt, U. and Schmidt, R. A. 1997. \u201cOn evaluating decision procedures for modal logic. Research report MPI-I-97-2-003, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, February\u201d."},{"key":"CIT0025","author":"Hustadt U.","year":"1998","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"3","key":"CIT0026","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"Joyner W. H.","year":"1976","journal-title":"Journal of the ACM"},{"issue":"3","key":"CIT0027","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"Ladner R.","year":"1977","journal-title":"SIAM J. Comp."},{"key":"CIT0028","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"Lewis H. R.","year":"1980","journal-title":"Journal of Computer and System Sciences"},{"key":"CIT0029","volume-title":"Proc. of the 12th Conference on Automated Deduction","author":"Massacci F.","year":"1994"},{"key":"CIT0030","first-page":"459","volume-title":"Proc. of the 10th National Conference on Artificial Intelligence","author":"Mitchell D.","year":"1992"},{"issue":"5","key":"CIT0031","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"Ohlbach H. J.","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"CIT0032","unstructured":"Patel-Schneider, P. F. 87\u201389. DLP system description. In Franconi et al. [FGM+98]"},{"key":"CIT0033","unstructured":"Schmidt, R. A. 1998. \u201cAugust\u201d. Personal communication"},{"key":"CIT0034","author":"Schmidt R. A.","year":"1998","journal-title":"Journal of Automated Reasoning"},{"key":"CIT0035","unstructured":"Sebastiani, R. and Giunchiglia, F. 1997. \u201cFrom Tableau-based to SAT- based procedures\u2014preliminary report. Technical Report 9711\u201314, IRST, Trento, Italy, November\u201d."},{"key":"CIT0036","unstructured":"Sebastiani, R. and McAllester, D. 1997. \u201cNew upper bounds for satisfiability in modal logics\u2014the case-study of modal K. Technical Report 9710\u201315, IRST, Trento, Italy, October\u201d."},{"key":"CIT0037","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic.","author":"Smullyan R. M.","year":"1968"},{"key":"CIT0038","unstructured":"Tacchella, A. 1997. \u201cProcedure di decisione per logiche modali classiche (decision procedures for classical modal logics). Master's thesis, DIST, Universit\u00e0 di Genova, Italy\u201d. In italian"},{"key":"CIT0039","first-page":"167","volume-title":"Synthese Library","author":"van Benthem Johan","year":"1984"},{"key":"CIT0040","first-page":"141","volume-title":"Lecture Notes in Artificial Intelligence","author":"Weidenbach C.","year":"1996"},{"key":"CIT0041","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0004-3702(94)90104-X","volume":"70","author":"Williams C. P.","year":"1994","journal-title":"Artificial Intelligence"}],"container-title":["Journal of Applied Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.tandfonline.com\/doi\/pdf\/10.1080\/10256018808623883","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,29]],"date-time":"2019-06-29T07:08:50Z","timestamp":1561792130000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.tandfonline.com\/doi\/abs\/10.1080\/11663081.2000.10510994"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,1]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,1]]}},"alternative-id":["10.1080\/11663081.2000.10510994"],"URL":"https:\/\/doi.org\/10.1080\/11663081.2000.10510994","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,1]]}}}