{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:40:34Z","timestamp":1753886434379},"publisher-location":"Berlin\/Heidelberg","reference-count":16,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354019343X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012852","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"500-516","source":"Crossref","is-referenced-by-count":39,"title":["A resolution calculus for modal logics"],"prefix":"10.1007","author":[{"given":"Hans J\u00fcrgen","family":"Ohlbach","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"33_CR1","first-page":"172","volume":"86","author":"M. Abadi","year":"1986","unstructured":"M. Abadi, Z. Manna. Modal Theorem Proving. In Proc. of CADE 86, pp. 172\u2013189, 1986.","journal-title":"Proc. of CADE"},{"key":"33_CR2","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF03037397","volume":"5","author":"M. Chan","year":"1987","unstructured":"Chan, M. The Recursive Resolution Method for Modal Logic. New Generation Computing, 5, 1987, pp 155\u2013183.","journal-title":"New Generation Computing"},{"key":"33_CR3","doi-asserted-by":"crossref","unstructured":"N. Eisinger. What you always wanted to know about connection graphs. Proc. of 8th Conference on Automated Deduction, Oxford, 1985.","DOI":"10.1007\/3-540-16780-3_100"},{"key":"33_CR4","doi-asserted-by":"crossref","unstructured":"L. Fari\u00f1as del Cerro. Resolution modal logics. In Logics and Models of Concurrent Systems, (K.R. Apt, ed.), Springer 1985, pp 27\u201355.","DOI":"10.1007\/978-3-642-82453-1_2"},{"key":"33_CR5","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":"33_CR6","doi-asserted-by":"crossref","unstructured":"M.C. Fitting. Proof methods for modal and intuitionistic logics. Vol. 169 of Synthese Library, D. Reidel Publishing Company, Dordrecht, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"33_CR7","volume-title":"An Introduction to Modal Logics","author":"G.E. Hughes","year":"1968","unstructured":"G.E. Hughes, M.J. Cresswell, An Introduction to Modal Logics. Methuen & Co., London, 1968."},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"R. Kowalski: A Proof Procedure Using Connection Graphs. J.ACM Vol. 22, No.4, 1975.","DOI":"10.1145\/321906.321919"},{"key":"33_CR9","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":"33_CR10","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":"33_CR11","unstructured":"H.J. Ohlbach, A Resolution Calculus for Modal Logics. Thesis, FB Informatik, Univ. of Kaiserslautern (forthcoming 1988)."},{"issue":"1","key":"33_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A. A Machine Oriented Logic Based on the Resolution Principle. J.ACM Vol. 12, No. 1, pp 23\u201341, 1965.","journal-title":"J.ACM"},{"key":"33_CR13","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":"33_CR14","unstructured":"M. Schmidt-Schau\u00df. A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. Proc. of 9th IJCAI, Los Angeles, 1985, 1162\u20131168."},{"key":"33_CR15","unstructured":"L.A. Wallen Matrix proof methods for modal logics. In Proc. of 10th IJCAI, 1987."},{"key":"33_CR16","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","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.springerlink.com\/index\/pdf\/10.1007\/BFb0012852","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:24:07Z","timestamp":1586579047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0012852","relation":{},"subject":[]}}