{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:30:54Z","timestamp":1784845854685,"version":"3.55.0"},"publisher-location":"Berlin\/Heidelberg","reference-count":21,"publisher":"Springer-Verlag","isbn-type":[{"value":"354019343X","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0012823","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T06:12:39Z","timestamp":1132726359000},"page":"61-80","source":"Crossref","is-referenced-by-count":46,"title":["Specifying theorem provers in a higher-order logic programming language"],"prefix":"10.1007","author":[{"given":"Amy","family":"Felty","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Arnon Avron, Furio A. Honsell, and Ian A. Mason. Using Typed Lambda Calculus to Implement Formal Systems on a Machine. Technical Report ECS-LFCS-87-31, Laboratory for the Foundations of Computer Science, University of Edinburgh, June 1987."},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"W. W. Bledsoe. Non-resolution theorem proving. Artificial Intelligence, 9:1\u201335, 1977.","journal-title":"Artificial Intelligence"},{"key":"4_CR3","unstructured":"W. W. Bledsoe. The UT Prover. Technical Report ATP-17B, University of Texas at Austin, April 1983."},{"key":"4_CR4","unstructured":"R. L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"4_CR5","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR6","unstructured":"Amy Felty. Implementing theorem provers in logic programming. November 1987. Dissertation Proposal, University of Pennsylvania."},{"key":"4_CR7","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"G. Gentzen","year":"1969","unstructured":"Gerhard Gentzen. Investigations into logical deductions, 1935. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, pages 68\u2013131, North-Holland Publishing Co., Amsterdam, 1969."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Michael J. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation. Volume 78 of Lecture Notes in Computer Science, Springer-Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"4_CR9","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Symposium on Logic in Computer Science, pages 194\u2013204, Ithaca, NY, June 1987."},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G. P. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Proceedings of the Third International Logic Programming Conference, pages 448\u2013462, London, June 1986.","DOI":"10.1007\/3-540-16492-8_94"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247\u2013255, 1986.","DOI":"10.3115\/981131.981165"},{"key":"4_CR13","unstructured":"Dale Miller and Gopalan Nadathur. \u03bbProlog Version 2.6. August 1987. Distribution in C-Prolog code."},{"key":"4_CR14","unstructured":"Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In IEEE Symposium on Logic Programming, San Francisco, September 1987."},{"key":"4_CR15","unstructured":"Dale Miller, Gopalan Nadathur, and Andre Scedrov. Hereditary harrop formulas and uniform proof systems. In Symposium on Logic in Computer Science, pages 98\u2013105, Ithaca, NY, June 1987."},{"key":"4_CR16","unstructured":"Gopalan Nadathur. A Higher-Order Logic as the Basis for Logic Programming. PhD thesis, University of Pennsylvania, December 1986."},{"key":"4_CR17","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0743-1066(86)90015-4","volume":"3","author":"L. C. Paulson","year":"1986","unstructured":"Larence C. Paulson. Natural deduction as higher-order resolution. Journal of Logic Programming, 3:237\u2013258, 1986.","journal-title":"Journal of Logic Programming"},{"key":"4_CR18","unstructured":"Lawrence C. Paulson. The Representation of Logics in Higher-Order Logic. Draft, University of Cambridge, July 1987."},{"key":"4_CR19","volume-title":"Natural Deduction","author":"D. Prawitz","year":"1965","unstructured":"Dag Prawitz. Natural Deduction. Almqvist & Wiksell, Uppsala, 1965."},{"key":"4_CR20","volume-title":"The Art of Prolog: Advanced Programming Techniques","author":"L. Sterling","year":"1986","unstructured":"L. Sterling and E. Shapiro. The Art of Prolog: Advanced Programming Techniques. MIT Press, Cambridge MA, 1986."},{"key":"4_CR21","unstructured":"Mabry Tyson and W. W. Bledsoe. Conflicting bindings and generalized substitutions. In 4th International Conference on Automated Deduction, pages 14\u201318, Springer-Verlag, February 1979."}],"container-title":["Lecture Notes in Computer Science","9th International Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0012823.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T15:06:37Z","timestamp":1607353597000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0012823"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["354019343X"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/bfb0012823","relation":{},"subject":[]}}