{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:48Z","timestamp":1725663648372},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569442"},{"type":"electronic","value":"9783540478300"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56944-8_58","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:58:04Z","timestamp":1330257484000},"page":"253-264","source":"Crossref","is-referenced-by-count":6,"title":["Optimized translation of multi modal logic into predicate logic"],"prefix":"10.1007","author":[{"given":"Hans J\u00fcrgen","family":"Ohlbach","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/BF01448035","volume":"110","author":"W. Ackermann","year":"1935","unstructured":"Wilhelm Ackermann. Untersuchung \u00fcber das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 110:390\u2013413, 1935.","journal-title":"Mathematische Annalen"},{"issue":"3","key":"22_CR2","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1093\/logcom\/2.3.247","volume":"2","author":"Y. Auffray","year":"1992","unstructured":"Yves Auffray and Patrice Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 2(3):247\u2013297, 1992.","journal-title":"Journal of Logic and Computation"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Leo Bachmair, Harald Ganzinger, and Uwe Waldmann. Theorem proving for hierarchic first-order theories. In G. Levi and H. Kirchner, editors, Algebraic and Logic Programming, Third International Conference, pages 420\u2013434. Springer-Verlag, LNCS 632, September 1992.","DOI":"10.1007\/BFb0013841"},{"key":"22_CR4","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic: An Introduction","author":"B. F. Chellas","year":"1980","unstructured":"B. F. Chellas. Modal Logic: An Introduction. Cambridge University Press, Cambridge, 1980."},{"key":"22_CR5","volume-title":"Rapport LSI 293, Languages et Syst\u00e8mes Informatique","author":"F. Cerro del","year":"1988","unstructured":"Farinas del Cerro, Luis and Andreas Herzig. Quantified modal logic and unification theory. Rapport LSI 293, Languages et Syst\u00e8mes Informatique, Universit\u00e9 Paul Sabatier, Toulouse, 1988."},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"M. C. Fitting. Proof Methods for Modal and Intuitionistic Logics, volume 169 of Synthese Library. D. Reidel Publishing Company, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"22_CR7","series-title":"Workshops in Computing Series","first-page":"218","volume-title":"From a Hilbert calculus to its model theoretic semantics","author":"D. M. Gabbay","year":"1992","unstructured":"Dov M. Gabbay and Hans J\u00fcrgen Ohlbach. From a Hilbert calculus to its model theoretic semantics. In Krysha Broda, editor, Proc. of the 4 th UK Conference on Logic Programming, pages 218\u2013252. Imperial College, London, Springer Verlag, Workshops in Computing Series, 1992."},{"key":"22_CR8","volume-title":"A Companion to Modal Logic","author":"G.E. Hughes","year":"1984","unstructured":"G.E. Hughes and M.J. Cresswell. A Companion to Modal Logic. Methuen & Co., London, 1984."},{"key":"22_CR9","first-page":"167","volume-title":"Infinistic Methods","author":"L. Henkin","year":"1961","unstructured":"L. Henkin. Some remarks on infinitely long formulas. In Infinistic Methods, pages 167\u2013183. Pergamon Press, Oxford, 1961."},{"key":"22_CR10","volume-title":"PhD thesis","author":"A. Herzig","year":"1989","unstructured":"Andreas Herzig. Raisonnement automatique en logique modale et algorithmes d'unification. PhD thesis, Universit\u00e9 Paul-Sabatier, Toulouse, 1989."},{"key":"22_CR11","unstructured":"Ullrich Hustadt, Hans J\u00fcrgen Ohlbach, and Renate Schmidt. Qualified number restrictions and modal logic. forthcoming MPI report, 1993."},{"key":"22_CR12","first-page":"500","volume-title":"volume 310 of Lecture Notes in Computer Science","author":"H. J. Ohlbach","year":"1988","unstructured":"Hans J\u00fcrgen Ohlbach. A resolution calculus for modal logics. In Ewing Lusk and Ross Overbeek, editors, Proc. of 9 th International Conference on Automated Deduction, CADE-88 Argonne, IL, volume 310 of Lecture Notes in Computer Science, pages 500\u2013516, Berlin, Heidelberg, New York, 1988. Springer-Verlag, extended version: SEKI Report SR-88-08, FB Informatik, Universit\u00e4t Kaiserslautern, 1988."},{"key":"22_CR13","volume-title":"Filosofiska studier, nr. 13","author":"K. Segerberg","year":"1971","unstructured":"Krister Segerberg. An essay in classical modal logic (3 vols.). Filosofiska studier, nr. 13, Uppsala Universitet, Uppsala, 1971."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Harold Simmons. An algorithm for eliminating predicate variables from \u03c01\/1 sentences, 1993. To appear in Journal of Logic and Computation.","DOI":"10.1093\/logcom\/4.1.23"},{"key":"22_CR15","volume-title":"Technical Report MPI-I-92-209","author":"A. Szalas","year":"1992","unstructured":"Andrzej Szalas. On correspondence between modal and classical logic: Automated approach. Technical Report MPI-I-92-209, Max Planck Institut f\u00fcr Informatik, Saarbr\u00fccken, march 1992."},{"key":"22_CR16","volume-title":"Modal Logic and Classical Logic","author":"J. Benthem van","year":"1983","unstructured":"Johan van Benthem. Modal Logic and Classical Logic. Bibliopolis, Naples, 1983."},{"key":"22_CR17","first-page":"167","volume-title":"Handbook of Philosophical Logic, Vol. II, Extensions of Classical Logic, Synthese Library Vo. 165","author":"J. Benthem van","year":"1984","unstructured":"Johan van Benthem. Correspondence theory. In Gabbay Dov M and Franz Guenthner, editors, Handbook of Philosophical Logic, Vol. II, Extensions of Classical Logic, Synthese Library Vo. 165, pages 167\u2013248. D. Reidel Publishing Company, Dordrecht, 1984."},{"key":"22_CR18","volume-title":"Research Notes in Artificial Intelligence","author":"C. Walther","year":"1987","unstructured":"Christoph Walther. A Many-Sorted Calculus Based on Resolution and Paramodulation. Research Notes in Artificial Intelligence. Pitman Ltd., London, 1987."}],"container-title":["Lecture Notes in Computer Science","Logic Programming and Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56944-8_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:43Z","timestamp":1605647263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56944-8_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569442","9783540478300"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-56944-8_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}