{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,24]],"date-time":"2026-04-24T21:55:27Z","timestamp":1777067727047,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540193432","type":"print"},{"value":"9783540392163","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1988]]},"DOI":"10.1007\/bfb0012851","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"487-499","source":"Crossref","is-referenced-by-count":7,"title":["Linear modal deductions"],"prefix":"10.1007","author":[{"given":"Luis Fari\u00f1as","family":"del Cerro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Herzig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Abadi M., Manna Z. Modal theorem proving. 8CAD, LNCS, Springer-Verlag 1986, pp 172\u2013186.","DOI":"10.21236\/ADA325959"},{"key":"32_CR2","unstructured":"Auffray Y., Enjalbert P., Hebrard J.J., Strategics for modal resolution: results and problems. Rapport du Laboratoire d'Informatique de Caen, 1987."},{"key":"32_CR3","unstructured":"Balbiani Ph., Fari\u00f1as del Cerro L., Herzig A., Declarative semantics for modal logic programs. Rapport LSI, November 1987."},{"key":"32_CR4","unstructured":"Bieber P., Cooperating with untrusted agents. Rapport LSI, UPS, 1988."},{"key":"32_CR5","volume-title":"Une m\u00e9thode de d\u00e9duction automatique en logique modale","author":"M. Cialdea","year":"1986","unstructured":"Cialdea M., Une m\u00e9thode de d\u00e9duction automatique en logique modale. Th\u00e8se Universit\u00e9 Paul Sabatier, Toulouse, 1986."},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Enjalbert P., Fari\u00f1as del Cerro L., Modal resolution in clausal form, Theoretical Computer Sciences, to appear.","DOI":"10.1016\/0304-3975(89)90137-0"},{"key":"32_CR7","doi-asserted-by":"crossref","unstructured":"Fari\u00f1as del Cerro L., A simple deduction method for modal logic. Information Processing Letter 14, 1982.","DOI":"10.1016\/0020-0190(82)90085-0"},{"key":"32_CR8","unstructured":"Fari\u00f1as del Cerro L., Herzig A., Quantified modal logic and unification theory. Rapport LSI, UPS, 1988."},{"key":"32_CR9","unstructured":"Fari\u00f1as del Cerro L., Orlowska. E., Automated reasoning in non classical logic. Logique et Analyse, no 110\u2013111, 1985."},{"key":"32_CR10","volume-title":"Proof methods for modal and intuitionistic logics","author":"M.C. Fitting","year":"1986","unstructured":"Fitting M.C., Proof methods for modal and intuitionistic logics. Methuen & Co., London 1986."},{"key":"32_CR11","volume-title":"A companion to Modal Logic","author":"G.E. Hughes","year":"1986","unstructured":"Hughes G.E., Cresswell M.J., A companion to Modal Logic, Methuen & Co. Ltd., London 1986."},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"Konolige K., Resolution and quantified epistemic logics. 8CAD, LNCS, Springer-Verlag 1986, pp199\u2013209.","DOI":"10.1007\/3-540-16780-3_91"},{"key":"32_CR13","unstructured":"Konolige K., A deductive model of belief and its logics. Ph.D. Thesis, Computer Sciences Department, Stanford University 1984."},{"key":"32_CR14","unstructured":"Mints G., Resolution calculi for modal logics. Proc. of the Academy of Estonian SSR, 1986 (in russian)."},{"key":"32_CR15","unstructured":"Ohlbach H.J., A resolution calculus for modal logics. Report University of Kaiserslautern, 1987."},{"key":"32_CR16","unstructured":"Wallen L.A., Matrix proof methods for modal logics. In Proc. of 10th ICALP, 1987."},{"key":"32_CR17","first-page":"35","volume":"1","author":"G. Wrightson","year":"1985","unstructured":"Wrightson, G., Non-classical theorem proving. Journal of automated Reasoning, 1,35\u201337, 1985.","journal-title":"Journal of automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012851","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:23:44Z","timestamp":1586579024000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012851"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988]]},"ISBN":["9783540193432","9783540392163"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0012851","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1988]]}}}