{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:09:53Z","timestamp":1760141393587,"version":"build-2065373602"},"reference-count":30,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1992,3,1]],"date-time":"1992-03-01T00:00:00Z","timestamp":699408000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2012,6,2]],"date-time":"2012-06-02T00:00:00Z","timestamp":1338595200000},"content-version":"vor","delay-in-days":7398,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1992,3]]},"DOI":"10.1016\/s0747-7171(10)80002-1","type":"journal-article","created":{"date-parts":[[2010,6,4]],"date-time":"2010-06-04T04:35:34Z","timestamp":1275626134000},"page":"235-254","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":9,"title":["A resolution framework for finitely-valued first-order logics"],"prefix":"10.1016","volume":"13","author":[{"given":"Peter W.","family":"O'Hearn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zbigniew","family":"Stachniak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(10)80002-1_bib1","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-16780-3_89","article-title":"Modal theorem proving","volume":"230","author":"Abadi","year":"1986","journal-title":"Proceedings of the 8th International Conference on Automated Deduction, LNCS"},{"key":"10.1016\/S0747-7171(10)80002-1_bib2","series-title":"Modern Uses of Multiple-Valued Logic","article-title":"A useful four-valued logic","author":"Belnap","year":"1977"},{"key":"10.1016\/S0747-7171(10)80002-1_bib3","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/BF03037397","article-title":"The recursive resolution method for modal logic","volume":"5","author":"Chan","year":"1987","journal-title":"New Generation Computing"},{"year":"1991","series-title":"Proceedings of the 21th International Symposium on Multiple-Valued Logic","author":"Current","key":"10.1016\/S0747-7171(10)80002-1_bib4"},{"key":"10.1016\/S0747-7171(10)80002-1_bib5","doi-asserted-by":"crossref","first-page":"487","DOI":"10.1007\/BFb0012851","article-title":"Linear modal deductions","volume":"310","author":"L.","year":"1988","journal-title":"Proceedings of the 9th International Conference on Automated Deduction, LNCS"},{"key":"10.1016\/S0747-7171(10)80002-1_bib6","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/FI-1988-11206","article-title":"Logic programming on a topological bilattice","volume":"11","author":"Fitting","year":"1988","journal-title":"Fundamenta Informalicae"},{"key":"10.1016\/S0747-7171(10)80002-1_bib7","first-page":"27","article-title":"Matrices for predicate logics","volume":"6","author":"Hawranek","year":"1977","journal-title":"Bulletin of the Section of Logic PAN"},{"key":"10.1016\/S0747-7171(10)80002-1_bib8","first-page":"243","article-title":"Multi-valued logics","author":"Ginsberg","year":"1986"},{"key":"10.1016\/S0747-7171(10)80002-1_bib9","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S1385-7258(58)50024-9","article-title":"Remarks on sentential logics","volume":"20","author":"Los","year":"1958","journal-title":"Indagationes Mathematicae"},{"key":"10.1016\/S0747-7171(10)80002-1_bib10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/4904.4905","article-title":"Special relations in automated deduction","volume":"33","author":"Manna","year":"1986","journal-title":"JACM"},{"key":"10.1016\/S0747-7171(10)80002-1_bib11","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","article-title":"Complexity and related enhancements for automated theorem-proving programs","volume":"2","author":"McCharen","year":"1976","journal-title":"Computers and Mathematisc with Applications"},{"key":"10.1016\/S0747-7171(10)80002-1_bib12","first-page":"311","article-title":"A resolution principle for a class of many-valued logics","volume":"74\u201376","author":"Morgan","year":"1976","journal-title":"Logique et Analyse"},{"key":"10.1016\/S0747-7171(10)80002-1_bib13","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0004-3702(82)90011-X","article-title":"Completely non-clausal theorem proving","volume":"18","author":"Murray","year":"1982","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0747-7171(10)80002-1_bib14","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1111\/j.1467-8640.1988.tb00280.x","article-title":"Multivalued logics: a uniform approach to reasoning in artificial intelligence","volume":"4","author":"Mycroft","year":"1988","journal-title":"Computational Intelligence"},{"key":"10.1016\/S0747-7171(10)80002-1_bib15","first-page":"78","article-title":"A resolution framework for finitely-valued first-order logics","author":"O'Hearn","year":"1989"},{"key":"10.1016\/S0747-7171(10)80002-1_bib16","first-page":"364","article-title":"Note on theorem proving strategies for resolution counterparts of finitely-valued logic","author":"O'Hearn","year":"1989"},{"key":"10.1016\/S0747-7171(10)80002-1_bib17","first-page":"500","article-title":"A resolution calculus for modal logics","volume":"310","author":"Ohlbach","year":"1988","journal-title":"LNCS"},{"key":"10.1016\/S0747-7171(10)80002-1_bib18","first-page":"173","article-title":"Mechanical theorem proving for post logics","volume":"110\u2013111","author":"Orlowska","year":"1985","journal-title":"Logique et Analyse"},{"key":"10.1016\/S0747-7171(10)80002-1_bib19","first-page":"341","article-title":"Three-valued non-monotonic formalisms and logic programming","author":"Przymusinski","year":"1989"},{"year":"1969","series-title":"Many-Valued Logics","author":"Rescher","key":"10.1016\/S0747-7171(10)80002-1_bib20"},{"key":"10.1016\/S0747-7171(10)80002-1_bib21","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/3-540-16780-3_90","article-title":"Computational aspects of three-valued logic","volume":"230","author":"Schmitt","year":"1986","journal-title":"Proceedings of the 8th International Conference on Automated Deduction, LNCS"},{"year":"1990","series-title":"Proceedings of the 20th International Symposium on Multiple-Valued Logic","key":"10.1016\/S0747-7171(10)80002-1_bib22"},{"key":"10.1016\/S0747-7171(10)80002-1_bib23","doi-asserted-by":"crossref","first-page":"129","DOI":"10.3233\/FI-1991-14107","article-title":"Minimization of resolution proof systems","volume":"14","author":"Stachniak","year":"1991","journal-title":"Fundamenta Informaticaei"},{"key":"10.1016\/S0747-7171(10)80002-1_bib24","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/BFb0043087","article-title":"Resolution rule: an algebraic perspective","volume":"425","author":"Stachniak","year":"1988","journal-title":"Proceedings of Algebraic Logic and Universal Algebra in Computer Science Conference, Ames, LNCS"},{"key":"10.1016\/S0747-7171(10)80002-1_bib25","doi-asserted-by":"crossref","first-page":"333","DOI":"10.3233\/FI-1990-13307","article-title":"Resolution in the domain of strongly finite logics","volume":"13","author":"Stachniak","year":"1990","journal-title":"Fundamenta Informaticae"},{"key":"10.1016\/S0747-7171(10)80002-1_bib26","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1007\/BF02297262","article-title":"On products of structures for generalized logics","volume":"25","author":"Waszkiewicz","year":"1969","journal-title":"Studio Logica"},{"year":"1988","series-title":"Automated Reasoning. 33 Basic Research Problems","author":"Wos","key":"10.1016\/S0747-7171(10)80002-1_bib27"},{"key":"10.1016\/S0747-7171(10)80002-1_bib28","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","article-title":"Efficiency and completeness of the set of support strategy in theorem proving","volume":"12","author":"Wos","year":"1965","journal-title":"Journal of ACM"},{"key":"10.1016\/S0747-7171(10)80002-1_bib29","first-page":"615","article-title":"The unit preference strategy in theorem proving","author":"Wos","year":"1964"},{"year":"1988","series-title":"Theory of Logical Calculi: Basic Theory of Consequence Operations","author":"W\u00f3jcicki","key":"10.1016\/S0747-7171(10)80002-1_bib30"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717110800021?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717110800021?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:11:30Z","timestamp":1760058690000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717110800021"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,3]]},"references-count":30,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1992,3]]}},"alternative-id":["S0747717110800021"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(10)80002-1","relation":{},"ISSN":["0747-7171"],"issn-type":[{"type":"print","value":"0747-7171"}],"subject":[],"published":{"date-parts":[[1992,3]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A resolution framework for finitely-valued first-order logics","name":"articletitle","label":"Article Title"},{"value":"Journal of Symbolic Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0747-7171(10)80002-1","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1992 Academic Press Limited. Published by Elsevier Ltd. All rights reserved.","name":"copyright","label":"Copyright"}]}}