{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,8]],"date-time":"2025-10-08T16:31:00Z","timestamp":1759941060191},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bf01058389","type":"journal-article","created":{"date-parts":[[2005,1,28]],"date-time":"2005-01-28T08:45:09Z","timestamp":1106901909000},"page":"197-232","source":"Crossref","is-referenced-by-count":3,"title":["A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics"],"prefix":"10.1007","volume":"52","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"St\ufffdphane","family":"Demri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Herment","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00302639","volume":"6","author":"Y. Auffray","year":"1990","unstructured":"Y. Auffray, P. Enjalbert andJ-J. Hebrard,Strategies for modal resolution: result and problems,Journal of Automated Reasoning 6 (1990), pp. 1?38.","journal-title":"Journal of Automated Reasoning"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"M. Abadi andZ. Manna,Modal theorem proving, inProc. CADE 8, LNCS 230, Springer-Verlag 1986.","DOI":"10.21236\/ADA325959"},{"key":"CR3","unstructured":"J. Barwise andS. Feferman (eds.),Model Theoretical Logics, Springer-Verlag 1985."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"J. Barwise,Model theoretical logics: background and aims, inModel Theoretical Logics, J. Barwise and S. Feferman (eds.), Springer-Verlag 1985, pp. 3 ? 23.","DOI":"10.1017\/9781316717158.004"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, R. Caferra andG. Chaminade,Some tools for an Inference Laboratory (ATINF),CADE-9, LNCS 310, Springer-Verlag 1988, pp. 744 ? 745.","DOI":"10.1007\/BFb0012877"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"R. Caferra, M. Herment andN. Zabel,User-oriented theorem proving with the ATINF graphic proof editor,Proc. of FAIR'91, LNAI 535, Springer-Verlag 1991 pp. 2 ? 10.","DOI":"10.1007\/3-540-54507-7_1"},{"key":"CR7","unstructured":"R. Caferra andS. Demri,Cooperation between dierct method and translation method in non-classical logics: some results in Propositional S5. Submitted."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"A, R. Cavalli andL. Farinas del Cerro,A decision method for linear temporal logic, inCADE 7, LNCS 170, R. E. Shostak (ed.) Springer-Verlag 1984, pp. 113 ? 127.","DOI":"10.1007\/BFb0047117"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF03037397","volume":"5","author":"M. C. Chan","year":"1987","unstructured":"M. C. Chan,The recursive resolution method for mosal logics New Generation Computing 5 (1987), pp. 155?183.","journal-title":"New Generation Computing"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"F. B. Chellas,Modal Logic, Cambridge University Press 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(89)90137-0","volume":"65","author":"P. Enjalbert","year":"1989","unstructured":"P. Enjalbert andL. Fari\u00f1as del Cerro,Modal resolution in clausal form Theoretical Computer Science 65 (1989), pp. 1?33.","journal-title":"Theoretical Computer Science"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"L. Fari\u00f1as del Cerro,Un principe de r\u00e9solution modale,R.A.I.R.O. Informatique th\u00e9orique 18 no 2 (1984).","DOI":"10.1051\/ita\/1984180201611"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"L. Fari\u00f1as del Cerro,Resolution modal logics, inLogics and Models of Concurrent Systems, K. R. Apt (ed.), Springer-Verlag 1985.","DOI":"10.1007\/978-3-642-82453-1_2"},{"key":"CR14","volume-title":"Machine learning, Metareasoning and Logics","author":"L. Fari\u00f1as del Cerro","year":"1989","unstructured":"L. Fari\u00f1as del Cerro andA. Herzig,Automated quantified modal logic inMachine learning, Metareasoning and Logics, P. Bradzdil and K. Konolige (eds), Kluwer Academic Publishers, Dordrecht\/Boston\/London 1989."},{"key":"CR15","volume-title":"Collection Logique Math\u00e9matique","author":"R. Feys","year":"1965","unstructured":"R. Feys,Modal Logic, edited by J. Dopp,Collection Logique Math\u00e9matique Serie B., E. Wauwelaerts, Gauhier-Villars, Paris 1965."},{"key":"CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"M. C. Fitting","year":"1983","unstructured":"M. C. Fitting,Proof Methods for Modal and Intuitionistic Logics D. Reidel Publ. Co., Dordrecht 1983."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"M. C. Fitting,First-Order Logic and Automated Theorem Proving, Springer-Verlag 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"35","DOI":"10.2307\/2272267","volume":"40","author":"R. I. Goldblatt","year":"1975","unstructured":"R. I. Goldblatt,First-Order definability in modal logic Journal of Symbolic Logic 40 (1975), Number 1, March, pp. 35?40.","journal-title":"Journal of Symbolic Logic"},{"key":"CR19","unstructured":"A. Herzig,Raisonnement automatique en logique modale et algorithmes d'unification, Th\u00e8se, Universit\u00e9 Paul-Sabatier de Toulouse, July 1989."},{"key":"CR20","unstructured":"K. Konolige,A Deduction model of Belief, Pitman 1986."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"J. Meseguer,General logics, inProc. of Logic Colloquium'87, H-D. Ebbinghaus et al. (eds.), North-Holland 1989.","DOI":"10.1016\/S0049-237X(08)70132-0"},{"key":"CR22","unstructured":"H.-J. Ohlbach,Context Logic, FB Informatik Univ. Kaiserslautern, 1989."},{"key":"CR23","doi-asserted-by":"crossref","first-page":"235","DOI":"10.3233\/FI-1980-3209","volume":"3","author":"E. Or?owska","year":"1979","unstructured":"E. Or?owska,Resolution systems and their applications I Fundamenta Informaticae 3 (1979), pp. 235?268.","journal-title":"Fundamenta Informaticae"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"333","DOI":"10.3233\/FI-1980-3306","volume":"3","author":"E. Or?owska","year":"1980","unstructured":"E. Or?owska,Resolution systems and their applications II Fundamenta Informaticae 3 (1980), pp. 333?362.","journal-title":"Fundamenta Informaticae"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"J. H. Schmerl,Transfer theorems and their applications to logics, inModel Theoretical Logics, J. Barwise and S. Feferman (eds.), Springer-Verlag 1985, pp. 177 ? 209.","DOI":"10.1017\/9781316717158.009"},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"R. M. Smullyan,First-Order Logic, Springer-Verlag 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"M. Schmidt-Schauss,Computational aspects of an order-sorted logic with term declarations, Thesis, FB Informatic Univ. Kaiserslautern, 1988.","DOI":"10.1007\/BFb0024065"},{"key":"CR28","unstructured":"P. B. Thislewaite, M. A. McRobbie andR. K. Meyer,Automated Theorem Proving in Non-Classical Logics, Pitman 1988."},{"key":"CR29","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-009-6259-0_4","volume-title":"Handbook of Philosophical Logic","author":"J. Benthem van","year":"1984","unstructured":"J. van Benthem,Correspondence theory inHandbook of Philosophical Logic D. Gabbay and F. Guenthner (eds.) Vol. II. D. Reidel Publ. Co., Dordrecht 1984, pp. 167?247."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01058389.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01058389\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01058389","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,4]],"date-time":"2021-07-04T10:32:14Z","timestamp":1625394734000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01058389"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":29,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF01058389"],"URL":"https:\/\/doi.org\/10.1007\/bf01058389","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}