{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:18Z","timestamp":1725663858864},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540527534"},{"type":"electronic","value":"9783540471370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52753-2_46","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:42:13Z","timestamp":1330206133000},"page":"271-308","source":"Crossref","is-referenced-by-count":0,"title":["New ways for developing proof theories for first-order multi modal logics"],"prefix":"10.1007","author":[{"given":"Hans J\u00fcrgen","family":"Ohlbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"18_CR1","unstructured":"R.S. Boyer, J.S. Moore: A Computational Logic. Academic Press 1979."},{"key":"18_CR2","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF03037397","volume":"5","author":"M. Chan","year":"1987","unstructured":"M. Chan. The Recursive Resolution Method. New Generation Computing, 5 pp. 155\u2013183, 1987.","journal-title":"New Generation Computing"},{"key":"18_CR3","volume-title":"Science and Applied Mathematics Series","author":"C.-L. Chang","year":"1973","unstructured":"C.-L. Chang, R.C.-T. Lee, Symbolic Logic and Mechanical Theorem Proving. Science and Applied Mathematics Series (ed. W. Rheinboldt), Academic Press, New York, 1973."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","first-page":"52","volume-title":"Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic","author":"M.C. Clarke","year":"1981","unstructured":"M.C. Clarke, E.A. Emerson. Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. Lecture Notes in Computer Science 131, Springer Verlag, New York, 1981, pp. 52\u201371."},{"key":"18_CR5","unstructured":"P. Enjalbert, Y. Auffray. Modal Theorem Proving: An Equational Viewpoint Submitted to IJCAI 89."},{"key":"18_CR6","unstructured":"L. Fari\u00f1as del Cerro, A.Herzig Quantified Modal Logic and Unification Theory Langages et Syst\u00e8mes Informatique, Universit\u00e9 Paul Sabatier, Toulouse. Rapport LSI no 293, jan. 1988. See also L. Fari\u00f1as del Cerro, A. Herzig Linear Modal Deductions. Proc. of 9th Conference on Automated Deduction, pp. 487\u2013499, 1988."},{"key":"18_CR7","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","volume":"XIII","author":"M.C. Fitting","year":"1972","unstructured":"M.C. Fitting. Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, XIII:237\u2013247,1972.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"M.C. Fitting. Proof methods for modal and intuitionistic logics. Vol. 169 of Synthese Library, D. Reidel Publishing Company, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"G. Gr\u00e4tzer. Universal Algebra. Springer Verlag (1979).","DOI":"10.1007\/978-0-387-77487-9"},{"key":"18_CR10","unstructured":"J.Y. Halpern and Y. Moses. A guide to modal logics of knowledge and belief: preliminary draft. In Proc. of 9th IJCAI, pp 479\u2013490, 1985."},{"key":"18_CR11","unstructured":"Herzig, A, @ PhD Thesis, Universit\u00e9 Paul Sabatier, Toulouse."},{"key":"18_CR12","volume-title":"An Introduction to Modal Logics","author":"G.E. Hughes","year":"1986","unstructured":"G.E. Hughes, M.J. Cresswell. An Introduction to Modal Logics. Methuen & Co., London, 1986."},{"key":"18_CR13","volume-title":"Knowledge and Belief","author":"J. Hintikka","year":"1962","unstructured":"J. Hintikka. Knowledge and Belief. Cornell University Press, Ithaca, New York, 1962."},{"key":"18_CR14","series-title":"Research Notes in Artificial Intelligence","volume-title":"A Deduction Model of Belief and its Logics","author":"K. Konolige","year":"1986","unstructured":"K. Konolige. A Deduction Model of Belief and its Logics. Research Notes in Artificial Intelligence, Pitman, London, 1986."},{"key":"18_CR15","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2964568","volume":"24","author":"S. Kripke","year":"1959","unstructured":"S. Kripke. A Completeness Theorem in Modal Logic. J. of Symbolic Logic, Vol 24, 1959, pp 1\u201314.","journal-title":"J. of Symbolic Logic"},{"key":"18_CR16","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S. Kripke","year":"1963","unstructured":"S. Kripke. Semantical analysis of modal logic I, normal propositional calculi. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik, Vol. 9, 1963, pp 67\u201396.","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"18_CR17","volume-title":"A logic of knowledge and active belief","author":"H.J. Levesque","year":"1984","unstructured":"H.J. Levesque. A logic of knowledge and active belief. Proc. of American Association of Artificial Intelligence, University of Texas, Austin 1984."},{"key":"18_CR18","series-title":"Fundamental Studies in Computer Science","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"D. Loveland: Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science, Vol. 6, North-Holland, New York 1978."},{"key":"18_CR19","volume-title":"Reasoning about Knowledge and Action","author":"R.C. Moore","year":"1980","unstructured":"R.C. Moore. Reasoning about Knowledge and Action. PhD Thesis, MIT, Cambridge 1980."},{"key":"18_CR20","unstructured":"H.J. Ohlbach. A Resolution Calculus for Modal Logics Thesis, FB. Informatik, University of Kaiserslautern, 1988."},{"key":"18_CR21","unstructured":"H.J. Ohlbach. Context Logic. SEKI Report SR-89-8, FB. Informatik, Univ. of Kaiserslautern."},{"issue":"1","key":"18_CR22","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"J.A. Robinson. A Machine Oriented Logic Based on the Resolution Principle J.ACM, Vol. 12, No 1, 1965, 23\u201341.","journal-title":"J.ACM"},{"key":"18_CR23","series-title":"Machine Intelligence","first-page":"135","volume-title":"Paramodulation and theorem provcing in first order theories with equality","author":"G. Robinson","year":"1969","unstructured":"Robinson, G., Wos, L. Paramodulation and theorem provcing in first order theories with equality. Machine Intelligence 4, American Elsevier, New York, pp. 135\u2013150, 1969."},{"key":"18_CR24","unstructured":"Schmidt-Schau\u00df, M. A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. Proc. of 9th IJCAI, Los Angeles, 1985, 1162\u20131168."},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Schmidt-Schau\u00df, M. Computational aspects of an order-sorted logic with term declarations. Thesis, FB. Informatik, University of Kaiserslautern, 1988.","DOI":"10.1007\/BFb0024065"},{"key":"18_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"R.M. Smullyan. First Order Logic, Springer Verlag, Berlin 1968."},{"issue":"4","key":"18_CR27","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"M. Stickel. Automated Deduction by Theory Resolution. Journal of Automated Reasoning Vol. 1, No. 4, 1985, pp 333\u2013356.","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR28","unstructured":"L.A. Wallen. Matrix proof methods for modal logics. In Proc. of 10th IJCAI, 1987."},{"key":"18_CR29","series-title":"Research Notes in Artifical Intelligence","volume-title":"A Many-sorted Calculus Based on Resolution and Paramodulation","author":"C. Walther","year":"1987","unstructured":"C. Walther: A Many-sorted Calculus Based on Resolution and Paramodulation. Research Notes in Artifical Intelligence, Pitman Ltd., London, M. Kaufmann Inc., Los Altos, 1987."}],"container-title":["Lecture Notes in Computer Science","CSL '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52753-2_46.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T18:02:34Z","timestamp":1687284154000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52753-2_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540527534","9783540471370"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/3-540-52753-2_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}