{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:06:47Z","timestamp":1762297607492},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_36","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"412-426","source":"Crossref","is-referenced-by-count":17,"title":["A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae"],"prefix":"10.1007","author":[{"given":"Renate A.","family":"Schmidt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ullrich","family":"Hustadt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"36_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF00173700","volume":"5","author":"G. Giacomo De","year":"1996","unstructured":"De Giacomo, G.: Eliminating \u201cconverse\u201d from converse PDL. J. Logic, Language and Inform.\u00a05(2), 193\u2013208 (1996)","journal-title":"J. Logic, Language and Inform."},{"issue":"3","key":"36_CR2","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H. Nivelle De","year":"2000","unstructured":"De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic J. IGPL\u00a08(3), 265\u2013292 (2000)","journal-title":"Logic J. IGPL"},{"issue":"6","key":"36_CR3","doi-asserted-by":"publisher","first-page":"933","DOI":"10.1093\/logcom\/11.6.933","volume":"11","author":"S. Demri","year":"2001","unstructured":"Demri, S.: The complexity of regularity in grammar logics and related modal logics. Journal of Logic and Computation\u00a011(6), 933\u2013960 (2001)","journal-title":"Journal of Logic and Computation"},{"key":"36_CR4","unstructured":"Demri, S., de Nivelle, H.: Deciding regular grammar logics with converse through first-order logic (2002) (manuscript)"},{"key":"36_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-48660-7_2","volume-title":"Automated Deduction - CADE-16","author":"S. Demri","year":"1999","unstructured":"Demri, S., Gor\u00e9, R.: Tractable transformations from modal provability logics into first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 16\u201330. Springer, Heidelberg (1999)"},{"key":"36_CR6","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0003-4843(75)90004-2","volume":"8","author":"D.M. Gabbay","year":"1975","unstructured":"Gabbay, D.M.: Decidability results in non-classical logics. Ann. Math. Logic\u00a08, 237\u2013295 (1975)","journal-title":"Ann. Math. Logic"},{"key":"36_CR7","first-page":"24","volume-title":"Proc. LICS","author":"H. Ganzinger","year":"1999","unstructured":"Ganzinger, H., Meyer, C., de Nivelle, H.: The two-variable guarded fragment with transitive relations. In: Proc. LICS, pp. 24\u201334. IEEE Computer Society, Los Alamitos (1999)"},{"key":"36_CR8","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/10720084_6","volume-title":"Frontiers of Combining Systems","author":"U. Hustadt","year":"2000","unstructured":"Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M.: Normal forms and proofs in combined modal and temporal logics. In: Kirchner, H. (ed.) FroCos 2000. LNCS (LNAI), vol.\u00a01794, pp. 73\u201387. Springer, Heidelberg (2000)"},{"key":"36_CR9","first-page":"110","volume-title":"Proc. IJCAI 1999","author":"U. Hustadt","year":"1999","unstructured":"Hustadt, U., Schmidt, R.A.: On the relation of resolution and tableaux proof systems for description logics. In: Proc. IJCAI 1999, pp. 110\u2013115. Morgan Kaufmann, San Francisco (1999)"},{"key":"36_CR10","series-title":"Studies in Logic","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(99)80001-9","volume-title":"Tools and Techniques in Modal Logic","author":"M. Kracht","year":"1999","unstructured":"Kracht, M.: Tools and Techniques in Modal Logic. Studies in Logic, vol.\u00a0142. Elsevier, Amsterdam (1999)"},{"issue":"6","key":"36_CR11","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1093\/logcom\/11.6.879","volume":"11","author":"M. Kracht","year":"2001","unstructured":"Kracht, M.: Reducing modal consequence relations. J. Logic Computat.\u00a011(6), 879\u2013907 (2001)","journal-title":"J. Logic Computat."},{"key":"36_CR12","unstructured":"Kracht, M.: Notes on the space requirements for checking satisfiability in modal logics. To appear in Advances in Modal Logic 4 (2002)"},{"key":"36_CR13","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/3-540-48242-3_12","volume-title":"Logic Programming and Automated Reasoning","author":"C. Lutz","year":"1999","unstructured":"Lutz, C.: Complexity of terminological reasoning revisited. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol.\u00a01705, pp. 181\u2013200. Springer, Heidelberg (1999)"},{"key":"36_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/BFb0054261","volume-title":"Automated Deduction - CADE-15","author":"H.J. Ohlbach","year":"1998","unstructured":"Ohlbach, H.J.: Combining Hilbert style and semantic reasoning in a resolution framework. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol.\u00a01421, pp. 205\u2013219. Springer, Heidelberg (1998)"},{"key":"36_CR15","doi-asserted-by":"crossref","unstructured":"Schmidt, R.A., Hustadt, U.: A principle for incorporating axioms into the firstorder translation of modal formulae. Preprint CSPP-22, Univ. Manchester, UK (2003)","DOI":"10.1007\/978-3-540-45085-6_36"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_36","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,5]],"date-time":"2019-06-05T22:12:02Z","timestamp":1559772722000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}