{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:53:07Z","timestamp":1676447587788},"reference-count":16,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2000,2,1]],"date-time":"2000-02-01T00:00:00Z","timestamp":949363200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4915,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1006\/jsco.1999.0359","type":"journal-article","created":{"date-parts":[[2002,9,18]],"date-time":"2002-09-18T18:57:36Z","timestamp":1032375456000},"page":"149-176","source":"Crossref","is-referenced-by-count":50,"title":["Cut-elimination and Redundancy-elimination by Resolution"],"prefix":"10.1006","volume":"29","author":[{"given":"Matthias","family":"Baaz","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Leitsch","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1006\/jsco.1999.0359_RF1","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1016\/0168-0072(92)90042-X","article-title":"Complexity of resolution proofs and function introduction","volume":"57","author":"Baaz","year":"1992","journal-title":"Ann. Pure Appl. Log."},{"key":"10.1006\/jsco.1999.0359_RF2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","article-title":"On skolemization and proof complexity","volume":"20","author":"Baaz","year":"1994","journal-title":"Fundam. Inform."},{"key":"10.1006\/jsco.1999.0359_RF3","doi-asserted-by":"crossref","unstructured":"M. Baaz, A. Leitsch, Proc. CSL\u201996, 1997, Springer, Berlin, 18, 33","DOI":"10.1007\/3-540-63172-0_30"},{"key":"10.1006\/jsco.1999.0359_RF4","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/S0168-0072(98)00026-8","article-title":"Cut normal forms and proof complexity","volume":"97","author":"Baaz","year":"1999","journal-title":"Ann. Pure Appl. Log."},{"key":"10.1006\/jsco.1999.0359_RF5","doi-asserted-by":"crossref","unstructured":"G. D\u00e9fourneaux, N. Peltier, Proc. CADE-14, 1997, Springer, Berlin, 431, 445","DOI":"10.1007\/3-540-63104-6_43"},{"key":"10.1006\/jsco.1999.0359_RF6","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/BF01201363","article-title":"Untersuchungen \u00fcber das logische Schlie\u00dfen","volume":"39","author":"Gentzen","year":"1934","journal-title":"Math. Z."},{"key":"10.1006\/jsco.1999.0359_RF7","series-title":"Proof Theory and Logical Complexity","author":"Girard","year":"1987"},{"key":"10.1006\/jsco.1999.0359_RF8","series-title":"The Resolution Calculus","author":"Leitsch","year":"1997"},{"key":"10.1006\/jsco.1999.0359_RF9","doi-asserted-by":"crossref","first-page":"234","DOI":"10.2307\/2275028","article-title":"Herbrand-Analysen zweier Beweise des Satzes von Roth: polynomiale Anzahlschranken","volume":"54","author":"Luckhardt","year":"1989","journal-title":"J. Symb. Log."},{"key":"10.1006\/jsco.1999.0359_RF10","series-title":"Mathematics and Plausible Reasoning","author":"P\u00f3lya","year":"1954"},{"key":"10.1006\/jsco.1999.0359_RF11","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1006\/jsco.1999.0359_RF12","series-title":"Handbook of Mathematical Logic","first-page":"867","article-title":"Proof theory: some applications of cut-elimination","author":"Schwichtenberg","year":"1977"},{"key":"10.1006\/jsco.1999.0359_RF13","first-page":"104","article-title":"Lower bounds on Herbrand\u2019s theorem","volume":"75","author":"Statman","year":"1979","journal-title":"Proc. Am. Math. Soc."},{"key":"10.1006\/jsco.1999.0359_RF14","series-title":"Normal derivability in classical logic","first-page":"204","author":"Tait","year":"1968"},{"key":"10.1006\/jsco.1999.0359_RF15","series-title":"Proof Theory","author":"Takeuti","year":"1987"},{"key":"10.1006\/jsco.1999.0359_RF16","series-title":"Two Applications of Logic to Mathematics","author":"Takeuti","year":"1978"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717199903590?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717199903590?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,12,18]],"date-time":"2019-12-18T04:56:09Z","timestamp":1576644969000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717199903590"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["S0747717199903590"],"URL":"http:\/\/dx.doi.org\/10.1006\/jsco.1999.0359","relation":{},"ISSN":["0747-7171"],"issn-type":[{"value":"0747-7171","type":"print"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}
