{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,3,5]],"date-time":"2023-03-05T06:26:20Z","timestamp":1677997580276},"reference-count":24,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2004,12,1]],"date-time":"2004-12-01T00:00:00Z","timestamp":1101859200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3186,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2004,12]]},"DOI":"10.1016\/j.tcs.2004.09.001","type":"journal-article","created":{"date-parts":[[2004,10,4]],"date-time":"2004-10-04T17:02:47Z","timestamp":1096909367000},"page":"325-354","source":"Crossref","is-referenced-by-count":7,"title":["Linearity and regularity with negation normal form"],"prefix":"10.1016","volume":"328","author":[{"given":"Reiner","family":"H\u00e4hnle","sequence":"first","affiliation":[]},{"given":"Neil V.","family":"Murray","sequence":"additional","affiliation":[]},{"given":"Erik","family":"Rosenthal","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/j.tcs.2004.09.001_bib1","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1145\/321592.321603","article-title":"A linear format for resolution with merging and a new technique for establishing completeness","volume":"17","author":"Anderson","year":"1970","journal-title":"J. Assoc. Comput. Mach."},{"issue":"2","key":"10.1016\/j.tcs.2004.09.001_bib2","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","article-title":"Theorem proving via general matings","volume":"28","author":"Andrews","year":"1981","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/j.tcs.2004.09.001_bib3","first-page":"19","article-title":"Resolution theorem proving","volume":"Vol. 1","author":"Bachmair","year":"2001"},{"key":"10.1016\/j.tcs.2004.09.001_bib4","doi-asserted-by":"crossref","unstructured":"P. Baumgartner, U. Furbach, Model elimination without contrapositives, in: Bundy (Ed.), Proc. 12th Conf. on Automated Deduction CADE, Nancy, France, Lecture Notes in Artificial Intelligence, Vol. 814, Springer, Berlin, 1994, pp. 87\u2013101.","DOI":"10.1007\/3-540-58156-1_7"},{"key":"10.1016\/j.tcs.2004.09.001_bib5","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","article-title":"On matrices with connections","volume":"28","author":"Bibel","year":"1981","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/j.tcs.2004.09.001_bib6","series-title":"Handbook of Tableau Methods","author":"D\u2019Agostino","year":"1999"},{"key":"10.1016\/j.tcs.2004.09.001_bib7","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","article-title":"A computing procedure for quantification theory","volume":"7","author":"Davis","year":"1960","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/j.tcs.2004.09.001_bib8","series-title":"First-Order Logic and Automated Theorem Proving","author":"Fitting","year":"1996"},{"key":"10.1016\/j.tcs.2004.09.001_bib9","first-page":"101","article-title":"Tableaux and related methods","volume":"Vol. 1","author":"H\u00e4hnle","year":"2001"},{"key":"10.1016\/j.tcs.2004.09.001_bib10","doi-asserted-by":"crossref","unstructured":"R. H\u00e4hnle, N.V. Murray, E. Rosenthal, Completeness for linear regular negation normal form inference systems, Proc. of the Tenth Internat. Symp. on Methodologies for Intelligent Systems, Charlotte, NC, Lecture Notes in Artificial Intelligence, Vol. 1325, Springer, Berlin, 1997, pp. 590\u2013599.","DOI":"10.1007\/3-540-63614-5_57"},{"issue":"3","key":"10.1016\/j.tcs.2004.09.001_bib11","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","article-title":"Linear resolution with selection function","volume":"2","author":"Kowalski","year":"1971","journal-title":"Artificial Intelligence"},{"key":"10.1016\/j.tcs.2004.09.001_bib12","unstructured":"R. Letz, First-order calculi and proof procedures for automated deduction, Ph.D. Dissertation, TU Darmstadt, 1993."},{"key":"10.1016\/j.tcs.2004.09.001_bib13","series-title":"Automated Theorem Proving","author":"Loveland","year":"1978"},{"issue":"1","key":"10.1016\/j.tcs.2004.09.001_bib14","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","article-title":"A deductive approach to program synthesis","volume":"2","author":"Manna","year":"1980","journal-title":"ACM Trans. Progr. Languages Systems"},{"issue":"1","key":"10.1016\/j.tcs.2004.09.001_bib15","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":"J. Assoc. Comput. Mach."},{"issue":"1","key":"10.1016\/j.tcs.2004.09.001_bib16","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"},{"issue":"2","key":"10.1016\/j.tcs.2004.09.001_bib17","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/23005.23716","article-title":"Inference with path resolution and semantic graphs","volume":"34","author":"Murray","year":"1987","journal-title":"J. Assoc. Comput. Mach."},{"issue":"3","key":"10.1016\/j.tcs.2004.09.001_bib18","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/174130.174135","article-title":"Dissolution","volume":"40","author":"Murray","year":"1993","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/j.tcs.2004.09.001_bib19","series-title":"Proc. of the Eighth Internat. Symp. on Artificial Intelligence","first-page":"378","article-title":"An application of non-clausal deduction in diagnosis","author":"Ramesh","year":"1995"},{"key":"10.1016\/j.tcs.2004.09.001_bib20","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","article-title":"A theory of diagnosis from first principles","volume":"32","author":"Reiter","year":"1987","journal-title":"Artificial Intelligence J."},{"key":"10.1016\/j.tcs.2004.09.001_bib21","first-page":"77","article-title":"The generalized resolution principle","volume":"Vol. 3","author":"Robinson","year":"1968"},{"key":"10.1016\/j.tcs.2004.09.001_bib22","first-page":"103","article-title":"A machine-oriented logic incorporating the equality relation","volume":"Vol. 4","author":"Sibert","year":"1969"},{"key":"10.1016\/j.tcs.2004.09.001_bib23","series-title":"First-Order Logic","author":"Smullyan","year":"1995"},{"key":"10.1016\/j.tcs.2004.09.001_bib24","unstructured":"K. Wallace, G. Wrightson, Regressive merging in model elimination tableau-based theorem provers, J. Interest Group Pure Appl. Logics (Special Issue: Selected Papers from Tableaux\u201994) 3 (1995) 921\u2013938."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397504005973?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397504005973?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T09:21:06Z","timestamp":1549185666000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397504005973"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2004,12]]}},"alternative-id":["S0304397504005973"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2004.09.001","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2004,12]]}}}