{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,27]],"date-time":"2025-09-27T13:19:52Z","timestamp":1758979192897,"version":"3.41.0"},"reference-count":12,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,4,1]],"date-time":"2000-04-01T00:00:00Z","timestamp":954547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,4,1]],"date-time":"2000-04-01T00:00:00Z","timestamp":954547200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2000,4]]},"DOI":"10.1023\/a:1006249507577","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T01:20:41Z","timestamp":1040520041000},"page":"297-317","source":"Crossref","is-referenced-by-count":33,"title":["A Benchmark Method for the Propositional Modal Logics K, KT, S4"],"prefix":"10.1007","volume":"24","author":[{"given":"Peter","family":"Balsiger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Heuerding","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Schwendimann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"232628_CR1","doi-asserted-by":"crossref","unstructured":"Balsiger, P. and Heuerding, A.: Comparison of theorem provers for modal logics-introduction and summary, in H. de Swart (ed.), TABLEAUX\u2019 98, LNAI 1397, 1998, pp. 25-26.","DOI":"10.1007\/3-540-69778-0_4"},{"key":"232628_CR2","doi-asserted-by":"crossref","first-page":"489","DOI":"10.1007\/BF01880326","volume":"7","author":"L. Catach","year":"1991","unstructured":"Catach, L.: Tableaux: A general theorem prover for modal logics, J. Automated Reasoning\n7 (1991), 489-510.","journal-title":"J. Automated Reasoning"},{"key":"232628_CR3","doi-asserted-by":"crossref","unstructured":"de Swart, H. (ed.): Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX\u2019 98, LNAI 1397, Springer, 1998.","DOI":"10.1007\/3-540-69778-0"},{"issue":"1","key":"232628_CR4","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1080\/11663081.1995.10510844","volume":"5","author":"S. Demri","year":"1995","unstructured":"Demri, S.: Uniform and non uniform strategies for tableaux calculi for modal logics, J. Appl. Non-Classical Logics\n5(1) (1995), 77-96.","journal-title":"J. Appl. Non-Classical Logics"},{"key":"232628_CR5","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F. and Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures-the case study of modal K, in CADE 96, LNCS, 1996.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"232628_CR6","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J. Halpern","year":"1992","unstructured":"Halpern, J. and Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief, Artif. Intell.\n54 (1992), 319-379.","journal-title":"Artif. Intell."},{"key":"232628_CR7","doi-asserted-by":"crossref","unstructured":"Heuerding, A., J\u00e4ger, G., Schwendimann, S. and Seyfried, M.: Propositional logics on the computer, in P. Baumgartner, R. H\u00e4hnle, and J. Posegga (eds.), Tableaux 95, LNCS 918, 1995, pp. 310-323.","DOI":"10.1007\/3-540-59338-1_44"},{"key":"232628_CR8","doi-asserted-by":"crossref","unstructured":"Heuerding, A. and Schwendimann, S.: On the modal logic K plus theories, in H. Kleine B\u00fcning (eds.), CSL 95, LNCS 1092, 1996, pp. 308-319.","DOI":"10.1007\/3-540-61377-3_45"},{"key":"232628_CR9","doi-asserted-by":"crossref","unstructured":"Heuerding, A., Seyfried, M. and Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics, in P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi (eds.), Tableaux 96, LNCS 1071, 1996, pp. 210-225.","DOI":"10.1007\/3-540-61208-4_14"},{"key":"232628_CR10","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. Pelletier","year":"1986","unstructured":"Pelletier, F.: Seventy-five problems for testing automatic theorem provers, J. Automated Reasoning\n2 (1986), 191-216.","journal-title":"J. Automated Reasoning"},{"key":"232628_CR11","unstructured":"Selman, B., Levesque, H. and Mitchell, D.: A new method for solving hard satisfiability problems, in Proceedings 10th AAAI, 1992, pp. 47-59."},{"key":"232628_CR12","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, S. and Yemenis, T.: The TPTP problem library, in A. Bundy (ed.), CADE 12, LNCS 814, 1994, pp. 252-266.","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006249507577.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006249507577\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006249507577.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:10Z","timestamp":1749123910000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006249507577"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,4]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,4]]}},"alternative-id":["232628"],"URL":"https:\/\/doi.org\/10.1023\/a:1006249507577","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2000,4]]}}}