{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:05Z","timestamp":1725664805202},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616306"},{"type":"electronic","value":"9783540706434"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61630-6_5","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:09:21Z","timestamp":1330294161000},"page":"70-86","source":"Crossref","is-referenced-by-count":2,"title":["Labelled proofs for quantified modal logic"],"prefix":"10.1007","author":[{"given":"Alberto","family":"Artosi","sequence":"first","affiliation":[]},{"given":"Paola","family":"Benassi","sequence":"additional","affiliation":[]},{"given":"Guido","family":"Governatori","sequence":"additional","affiliation":[]},{"given":"Antonino","family":"Rotolo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"5_CR1","unstructured":"Alberto Artosi, Paola Cattabriga, and Guido Governatori. An Automated Approach to Normative Reasoning. In Joost Breuker, editor, Artificial Normative Reasoning, pages 132\u2013145, Amsterdam, 1994. ECAI'94."},{"key":"5_CR2","first-page":"60","volume-title":"ICLP'94","author":"A. Artosi","year":"1994","unstructured":"Alberto Artosi, Paola Cattabriga, and Guido Governatori. KED: A Deontic Theorem Prover. In C. Biagioli, G. Sartor, and D. Tiscornia, editors, Workshop on Legal Application of Logic Programming, ICLP'94, Firenze, IDG, 1994: 60\u201376."},{"key":"5_CR3","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y. Auffray","year":"1992","unstructured":"Y. Auffray and P. Enjalbert. Modal Theorem Proving: An Equational Viewpoint. Journal of Logic and Computation, 2, 1992: 247\u2013259.","journal-title":"Journal of Logic and Computation"},{"key":"5_CR4","first-page":"11","volume":"12","author":"A. Artosi","year":"1994","unstructured":"Alberto Artosi and Guido Governatori. Labelled Model Modal Logic. In Workshop on Automated Model Building, CADE 12, Nancy, 1994: 11\u201317.","journal-title":"CADE"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"M. Abadi and Z. Manna. Modal Theorem Proving. In J. H.Siekmann (ed.), Proceedings of 8th International Conference on Automated Deduction, LNCS, Vol. 230, Springer Verlag, 1986: 172\u2013189.","DOI":"10.21236\/ADA325959"},{"key":"5_CR6","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1093\/logcom\/4.3.285","volume":"4","author":"M. D'Agostino","year":"1994","unstructured":"Marcello D'Agostino and Marco Mondadori. The Taming of the Cut. Journal of Logic and Computation, 4, 1994: 285\u2013319.","journal-title":"Journal of Logic and Computation"},{"key":"5_CR7","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":"Melvin Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, 1983."},{"key":"5_CR8","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M. Fitting","year":"1988","unstructured":"M. Fitting. First-Order Modal Tableaux. Journal of Automated Reasoning, 4, 1988: 191\u2013213.","journal-title":"Journal of Automated Reasoning"},{"key":"5_CR9","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1093\/oso\/9780198537458.003.0006","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1","author":"M. Fitting","year":"1993","unstructured":"Melvin Fitting. Basic Modal Logic. In C.J. Hogger, Dov M. Gabbay, and J.A. Robinson (eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, volume 1. Oxford University Press, Oxford, 1993: 368\u2013448."},{"key":"5_CR10","volume-title":"Investigations in Modal and Tense Logics","author":"D. M. Gabbay","year":"1976","unstructured":"Dov M. Gabbay. Investigations in Modal and Tense Logics. Reidel, Dordrecht, 1976."},{"key":"5_CR11","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1093\/oso\/9780198537465.003.0006","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2","author":"D. M. Gabbay","year":"1994","unstructured":"Dov M. Gabbay. Classical vs Non-Classical Logics. In C.J. Hogger, Dov M. Gabbay, and J.A. Robinson (eds), Handbook of Logic in Artificial Intelligence and Logic Programming, volume 2, Oxford University Press, Oxford, 1994: 359\u2013500."},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF01058390","volume":"52","author":"I. Gent","year":"1993","unstructured":"Ian Gent. Theory Matrices (for Modal Logics) Using Alphabetical Monotonicity. Studia logica, 52, 1993: 233\u2013257.","journal-title":"Studia logica"},{"key":"5_CR13","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/3-540-59338-1_29","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods, LNAI, Vol. 918","author":"G. Governatori","year":"1995","unstructured":"Guido Governatori. Labelled Tableaux for Multi-Modal Logics. In P. Baumgartner, R. H\u00e4hnle and J. Posegga (eds.), Theorem Proving with Analytic Tableaux and Related Methods, LNAI, Vol. 918, Springer-Verlag, Berlin, 1995: 79\u201394."},{"key":"5_CR14","unstructured":"Guido Governatori. A Duplication and Loop Checking Free System for S4. In P. Miglioli, U. Moscato, D. Mundici and M. Ornaghi (eds.) 5 th Workshop on Theoprem Proving with Analytic tableaux and Related Methods (Short Popers), Technical report 154-96, Universit\u00e0 di Milano, 1996: 19\u201332."},{"key":"5_CR15","volume-title":"An Introduction to Modal Logic","author":"G.E. Hughes","year":"1968","unstructured":"G.E. Hughes and M.J. Cresswell. An Introduction to Modal Logic. Methuen, London, 1968."},{"key":"5_CR16","first-page":"177","volume-title":"A General Proof Method for Modal Predicate Logic","author":"P. Jackson","year":"1989","unstructured":"Peter Jackson and Han Reichgelt. Logic-Based Knowledge Representation. Chapter A General Proof Method for Modal Predicate Logic, MIT Press, Cambridge Mass., 1989: 177\u2013228."},{"key":"5_CR17","first-page":"83","volume":"16","author":"S. Kripke","year":"1963","unstructured":"Saul Kripke. Semantical Considerations on Modal Logics. Acta Philosophica Fennica, 16, 1963: 83\u201394.","journal-title":"Acta Philosophica Fennica"},{"key":"5_CR18","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"H. J. Ohlbach","year":"1991","unstructured":"Hans J\u00fcrgen Ohlbach. Semantic Based Translation Methods for Modal Logics. Journal of Logic and Computation, 1, 1991: 691\u2013746.","journal-title":"Journal of Logic and Computation"},{"key":"5_CR19","volume-title":"Automated Deduction in Nonclassical Logics","author":"L. Wallen","year":"1990","unstructured":"L. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, Cambridge Mass., 1990."}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61630-6_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:39:38Z","timestamp":1713634778000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61630-6_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616306","9783540706434"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61630-6_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}