{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:45Z","timestamp":1761611145687},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bf00881900","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:18:27Z","timestamp":1104002307000},"page":"43-81","source":"Crossref","is-referenced-by-count":42,"title":["Implementing tactics and tacticals in a higher-order logic programming language"],"prefix":"10.1007","volume":"11","author":[{"given":"Amy","family":"Felty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Brisset, Pascal and Ridoux, Olivier, ?The architecture of an implementation of ?Prolog: Prolog\/Mali?, in Dale Miller (Ed.),Proceedings of the Workshop on the ?Prolog Programming Language, University of Pennsylvania Technical Report MS-CIS-92-86, pp. 41?64 (1992)."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"Alonzo Church","year":"1940","unstructured":"Church, Alonzo, ?A formulation of the simple theory of types?,J. Symbolic Logic 5, 56?68 (1940).","journal-title":"J. Symbolic Logic"},{"key":"CR3","unstructured":"Constable, Robert L.et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall (1986)."},{"issue":"2\/3","key":"CR4","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"Thierry Coquand","year":"1988","unstructured":"Coquand, Thierry and Huet, G\u00e9rard, ?The calculus of constructions?,Information and Computation 76(2\/3), 95?120 (1988).","journal-title":"Information and Computation"},{"key":"CR5","unstructured":"deBruijn, N. G., ?A survey of the project AUTOMATH?, inTo H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 579?606, Academic Press (1980)."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Dietzen, Scott and Pfenning, Frank, ?Higher-order and modal logic as a framework for explanation-based generalization?, in Alberto Maria Segre (Ed.),Sixth International Workshop on Machine Learning, pp. 447?449, Morgan Kaufmann (1989).","DOI":"10.1016\/B978-1-55860-036-2.50113-2"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Elliott, Conal, ?Higher-order unification with dependent types?, inRewriting Techniques and Applications, pp. 121?136, Springer-Verlag Lecture Notes in Computer Science (1989).","DOI":"10.1007\/3-540-51081-8_104"},{"key":"CR8","unstructured":"Elliott, Conal and Pfenning, Frank, ?eLP, a Common Lisp Implementation of ?Prolog?, (1990)."},{"key":"CR9","unstructured":"Elliott, Conal and Pfenning, Frank, ?A semi-functional implementation of a higher-order logic programming language?, in Peter Lee (Ed.),Topics in Advanced Language Implementation, pp. 289?325, MIT Press (1991)."},{"key":"CR10","unstructured":"Felty, Amy,Specifying and Implementing Theorem Provers in a Higher-Order Logic Programming Language, Ph.D. thesis, University of Pennsylvania, Technical Report MS-CIS-89-53 (1989)."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Felty, Amy, ?Encoding dependent types in an intuitionistic logic?, in G\u00e9rard Huet and Gordon Plotkin (Eds.),Logical Frameworks, pp. 215?251, Cambridge University Press (1991).","DOI":"10.1017\/CBO9780511569807.010"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Felty, Amy, ?A logic program for transforming sequent proofs to natural deduction proofs?, in Peter Schroeder-Heister (Ed.),Proceedings of the First International Workshop on Extensions of Logic Programming, pp. 157?178, Springer-Verlag Lecture Notes in Artificial Intelligence (1991).","DOI":"10.1007\/BFb0038694"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Felty, Amy, ?A logic programming approach to implementing higher-order term rewriting?, in Lars-Henrik Eriksson, Lars Halln\u00e4s, and Peter Schroeder-Heister (Eds.),Proceedings of the Second International Workshop on Extensions of Logic Programming, pp. 135?161, Springer-Verlag Lecture Notes in Artificial Intelligence (1992).","DOI":"10.1007\/BFb0013606"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Felty, Amy and Miller, Dale, ?Specifying theorem provers in a higher-order logic programming language?, inNinth International Conference on Automated Deduction, pp. 61?80, Springer-Verlag Lecture Notes in Computer Science (1988).","DOI":"10.1007\/BFb0012823"},{"key":"CR15","unstructured":"Gardner, Philippa,Representing Logics in Type Theory. Ph.D. thesis, University of Edinburgh, Technical Report CST-93-92 (1992)."},{"key":"CR16","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gerhard Gentzen","year":"1969","unstructured":"Gentzen, Gerhard, ?Investigations into logical deductions, 1935?, in M. E. Szabo (Ed.),The Collected Papers of Gerhard Gentzen, pp. 68?131, North-Holland Publishing Co., Amsterdam (1969)."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"Gordon, Michael J., Milner, Arthur J. and Wadsworth, Christopher P.,Edinburgh LCF: A Mechanised Logic of Computation, Lecture Notes in Computer Science, Vol. 78, Springer-Verlag (1979).","DOI":"10.1007\/3-540-09724-4"},{"key":"CR18","unstructured":"Gordon, Mike, ?HOL: a machine oriented formulation of higher-order logic?, Technical Report 68, University of Cambridge (1985)."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Hagiya, Masami, ?Programming by example and proving by example using higher-order unification?, inTenth International Conference on Automated Deduction, pp. 588?602. Springer-Verlag Lecture Notes in Artificial Intelligence (1990).","DOI":"10.1007\/3-540-52885-7_116"},{"key":"CR20","unstructured":"Hannan, John and Miller, Dale, ?A meta language for functional programs?, in H. Abramson and M. Rogers (Eds.),Meta Programming in Logic Programming, Ch. 24, pp. 453?476, MIT Press (1989)."},{"issue":"1","key":"CR21","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"Robert Harper","year":"1993","unstructured":"Harper, Robert, Honsell, Furio, and Plotkin, Gordon, ?A framework for defining logics?,J. ACM 40(1), 143?184 (1993).","journal-title":"J. ACM"},{"key":"CR22","unstructured":"Hindley, J. Roger and Seldin, Jonathan P.,Introduction to Combinatory Logic and Lambda Calculus, Cambridge University Press (1986)."},{"key":"CR23","unstructured":"Howard, William A., ?The formulae-as-type notion of construction, 1969?, inTo H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp. 479?490, Academic Press (1980)."},{"key":"CR24","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G\u00e9rard Huet","year":"1975","unstructured":"Huet, G\u00e9rard, ?A unification algorithm for typed ?-calculus?,Theoretical Computer Science 1, 27?57 (1975).","journal-title":"Theoretical Computer Science"},{"key":"CR25","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"Richard E. Korf","year":"1985","unstructured":"Korf, Richard E., ?Depth-first iterative-deepening: an optimal admissible tree search?,Artificial Intelligence 27, 97?109 (1985).","journal-title":"Artificial Intelligence"},{"key":"CR26","unstructured":"Martin-L\u00f6f, Per,Intuitionistic Type Theory, Studies in Proof Theory, Lecture Notes. BIBLIOPOLIS, Napoli (1984)."},{"issue":"4","key":"CR27","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"Dale Miller","year":"1991","unstructured":"Miller, Dale, ?A logic programming language with lambda-abstraction, function variables, and simple unification?,J. Logic and Computation 1(4), 497?536 (1991).","journal-title":"J. Logic and Computation"},{"key":"CR28","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"Dale Miller","year":"1992","unstructured":"Miller, Dale, ?Unification under a mixed prefix?,J. Symbolic Computation 14, 321?358 (1992).","journal-title":"J. Symbolic Computation"},{"key":"CR29","unstructured":"Miller, Dale and Nadathur, Gopalan, ?A logic programming approach to manipulating formulas and programs?,IEEE Symposium on Logic Programming, pp. 379?388 (1987)."},{"key":"CR30","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"Dale Miller","year":"1991","unstructured":"Miller, Dale, Nadathur, Gopalan, Pfenning, Frank, and Scedrov, Andre, ?Uniform proofs as a foundation for logic programming?,Annals of Pure and Applied Logic 51, 125?157 (1991).","journal-title":"Annals of Pure and Applied Logic"},{"key":"CR31","unstructured":"Nadathur, Gopalan,A Higher-Order Logic as the Basis for Logic Programming, Ph.D. thesis, University of Pennsylvania, Technical Report MS-CIS-87-48 (1987)."},{"key":"CR32","unstructured":"Nadathur, Gopalan and Jayaraman, Bharat, ?Towards a WAM model for ?Prolog?, in Ewing Lusk and Ross Overbeek (Eds.),Proceedings of the North American Conference on Logic Programming, pp. 1180?1198 (1989)."},{"issue":"4","key":"CR33","doi-asserted-by":"crossref","first-page":"777","DOI":"10.1145\/96559.96570","volume":"37","author":"Gopalan Nadathur","year":"1990","unstructured":"Nadathur, Gopalan and Miller, Dale, ?Higher-order horn clauses?,J. ACM 37(4), 777?814 (1990).","journal-title":"J. ACM"},{"key":"CR34","unstructured":"Pareschi, Remo and Miller, Dale, ?Extending definite clause grammars with scoping constructs?, in D. H. D. Warren and P. Szeredi (Eds.),International Conference in Logic Programming, pp. 373?389, MIT Press (1990)."},{"issue":"3","key":"CR35","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"Lawrence C. Paulson","year":"1989","unstructured":"Paulson, Lawrence C., ?The foundation of a generic theorem prover?,J. Automated Reasoning 5(3), 363?397 (1989).","journal-title":"J. Automated Reasoning"},{"key":"CR36","doi-asserted-by":"crossref","unstructured":"Pfenning, Frank, ?Logic programming in the LF logical framework?, in G\u00e9rard Huet and Gordon Plotkin (Eds.),Logical Frameworks, pp. 149?181, Cambridge University Press (1991).","DOI":"10.1017\/CBO9780511569807.008"},{"key":"CR37","doi-asserted-by":"crossref","unstructured":"Pfenning, Frank and Elliot, Conal, ?Higher-order abstract syntax?, inProceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp. 199?208 (1988).","DOI":"10.1145\/960116.54010"},{"key":"CR38","volume-title":"Natural Deduction","author":"Dag Prawitz","year":"1965","unstructured":"Prawitz, Dag,Natural Deduction, Almqvist & Wiksell, Uppsala (1965)."},{"key":"CR39","doi-asserted-by":"crossref","unstructured":"Prawitz, Dag, ?Ideas and results in proof theory?, in J.E. Fenstad (Ed.),Proceedings of the Second Scandinavian Logic Symposium, Vol. 63 ofStudies in Logic and the Foundations of Mathematics, pp. 235?307, North-Holland (1971).","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"CR40","volume-title":"The Art of Prolog: Advanced Programming Techniques","author":"Leon Sterling","year":"1986","unstructured":"Sterling, Leon and Shapiro, Ehud,The Art of Prolog: Advanced Programming Techniques, MIT Press, Cambridge, MA (1986)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881900.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881900\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:30:02Z","timestamp":1586043002000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881900"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881900"],"URL":"https:\/\/doi.org\/10.1007\/bf00881900","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}