{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:25Z","timestamp":1725475885684},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_16","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"175-189","source":"Crossref","is-referenced-by-count":1,"title":["Variants of First-Order Modal Logics"],"prefix":"10.1007","author":[{"given":"Marta","family":"Cialdea Mayer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Serenella","family":"Cerrito","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-16780-3_89","volume-title":"8th International Conference on Automated Deduction","author":"M. Abadi","year":"1986","unstructured":"Abadi, M., Manna, Z.: Modal theorem proving. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 172\u2013189. Springer, Heidelberg (1986)"},{"key":"16_CR2","unstructured":"Artosi, A., Benassi, P., Governatori, G., Rotolo, A.: Shakespearian modal logic: A labelled treatment of modal identity. Advances in Modal Logic, 1\u201321 (1998)"},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y. Auffray","year":"1992","unstructured":"Auffray, Y., Enjalbert, P.: Modal theorem proving: an equational viewpoint. J. of Logic and Computation\u00a02, 247\u2013297 (1992)","journal-title":"J. of Logic and Computation"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/3-540-59338-1_38","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"M. Baaz","year":"1995","unstructured":"Baaz, M., Ferm\u00fcller, C.G.: Non-elementary speedups between different versions of tableaux. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS, vol.\u00a0918, pp. 217\u2013230. Springer, Heidelberg (1995)"},{"issue":"3","key":"16_CR5","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1008278803780","volume":"7","author":"D. Basin","year":"1998","unstructured":"Basin, D., Matthews, M., Vigan\u00f2, L.: Labelled modal logics: Quantifiers. J. of Logic, Language and Information\u00a07(3), 237\u2013263 (1998)","journal-title":"J. of Logic, Language and Information"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/BFb0022559","volume-title":"Computational Logic and Proof Theory","author":"B. Beckert","year":"1993","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: The even more liberalized \u03b4-rule in free variable semantic tableaux. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol.\u00a0713, pp. 108\u2013119. Springer, Heidelberg (1993)"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0304-3975(91)90181-Z","volume":"85","author":"M. Cialdea","year":"1991","unstructured":"Cialdea, M.: Resolution for some first order modal systems. Theoretical Computer Science\u00a085, 213\u2013229 (1991)","journal-title":"Theoretical Computer Science"},{"key":"16_CR8","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1002\/malq.19860323106","volume":"32","author":"M. Cialdea","year":"1986","unstructured":"Cialdea, M., Fari\u00f1as del Cerro, L.: A modal Herbrand\u2019s property. Z. Math. Logik Grundlag. Math.\u00a032, 523\u2013539 (1986)","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"16_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. Fitting","year":"1983","unstructured":"Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. Reidel Publ. Co., Dordrechtz (1983)"},{"key":"16_CR10","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. Fitting","year":"1988","unstructured":"Fitting, M.: First-order modal tableaux. J. of Automated Reasoning\u00a04, 191\u2013213 (1988)","journal-title":"J. of Automated Reasoning"},{"key":"16_CR11","doi-asserted-by":"crossref","first-page":"105","DOI":"10.3233\/FI-1999-391206","volume":"39","author":"M. Fitting","year":"1999","unstructured":"Fitting, M.: On quantified modal logic. Fundamenta Informaticae\u00a039, 105\u2013121 (1999)","journal-title":"Fundamenta Informaticae"},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/978-94-009-6259-0_5","volume-title":"Handbook of Philosophical Logic","author":"J.W. Garson","year":"1984","unstructured":"Garson, J.W.: Quantification in modal logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol.\u00a0II, pp. 249\u2013307. Reidel Publ. Co., Dordrechtz (1984)"},{"key":"16_CR13","volume-title":"Handbook of tableau methods","author":"R. Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, G., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of tableau methods. Kluwer, Dordrecht (1999)"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\u00e4hnle","year":"1994","unstructured":"H\u00e4hnle, R., Schmitt, P.H.: The liberalized \u03b4-rule in free variable semantic tableaux. J. of Automated Reasoning\u00a013, 211\u2013222 (1994)","journal-title":"J. of Automated Reasoning"},{"key":"16_CR15","first-page":"942","volume-title":"IJCAI 1987","author":"P. Jackson","year":"1987","unstructured":"Jackson, P., Reichgelt, H.: A general proof method for first-order modal logic. In: IJCAI 1987, pp. 942\u2013944. Morgan Kaufmann, San Francisco (1987)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/3-540-16780-3_91","volume-title":"8th International Conference on Automated Deduction","author":"K. Konolige","year":"1986","unstructured":"Konolige, K.: Resolution and quantified epistemic logics. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol.\u00a0230, pp. 199\u2013208. Springer, Heidelberg (1986)"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"671","DOI":"10.1023\/A:1017948105274","volume":"26","author":"G. Mints","year":"1997","unstructured":"Mints, G.: Indexed systems of sequents and cut-elimination. J. of Philosophical Logic\u00a026, 671\u2013696 (1997)","journal-title":"J. of Philosophical Logic"},{"issue":"5","key":"16_CR18","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"H.J. Ohlbach","year":"1991","unstructured":"Ohlbach, H.J.: Semantics based translation methods for modal logics. J. of Logic and Computation\u00a01(5), 691\u2013746 (1991)","journal-title":"J. of Logic and Computation"},{"key":"16_CR19","volume-title":"Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics","author":"L.A. Wallen","year":"1990","unstructured":"Wallen, L.A.: Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics. MIT Press, Cambridge (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T11:21:25Z","timestamp":1587295285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/10722086_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}