{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T08:29:06Z","timestamp":1742632146244},"reference-count":23,"publisher":"Elsevier BV","issue":"1-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":["Theoretical Computer Science"],"published-print":{"date-parts":[[2000,2]]},"DOI":"10.1016\/s0304-3975(99)00177-2","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T20:48:18Z","timestamp":1027630098000},"page":"273-298","source":"Crossref","is-referenced-by-count":8,"title":["Correspondences between classical, intuitionistic and uniform provability"],"prefix":"10.1016","volume":"232","author":[{"given":"Gopalan","family":"Nadathur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/S0304-3975(99)00177-2_BIB1","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB2","unstructured":"A.G. Dragalin, Mathematical Intuitionism: Introduction to Proof Theory, Translations of Mathematical Monographs, Vol. 67, American Mathematical Society, Providence, RI, 1979."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB3","doi-asserted-by":"crossref","unstructured":"R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, J. Symbolic Logic 57(3) (1992).","DOI":"10.2307\/2275431"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB4","doi-asserted-by":"crossref","unstructured":"M. Fitting, First-order Logic and Automated Theorem Proving, Springer, Berlin, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB5","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","article-title":"N-Prolog: an extension of Prolog with hypothetical implication. II. Logical foundations and negation as failure","volume":"4","author":"Gabbay","year":"1985","journal-title":"J. Logic Programming"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB6","doi-asserted-by":"crossref","unstructured":"G. Gentzen, Investigations into logical deduction, in: M.E. Szabo (Ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969, pp. 68\u2013131.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"issue":"1","key":"10.1016\/S0304-3975(99)00177-2_BIB7","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1080\/11663081.1993.10510797","article-title":"Computation with run-time skolemization (N-Prolog part 3)","volume":"3","author":"Gabbay","year":"1993","journal-title":"J. Appl. Non-Classical Logics"},{"issue":"1","key":"10.1016\/S0304-3975(99)00177-2_BIB8","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1093\/logcom\/4.1.69","article-title":"A proof-theoretic analysis of goal-directed provability","volume":"4","author":"Harland","year":"1994","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB9","unstructured":"J. Hudelmaier, Bounds for cut elimination for propositional intuitionistic logic. Technical Report CIS-Bericht-90-3, Centrum f\u00fcr Informations-und Sprachverarbeitung, Universit\u00e4t M\u00fcnchen, 1990. Arch. Math. Logic (1991)."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB10","unstructured":"S.C. Kleene, Permutability of inferences in Gentzen's calculi LK and LJ, Mem. Amer. Math. Soc. (10) (1952) 1\u201326."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB11","doi-asserted-by":"crossref","unstructured":"J. Lobo, J. Minker, A. Rajasekar, Foundations of Disjunctive Logic Programming, MIT Press, Cambridge, MA, 1992.","DOI":"10.1016\/B978-0-12-450010-5.50022-0"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB12","unstructured":"D.W. Loveland, D.W. Reed, A near-Horn Prolog for compilation, in: J. Lassez, G. Plotkin (Eds.), Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA, 1991."},{"issue":"4","key":"10.1016\/S0304-3975(99)00177-2_BIB13","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","article-title":"A logic programming language with lambda-abstraction, function variables, and simple unification","volume":"1","author":"Miller","year":"1991","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB14","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","article-title":"Uniform proofs as a foundation for logic programming","volume":"51","author":"Miller","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB15","unstructured":"G.E. Minc, V.P. Orevkov, An extension of the theorems of Glivenko and Kreisel to a certain class of formulas of predicate calculus, Soviet Math. 4(3) (1963) 1365\u20131367. Translation of Doklady, Academy of Sciences of the USSR, Published by the American Mathematical Society, Providence, RI."},{"issue":"1","key":"10.1016\/S0304-3975(99)00177-2_BIB16","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF00881902","article-title":"A proof procedure for the logic of hereditary Harrop formulas","volume":"11","author":"Nadathur","year":"1993","journal-title":"J. Automat. Reason."},{"issue":"2","key":"10.1016\/S0304-3975(99)00177-2_BIB17","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1093\/logcom\/8.2.209","article-title":"Uniform provability in classical logic","volume":"8","author":"Nadathur","year":"1998","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB18","doi-asserted-by":"crossref","unstructured":"G. Nadathur, D.W. Loveland, Uniform proofs and disjunctive logic programming, in: D. Kozen (Ed.), 10th Ann. IEEE Symp. on Logic in Computer Science, IEEE Computer Soc. Press, Silver Springer, MD, 1995, pp. 148\u2013155.","DOI":"10.1109\/LICS.1995.523252"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB19","unstructured":"V.P. Orevkov, On Glivenko sequent classes, Proc. Steklov Inst. Math. 98: 1968, 147\u2013173. English translation published by American Mathematical Society, Providence, RI, 1971."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB20","unstructured":"D. Prawitz, Natural Deduction: A Proof-Theoretical Study, Almqvist & Wiksell, Stockholm, 1965."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB21","unstructured":"D. Pym, E. Ritter, L. Wallen, Proof-terms for classical and intuitionistic resolution, in: Automat. Deduction \u2013 CADE-13, Lecture Notes in Artificial Intelligence, vol. 1404, Springer, Berlin, 1996, pp. 17\u201331."},{"key":"10.1016\/S0304-3975(99)00177-2_BIB22","doi-asserted-by":"crossref","unstructured":"N. Shankar, Proof search in the intuitionistic sequent calculus, in: D. Kapur (Ed.), Proc. 11th Internat. Conf. Automat. Deduction \u2013 CADE-11, Springer, Berlin, 1992, pp. 522\u2013536.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"10.1016\/S0304-3975(99)00177-2_BIB23","unstructured":"A.S. Troelstra, H. Schwichtenberg, Basic Proof Theory, Cambridge University Press, Cambridge, 1996."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001772?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397599001772?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,2,4]],"date-time":"2020-02-04T14:16:54Z","timestamp":1580825814000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397599001772"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,2]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2000,2]]}},"alternative-id":["S0304397599001772"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(99)00177-2","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2000,2]]}}}