{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T16:10:36Z","timestamp":1725466236954},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646754"},{"type":"electronic","value":"9783540691105"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054261","type":"book-chapter","created":{"date-parts":[[2006,6,7]],"date-time":"2006-06-07T07:28:51Z","timestamp":1149665331000},"page":"205-219","source":"Crossref","is-referenced-by-count":11,"title":["Combining Hilbert style and semantic reasoning in a resolution framework"],"prefix":"10.1007","author":[{"given":"Hans J\u00fcrgen","family":"Ohlbach","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"issue":"2","key":"22_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0898-1221(94)00217-9","volume":"29","author":"C. Brink","year":"1994","unstructured":"Chris Brink, Dov Gabbay, and Hans J\u00fcrgen Ohlbach. Towards Automating Duality. Journal of Computers and Mathematics with Applications, 29(2):73\u201390, 1994.","journal-title":"Journal of Computers and Mathematics with Applications"},{"key":"22_CR2","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."},{"doi-asserted-by":"crossref","unstructured":"Dov M. Gabbay. Self fibring in predicate logics, fibred semantics and the weaving of logics, part 4, 1996. manuscript.","key":"22_CR3","DOI":"10.1007\/978-94-009-0349-4_1"},{"unstructured":"Dov M. Gabbay and Hans J\u00fcrgen Ohlbach. Quantifier elimination in second-order predicate logic. In Bernhard Nebel, Charles Rich, and William Swartout, editors, Principles of Knowledge Representation and Reasoning (KR92), pages 425\u2013435. Morgan Kaufmann, 1992.","key":"22_CR4"},{"unstructured":"Maria Manzano. Extensions of First Order Logic. Cambridge Tracts in Theoretical Computer Science 19, Cambridge University Press, 1996.","key":"22_CR5"},{"doi-asserted-by":"crossref","unstructured":"Williman McCune and Larry Wos. Experiments in automated deduction with condensed detachment. In Deepak Kapur, editor, Automated Deduction \u2014 CADE 11, Lecture Notes in AI, vol. 607, pages 209\u2013223. Springer Verlag, 1992.","key":"22_CR6","DOI":"10.1007\/3-540-55602-8_167"},{"key":"22_CR7","volume-title":"PhD thesis","author":"A. Nonnengart","year":"1995","unstructured":"Andreas Nonnengart. A Resolution-Based Calculus for Temporal Logics. PhD thesis, Universit\u00c4t des Saarlandes, Saarbr\u00fccken, Germany, December 1995."},{"issue":"5","key":"22_CR8","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. Semantics based translation methods for modal logics. Journal of Logic and Computation, 1(5):691\u2013746, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"22_CR9","volume-title":"PhD thesis","author":"R. A. Schmidt","year":"1997","unstructured":"Renate A. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, 1997."},{"key":"22_CR10","first-page":"167","volume-title":"Handbook of Philosophical Logic, Vol. II, Extensions of Classical Logic, Synthese Library Vol. 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 Vol. 165, pages 167\u2013248. D. Reidel Publishing Company, Dordrecht, 1984."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-15"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054261","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,19]],"date-time":"2019-04-19T06:45:52Z","timestamp":1555656352000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054261"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646754","9783540691105"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/bfb0054261","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}