{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:05:49Z","timestamp":1749125149247},"reference-count":17,"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\/bf01058390","type":"journal-article","created":{"date-parts":[[2005,1,28]],"date-time":"2005-01-28T08:45:09Z","timestamp":1106901909000},"page":"233-257","source":"Crossref","is-referenced-by-count":5,"title":["Theory matrices (for modal logics) using alphabetical monotonicity"],"prefix":"10.1007","volume":"52","author":[{"given":"Ian P.","family":"Gent","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"Peter B. Andrews","year":"1981","unstructured":"Peter B. Andrews,Theorem proving via general matings Journal of the Association for Computing Machinery 28 (1981), pp. 193?214.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"CR2","first-page":"441","volume-title":"Modal theorem proving, an equationa viewpoint","author":"Yves Auffray","year":"1989","unstructured":"Yves Auffray andPatrice Enjalbert,Modal theorem proving, an equationa viewpoint Proceedings of the International Joint Conference on Artificial Intelligence Morgan Kaufmann, San Mateo, CA 1989, pp. 441?445."},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Wolfgang Bibel,Automated Theorem Proving, Vieweg, second edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"CR4","unstructured":"R. S. Boyer andJ. S. Moore,The sharing of structure in theorem-proving programs, inMachine Intelligence 7, B. Meltzer and D. Michie (eds), Edinburgh University Press, 1972, pp. 101 ? 116."},{"key":"CR5","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/3-540-52885-7_87","volume-title":"10th International Conference on Automated Deduction","author":"Hans-Jurgen Burckert","year":"1990","unstructured":"Hans-Jurgen Burckert,A resolution principle for clauses with constraints in10th International Conference on Automated Deduction M. E. Stickel (ed.), Springer-Verlag, Berlin 1990, pp. 178?192."},{"key":"CR6","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","volume":"13","author":"Melvin Fitting","year":"1972","unstructured":"Melvin Fitting,Tableau methods of proof for modal logics Notre Dame Journal of Formal Logic 13 (1972), pp. 237?247.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof Methods for Modal and Intuitionistic Logics","author":"Melvin Fitting","year":"1983","unstructured":"Melvin Fitting,Proof Methods for Modal and Intuitionistic Logics D. Reidel Publ. Co., Dordrecht 1983."},{"key":"CR8","volume-title":"Proceedings of the First International Conference on Principles of Knowledge Representation and Reasoning","author":"Alan M. Frisch","year":"1989","unstructured":"Alan M. Frisch,A general framework for sorted deduction: fundamental results on hybrid reasoning inProceedings of the First International Conference on Principles of Knowledge Representation and Reasoning, R. J. Brachman, H. Levesque & R. Reiter (eds), Morgan Kaufmann, San Mateo, CA 1989. Revised version inArtificial Intelligence vol. 49 (1991), pp. 161 ? 198."},{"key":"CR9","volume-title":"Principles of Knowledge Representation and Reasoning: Proceedings of the Second International Conference","author":"Alan M. Frisch","year":"1991","unstructured":"Alan M. Frisch andRichard B. Scherl,A general framework for modal de duction inPrinciples of Knowledge Representation and Reasoning: Proceedings of the Second International Conference, J. A. Allen, R. Fikes & E. Sandewall (eds), Morgan Kaufmann, San Mateo, CA 1991."},{"key":"CR10","volume-title":"Analytic Proof Systems for Classical and Modal Logics of Restricted Quantification","author":"Ian P. Gent","year":"1991","unstructured":"Ian P. Gent,Analytic Proof Systems for Classical and Modal Logics of Restricted Quantification PhD thesis, Warwick University, Coventry, England, in preparation, 1991."},{"key":"CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-96826-6","volume-title":"Foundations of Logic Programming","author":"J. W. Lloyd","year":"1984","unstructured":"J. W. Lloyd,Foundations of Logic Programming Springer-Verlag, Berlin 1984."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"852","DOI":"10.1109\/TC.1976.1674704","volume":"C-25","author":"Charles G. Morgan","year":"1976","unstructured":"Charles G. Morgan,Methods for automated theorem proving in nonclassical logics IEEE Tansactions on Computers C-25 (1976), pp. 852?862.","journal-title":"IEEE Tansactions on Computers"},{"key":"CR13","first-page":"444","volume-title":"Logics in AI","author":"Uwe Petermann","year":"1990","unstructured":"Uwe Petermann,Towards a connection procedure with built in theories inLogics in AI, J. van Eijck (ed.), Springer-Verlag, Berlin 1990, pp. 444?453."},{"key":"CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R. M. Smullyan","year":"1968","unstructured":"R. M. Smullyan,First Order Logic Springer-Verlag, Berlin 1968."},{"key":"CR15","first-page":"333","volume":"1","author":"Mark E. Stickel","year":"1985","unstructured":"Mark E. Stickel,Automated deduction by theory resolution Journal of Automated Reasoning,1 (1985), pp. 333?355.","journal-title":"Journal of Automated Reasoning,"},{"key":"CR16","first-page":"35","volume-title":"Artificial Intelligence and its Applications","author":"Lincoln A. Wallen","year":"1986","unstructured":"Lincoln A. Wallen,Generating connection calculi from tableau and sequent based proof systems inArtificial Intelligence and its Applications A. G. Cohn & J. R. Thomas (eds), John Wiley & Sons, Chichester 1986, pp. 35?50."},{"key":"CR17","volume-title":"Automated Deduction in Nonclassical Logics","author":"Lincoln A. Wallen","year":"1989","unstructured":"Lincoln A. Wallen,Automated Deduction in Nonclassical Logics MIT Press, Cambridge, Massachusetts 1989."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01058390.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01058390\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01058390","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T13:09:04Z","timestamp":1586092144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01058390"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":17,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF01058390"],"URL":"https:\/\/doi.org\/10.1007\/bf01058390","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}