{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T22:56:53Z","timestamp":1762297013985},"publisher-location":"Berlin\/Heidelberg","reference-count":39,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"354053590X"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0038693","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T14:16:05Z","timestamp":1138198565000},"page":"101-156","source":"Crossref","is-referenced-by-count":9,"title":["Some applications of Gentzen's proof theory in automated deduction"],"prefix":"10.1007","author":[{"given":"Michael","family":"Beeson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M. Beeson","year":"1985","unstructured":"Beeson, M. [1985], Foundations of Constructive Mathematics, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1985)."},{"key":"4_CR2","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-1-4613-9647-5_25","volume-title":"Computers and Mathematics '89","author":"M. Beeson","year":"1989","unstructured":"Beeson, M. [1989], Logic and computation in MATHPERT: An expert system for learning mathematics, in: Kaltofen and Watt (eds.), Computers and Mathematics '89, pp. 202\u2013214, Springer-Verlag, New York\/ Heidelberg\/ Berlin (1989)."},{"key":"4_CR3","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop, E. [1967], Foundations of Constructive Analysis, McGraw-Hill, New York (1967)."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W. [1984], Some automatic proofs in analysis, in: Automated Theorem Proving: After 25 years, ed. by W. W. Bledsoe and D. W. Loveland, A.M.S. Contemporary Mathematics series, vol. 29, Providence, R. I. (1984).","DOI":"10.1090\/conm\/029"},{"key":"4_CR5","unstructured":"Bowen, K. [1980] Programming with Full First Order Logic (dissertation), School of Computer and Information Sciences, Syracuse University, November 1980."},{"key":"4_CR6","volume-title":"A Computational Logic","author":"R. Boyer","year":"1979","unstructured":"Boyer, R., and Moore, J. [1979] A Computational Logic, Academic Press, New York (1979)."},{"key":"4_CR7","volume-title":"Programming in Prolog","author":"Clocksin","year":"1981","unstructured":"Clocksin and Mellish [], Programming in Prolog, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1981)."},{"key":"4_CR8","volume-title":"Implementing Mathematics with the NuPrl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"Constable, R. L. [1986], et. al., Implementing Mathematics with the NuPrl Proof Development System, Prentice-Hall, Englewood Cliffs, N. J. (1986)."},{"key":"4_CR9","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/BFb0062852","volume-title":"Algebra and Logic","author":"S. Feferman","year":"1975","unstructured":"Feferman, S. [1975], A language and axioms for explicit mathematics, in: Algebra and Logic, Lecture Notes in Mathematics 450 87\u2013139, Springer-Verlag, Berlin (1975)."},{"key":"4_CR10","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S0049-237X(08)71625-2","volume-title":"Logic Colloquium '78: Proceedings of the Logic Colloquium at Mons, 1978","author":"S. Feferman","year":"1979","unstructured":"Feferman, S. [1979], Constructive theories of functions and classes, in: Boffa, M., van Dalen, D., and McAloon, K. (eds.), Logic Colloquium '78: Proceedings of the Logic Colloquium at Mons, 1978, pp. 159\u2013224, North-Holland, Amsterdam (1979)."},{"key":"4_CR11","first-page":"95","volume":"XIX","author":"S. Feferman","year":"1985","unstructured":"Feferman, S. [1985] A theory of variable types, Rev. Colombiana de Matem\u00e1ticas, XIX, 95\u2013106.","journal-title":"Rev. Colombiana de Matem\u00e1ticas"},{"key":"4_CR12","first-page":"61","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988","author":"A. Felty","year":"1988","unstructured":"Felty, A., and Miller, D. [1988] Specifying Theorem Provers in a Higher-Order Logic Programming Language, in: Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988, pp. 61\u201380, Springer Lecture Notes in Computer Science 310, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1988)."},{"key":"4_CR13","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0743-1066(84)90029-3","volume":"1","author":"D. M. Gabbay","year":"1984","unstructured":"Gabbay, D. M., and Reyle, U. [1984], N-Prolog: an extension of Prolog with hypothetical implication, Part I, J. Logic Programming 1 (1984) 319\u2013355.","journal-title":"J. Logic Programming"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Gabbay, D. M., and Reyle, U. [1989], Computation with run time skolemisation (N-Prolog Part 3), to appear.","DOI":"10.1080\/11663081.1993.10510797"},{"key":"4_CR15","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/0743-1066(87)90020-3","volume":"4","author":"A Gelder","year":"1987","unstructured":"van Gelder, A. [1987], Efficient loop detection in Prolog using the tortoise-and-hare technique, J. Logic Programming 4 (23\u201332), 1987.","journal-title":"J. Logic Programming"},{"key":"4_CR16","volume-title":"Proofs and Types","author":"J. Girard","year":"1989","unstructured":"Girard, J. [1989] Proofs and Types, Cambridge University Press, New York (1989)."},{"key":"4_CR17","series-title":"SICS R88005 Research Report ISSN","volume-title":"A proof-theoretic approach to logic programming","author":"L Halln\u00e4s","year":"1987","unstructured":"Halln\u00e4s, L, and Schroeder-Heister, P., [1987] A proof-theoretic approach to logic programming, SICS R88005 Research Report ISSN 0283-3638, Swedish Institute of Computer Science, Box 1263, S-164 28 Kista, Sweden (1987)."},{"key":"4_CR18","volume-title":"PX: A Computational Logic","author":"S. Hayashi","year":"1988","unstructured":"Hayashi, S. [1988], PX: A Computational Logic, MIT Press, Cambridge, Mass. (1988)."},{"key":"4_CR19","first-page":"238","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988","author":"D. Howe","year":"1988","unstructured":"Howe, D. [1988], Computational metatheory in Nuprl, in: Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988, pp. 238\u2013257, Springer Lecture Notes in Computer Science 310, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1988)."},{"key":"4_CR20","unstructured":"Huet,G. [1987] A uniform approach to type theory, INRIA Laboratory Research Report No. 795 (February 1988). An earlier version is more accessible"},{"key":"4_CR21","volume-title":"Fundamentals in Artificial Intelligence","author":"G. Huet","year":"1986","unstructured":"Huet, G. [1986], Deduction and computation, in: Fundamentals in Artificial Intelligence, ed. by Bibel, W. and Jorrand, P., Lecture Notes in Computer Science 232, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1986)."},{"key":"4_CR22","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"Kleene, S. C. [1952], Introduction to Metamathematics, van Nostrand, Princeton, N. J. (1952)."},{"key":"4_CR23","unstructured":"Kleene, S. C. [1952a], Permutability of inferences in Gentzen's calculi LK and LJ, in: Two Papers on the Predicate Calculus, A.M.S. Memoirs 10 (1952), A. M. S., Providence, R. I."},{"key":"4_CR24","unstructured":"Lifschitz, V. [1986], On the declarative semantics of logic programming with negation, in: Proc. Workshop on Foundationsof Deductive Databases and Logic Programming, Washington, D.C., August, 1986."},{"key":"4_CR25","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-96826-6","volume-title":"Foundations of Logic Programming","author":"J. W. Lloyd","year":"1984","unstructured":"Lloyd, J. W. [1984], Foundations of Logic Programming, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1984)."},{"key":"4_CR26","first-page":"415","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., and Bry, Francois [1988], SATCHMO: a theorem prover implemented in Prolog, in: Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988, pp. 415\u2013434, Springer Lecture Notes in Computer Science 310, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1988)."},{"key":"4_CR27","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P. [1984], Intuitionistic Type Theory, Bibliopolis, Naples (1984)."},{"issue":"12","key":"4_CR28","doi-asserted-by":"crossref","first-page":"1029","DOI":"10.1145\/33447.33448","volume":"30","author":"J. McCarthy","year":"1987","unstructured":"McCarthy, J. [1987], Generality in artificial intelligence, Communications of the ACM, vol. 30, no. 12, December, 1987, pp. 1029\u20131035.","journal-title":"Communications of the ACM"},{"key":"4_CR29","first-page":"325","volume-title":"Proceedings, AAAI Nonmonotonic Reasoning Workshop","author":"L. T. McCarty","year":"1984","unstructured":"McCarty, L. T., [1984], Programming directly in a nonmonotonic logic: extended abstract, in: Proceedings, AAAI Nonmonotonic Reasoning Workshop, New Paltz, N.Y, Oct 1984, pp. 325\u2013336."},{"key":"4_CR30","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0743-1066(88)90005-2","volume":"5","author":"L. T. McCarty","year":"1988","unstructured":"McCarty, L. T., [1988] Clausal intuitionistic logic I. Fixed-point semantics, J. Logic Programming 5, 1\u201333 (1988).","journal-title":"J. Logic Programming"},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"McCarty, L. T., [1988a] Clausal intuitionistic logic II. Tableau proof procedures, J. Logic Programming (to appear).","DOI":"10.1016\/0743-1066(88)90014-3"},{"key":"4_CR32","first-page":"98","volume-title":"Proceedings of the Symposium on Logic in Computer Science, Cornell University, June 1987","author":"D. Miller","year":"1987","unstructured":"Miller, D., Nadathur, G., and Scedrov, A. [1987], Hereditary Harrop Formulas and Uniform Proofs Systems, in: Proceedings of the Symposium on Logic in Computer Science, Cornell University, June 1987, pp. 98\u2013105, IEEE Computer Society Press, Washington, D.C. (1987)."},{"key":"4_CR33","unstructured":"Miller, D., Nadathur, G., Pfenning, F., and Scedrov, A. [TA], Uniform Proofs as a Foundation for Logic Programming, to appear in Annals of Pure and Applied Logic, available as Report MS-CIS-89-36, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA 19104."},{"key":"4_CR34","unstructured":"Nadathur, G. [1987], A Higher-Order Logic as the Basis for Logic Programming, Ph. D. Thesis, University of Pennsylvania, 1987."},{"key":"4_CR35","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. C. Paulson","year":"1986","unstructured":"Paulson, L. C. [1986] Natural deduction as higher-order resolution, J. Logic Programming 3 237\u2013258.","journal-title":"J. Logic Programming"},{"key":"4_CR36","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof Theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"Sch\u00fctte, K. [1977], Proof Theory, Springer-Verlag, Berlin\/Heidelberg\/New York (1977)."},{"key":"4_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"573","DOI":"10.1007\/3-540-16780-3_122","volume-title":"Proc. 8th CADE","author":"M. Stickel","year":"1986","unstructured":"Stickel, M. [1986] A Prolog technology theorem prover: implementation by an extended Prolog compiler, in: Proc. 8th CADE, Oxford, 1986, pp. 573\u2013587, Lecture Notes in Computer Science 230, Springer-Verlag, Berlin\/ Heidelberg\/ New York (1986). Longer version is to appear in J. Automated Reasoning."},{"key":"4_CR38","first-page":"752","volume-title":"Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988","author":"M. Stickel","year":"1988","unstructured":"Stickel, M. [1988] A Prolog technology theorem prover, in: Proceedings of the Ninth International Conference on Automated Deduction, Argonne Ill, May 1988, pp. 752\u2013753, Springer Lecture Notes in Computer Science 310, Springer-Verlag, Berlin\/ Heidelberg\/New York (1988)."},{"key":"4_CR39","unstructured":"Thistlewaite, P.B., McRobbie, M.A., and Meyer, R.K., Automated Theorem Proving in Non-Classical Logics, Pitman, London, and Wiley, New York (1988)."}],"container-title":["Lecture Notes in Computer Science","Extensions of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0038693.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:23:40Z","timestamp":1607552620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0038693"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354053590X"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/bfb0038693","relation":{},"subject":[]}}