{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,11,6]],"date-time":"2022-11-06T17:28:41Z","timestamp":1667755721306},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2005,8,1]],"date-time":"2005-08-01T00:00:00Z","timestamp":1122854400000},"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":[[2005,8]]},"DOI":"10.1007\/s11225-005-8469-4","type":"journal-article","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T11:23:12Z","timestamp":1128597792000},"page":"195-234","source":"Crossref","is-referenced-by-count":1,"title":["Double-Negation Elimination in Some Propositional Logics"],"prefix":"10.1007","volume":"80","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]},{"given":"Robert","family":"Veroff","sequence":"additional","affiliation":[]},{"given":"Larry","family":"Wos","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8469_CR1","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1090\/S0002-9947-1958-0094302-9","volume":"88","author":"C.C. CHANG","year":"1958","unstructured":"CHANG, C.C., \u2018Algebraic analysis of many valued logics\u2019, Trans. Amer. Math. Soc. 88:467\u2013490, 1958.","journal-title":"Trans. Amer. Math. Soc."},{"issue":"3","key":"8469_CR2","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1023\/A:1012486904520","volume":"68","author":"B. FITELSON","year":"2001","unstructured":"FITELSON, B., and L. WOS, \u2018Finding missing proofs with automated reasoning\u2019, Studia Logica 68(3):329\u2013356, 2001.","journal-title":"Studia Logica"},{"issue":"1","key":"8469_CR3","doi-asserted-by":"crossref","first-page":"90","DOI":"10.2307\/2274956","volume":"55","author":"J.R. HINDLEY","year":"1990","unstructured":"HINDLEY, J.R., and D. MEREDITH, \u2018Principal type-schemes and condensed detachment\u2019, J. Symbolic Logic 55(1):90\u2013105, 1990.","journal-title":"J. Symbolic Logic"},{"key":"8469_CR4","doi-asserted-by":"crossref","first-page":"391","DOI":"10.2307\/2964545","volume":"27","author":"A. HORN","year":"1962","unstructured":"HORN, A., \u2018The separation theorem of intuitionist propositional calculus\u2019, J. Symbolic Logic 27:391\u2013399, 1962.","journal-title":"J. Symbolic Logic"},{"key":"8469_CR5","volume-title":"Introduction to Metamathematics","author":"S.C. KLEENE","year":"1952","unstructured":"KLEENE, S.C., Introduction to Metamathematics, van Nostrand, Princeton, New Jersey, 1952."},{"key":"8469_CR6","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1305\/ndjfl\/1093957574","volume":"4","author":"CA. MEREDITH","year":"1963","unstructured":"MEREDITH, CA., and A. PRIOR, \u2018Notes on the axiomatics of the propositional calculus\u2018, Notre Dame J. Formal Logic 4:171\u2013187, 1963.","journal-title":"Notre Dame J. Formal Logic"},{"key":"8469_CR7","unstructured":"McCUNE, W., Otter 3.3 Reference Manual, Tech. Memo ANL\/MCS-TM-263, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL, August 2003."},{"issue":"4","key":"8469_CR8","doi-asserted-by":"crossref","first-page":"587","DOI":"10.1007\/BF01880330","volume":"7","author":"G. MINTS","year":"1991","unstructured":"MINTS, G., and T. TAMMET, \u2018Condensed detachment is complete for relevance logic: A computer-aided proof\u2019, J. Automated Reasoning 7(4):587\u2013596, 1991.","journal-title":"J. Automated Reasoning"},{"issue":"2\u20133","key":"8469_CR9","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/BF00370844","volume":"57","author":"A. PRIJATELJ","year":"1996","unstructured":"PRIJATELJ, A., \u2018Bounded contraction and Gentzen-style formulation of Lukasiewicz logics\u2019, Studia Logica 57(2\u20133):437\u2013456, 1996.","journal-title":"Studia Logica"},{"key":"8469_CR10","doi-asserted-by":"crossref","first-page":"182","DOI":"10.1080\/00048405685200181","volume":"34","author":"A.N. PRIOR","year":"1956","unstructured":"PRIOR, A.N., \u2018Logicians at play; or Syll, Simp, and Hilbert\u2019, Australasian J. Phil. 34:182\u2013192, 1956.","journal-title":"Australasian J. Phil."},{"key":"8469_CR11","volume-title":"Formal Logic","author":"A.N. PRIOR","year":"1962","unstructured":"PRIOR, A.N., Formal Logic, 2nd edition, Clarendon Press, Oxford, 1962.","edition":"2"},{"key":"8469_CR12","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. ROBINSON","year":"1965","unstructured":"ROBINSON, J., \u2018A machine-oriented logic based on the resolution principle\u2019, J. ACM 12:23\u201341, 1965.","journal-title":"J. ACM"},{"key":"8469_CR13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1090\/S0002-9947-1958-0094299-1","volume":"87","author":"A. ROSE","year":"1958","unstructured":"ROSE, A., and J.B. ROSSER, \u2018Fragments of many-valued statement calculi\u2019, Trans. Amer. Math. Soc. 87:1\u201353, 1958.","journal-title":"Trans. Amer. Math. Soc."},{"key":"8469_CR14","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1305\/ndjfl\/1093891799","volume":"16","author":"I. THOMAS","year":"1975","unstructured":"THOMAS, I., \u2018Shorter development of an axiom\u2019, Notre Dame J. Formal Logic 16:378, 1975.","journal-title":"Notre Dame J. Formal Logic"},{"issue":"2","key":"8469_CR15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1023\/A:1010683508225","volume":"27","author":"D. ULRICH","year":"2001","unstructured":"ULRICH, D., \u2018A legacy recalled and a tradition continued\u2019, J. Automated Reasoning 27(2):97\u2013122, 2001.","journal-title":"J. Automated Reasoning"},{"issue":"3","key":"8469_CR16","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R. VEROFF","year":"1996","unstructured":"VEROFF, R., \u2018Using hints to increase the effectiveness of an automated reasoning program: Case studies\u2019, J. Automated Reasoning 16(3):223\u2013239, 1996.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"8469_CR17","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0898-1221(94)00220-F","volume":"29","author":"L. WOS","year":"1996","unstructured":"WOS, L., \u2018The resonance strategy\u2019, Computers and Mathematics with Applications 29(2):133\u2013178, 1996.","journal-title":"Computers and Mathematics with Applications"},{"issue":"2","key":"8469_CR18","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1023\/A:1010691726881","volume":"27","author":"L. WOS","year":"2001","unstructured":"WOS, L., \u2018Conquering the Meredith single axiom\u2019, J. Automated Reasoning 27(2):175\u2013199, 2001.","journal-title":"J. Automated Reasoning"},{"key":"8469_CR19","doi-asserted-by":"crossref","DOI":"10.1142\/4132","volume-title":"A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning","author":"L. WOS","year":"1999","unstructured":"WOS, L., and G. PIEPER, A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning. World Scientific, Singapore, 1999."},{"issue":"3","key":"8469_CR20","first-page":"165","volume":"30","author":"L. WOS","year":"2001","unstructured":"WOS, L., and R. THIELE, \u2018Hilbert's new problem\u2019, Bulletin of the Section of Logic 30(3):165\u2013175, 2001.","journal-title":"Bulletin of the Section of Logic"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-005-8469-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11225-005-8469-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-005-8469-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T06:24:39Z","timestamp":1559370279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11225-005-8469-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,8]]},"references-count":20,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2005,8]]}},"alternative-id":["8469"],"URL":"https:\/\/doi.org\/10.1007\/s11225-005-8469-4","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,8]]}}}