{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:27:46Z","timestamp":1659317266772},"reference-count":16,"publisher":"Informa UK Limited","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[1993,1]]},"DOI":"10.1080\/11663081.1993.10510808","type":"journal-article","created":{"date-parts":[[2012,5,30]],"date-time":"2012-05-30T03:54:25Z","timestamp":1338350065000},"page":"205-223","source":"Crossref","is-referenced-by-count":2,"title":["Herbrand style proof procedures for modal logic"],"prefix":"10.1080","volume":"3","author":[{"given":"Marta","family":"Cialdea","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"301","reference":[{"key":"CIT0001","doi-asserted-by":"crossref","unstructured":"Abadi, M. and Manna, Z. 1986.Modal theorem proving. Proc. of the 8th Inter. Conf. on Automated Deduction, Lecture Notes in Computer Science172\u2013189. Springer Verlag.","DOI":"10.1007\/3-540-16780-3_89"},{"key":"CIT0002","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1002\/malq.19860323106","volume":"32","author":"Cialdea M.","year":"1986","journal-title":"Zeitschr. f. math. Logik und Grundlagen d. Math."},{"key":"CIT0003","unstructured":"Cialdea, M. 1986. \u201cUne m\u00e9thode de d\u00e9duction automatique en logique modale. Thesis, Universit\u00e9 Paul Sabatier, Toulouse, France\u201d."},{"key":"CIT0004","unstructured":"Cialdea, M. 1987. \u201cTowards first order resolution for the modal systems T and S4. L.S.I. Technical Report, Universit\u00e9 Paul Sabatier, Toulouse, France\u201d."},{"key":"CIT0005","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0304-3975(91)90181-Z","volume":"85","author":"Cialdea M.","year":"1991","journal-title":"Theoretical Computer Science"},{"key":"CIT0006","unstructured":"Enjalbert, P. 1986. \u201cFari\u00f1as del Cerro L. Modal Resolution in clausal form. Report GRECO Programmation, R.G. 14\u201386\u201d."},{"key":"CIT0007","first-page":"83","volume-title":"J.","volume":"1","author":"Fitting M.","year":"1990"},{"key":"CIT0008","unstructured":"Geissler, C. and Konolige, K. 1986. \u201cA resolution method for quantified modal logics of knowledge and belief. Proc. of the Conf. on Theoretical Aspects of Reasoning about Knowledge, Monterey, CA\u201d. 309\u2013324."},{"key":"CIT0009","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"Gentzen G.","year":"1935","journal-title":"Mathematische Zeitschrift"},{"key":"CIT0010","unstructured":"Hughes, G. E. and Cresswell, M. J. 1968. \u201cAn Introduction to Modal Logic. Methuen & Co., London\u201d."},{"key":"CIT0011","unstructured":"Jackson, P. and Reichgelt, H. 1987. \u201cA general proof method for first-order modal logic. Proc. of the 10th Inter. Joint Conf. on Artificial Intelligence (IJCAI'87), Morgan Kaufmann, Los Altos, CA\u201d. 942\u2013944."},{"key":"CIT0012","unstructured":"Kleene, S. C. 1967. \u201cMathematical Logic. John Wiley & Sons, New York\u201d."},{"key":"CIT0013","doi-asserted-by":"crossref","unstructured":"Konolige, K. 1986.Resolution and quantified epistemic logics. Proc. of the 8th Inter. Conf. on Automated Deduction, Lecture Notes in Computer Science199\u2013208. Springer Verlag.","DOI":"10.1007\/3-540-16780-3_91"},{"key":"CIT0014","doi-asserted-by":"crossref","unstructured":"Ohlbach, H. J. 1988.A resolution calculus for modal logics. Proc. of the 9th CADE, Lecture Notes on Computer Science500\u2013516. Springer Verlag.","DOI":"10.1007\/BFb0012852"},{"key":"CIT0015","first-page":"113","volume":"9","author":"Ohnishi M.","year":"1957","journal-title":"Osaka Mathematical J."},{"key":"CIT0016","unstructured":"Takeuti, G. 1975. \u201cProof Theory. North-Holland, Amsterdam\u201d."}],"container-title":["Journal of Applied Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/www.tandfonline.com\/doi\/pdf\/10.1080\/10256018808623883","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,29]],"date-time":"2019-06-29T03:05:23Z","timestamp":1561777523000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.tandfonline.com\/doi\/abs\/10.1080\/11663081.1993.10510808"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,1]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993,1]]}},"alternative-id":["10.1080\/11663081.1993.10510808"],"URL":"https:\/\/doi.org\/10.1080\/11663081.1993.10510808","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,1]]}}}