{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:52Z","timestamp":1759638952568},"reference-count":27,"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\/bf00881902","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:18:27Z","timestamp":1104002307000},"page":"115-145","source":"Crossref","is-referenced-by-count":23,"title":["A proof procedure for the logic of hereditary Harrop formulas"],"prefix":"10.1007","volume":"11","author":[{"given":"Gopalan","family":"Nadathur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Elliott, Conal and Pfenning, Frank, ?eLP, a Common Lisp implementation of ?Prolog?, Implemented as part of the CMU ERGO project (1989)."},{"key":"CR2","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 Implementat6ion, pp. 289?325, MIT Press (1991)."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BFb0012823","volume-title":"Ninth International Conference on Automated Deduction","author":"Amy Felty","year":"1988","unstructured":"Felty, Amy and Miller, Dale, ?Specifying theorem provers in a higher-order logic programming language?, in Ewing Lusk and Ross Overbeek (Eds.),Ninth International Conference on Automated Deduction, pp. 61?80, Argonne, Illinois, Springer-Verlag (1988)."},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Fitting, Melvin,First-Order Logic and Automated Theorem Proving, Springer-Verlag (1990).","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Gentzen, Gerhard, ?Investigations into logical deduction?, in M. E. Szabo (Ed.),The Collected Papers of Gerhard Gentzen, pp. 68?131, North Holland Publishing Co. (1969).","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"CR6","unstructured":"Hannan, John J.,Investigating a Proof-Theoretic Meta-Language for Functional Programs, Ph.D. thesis, University of Pennsylvania (1990)."},{"key":"CR7","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":"CR8","first-page":"871","volume-title":"Eighth International Logic Programming Conference","author":"Bharat Jayaraman","year":"1991","unstructured":"Jayaraman, Bharat and Nadathur, Gopalan, ?Implementation techniques for scoping constructs in logic programming?, in K. Furukawa (Ed.),Eighth International Logic Programming Conference, pp. 871?886, Paris, MIT Press (1991)."},{"issue":"2","key":"CR9","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"Alberto Martelli","year":"1982","unstructured":"Martelli, Alberto and Montanari, Ugo, ?An efficient unification algorithm?,ACM Transactions on Programming Languages and Systems 4(2), 258?282 (1982).","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/0743-1066(88)90014-3","volume":"5","author":"L. Thorne McCarty","year":"1988","unstructured":"McCarty, L. Thorne, ?Clausal intuitionistic logic II. Tableau proof procedures?,J. Logic Programming 5, 93?132 (1988).","journal-title":"J. Logic Programming"},{"key":"CR11","unstructured":"Miller, Dale, ?Hereditary Harrop formulas and logic programming?, inProceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, pp. 153?156, Moscow (1987)."},{"key":"CR12","first-page":"268","volume-title":"Sixth International Logic Programming Conference","author":"Dale Miller","year":"1989","unstructured":"Miller, Dale, ?Lexical scoping as universal quantification?, in G. Levi and M. Martelli (Eds.),Sixth International Logic Programming Conference, pp. 268?283, Lisbon, Portugal, MIT Press (1989)."},{"issue":"4","key":"CR13","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":"CR14","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?,Journal of Symbolic Computation 14, 321?358 (1992).","journal-title":"Journal of Symbolic Computation"},{"key":"CR15","unstructured":"Miller, Dale and Nadathur, Gopalan, ?A logic programming approach to manipulating formulas and programs?, in S. Haridi (Ed.),IEEE Symposium on Logic Programming, pp. 379?388, San Francisco (1987)."},{"key":"CR16","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 Pure and Applied Logic 51, 125?157 (1991).","journal-title":"Annals Pure and Applied Logic"},{"key":"CR17","unstructured":"Miller, Dale, Nadathur, Gopalan and Scedrov, Andre, ?Hereditary Harrop formulas and uniform proof systems?, in David Gries (Ed.),Symposium on Logic in Computer Science, pp. 98?105, Ithaca, NY (1987)."},{"key":"CR18","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, Cleveland, Ohio (1989)."},{"key":"CR19","unstructured":"Nadathur, Gopalan, Jayaraman, Bharat and Kwon, Keehang, ?Scoping constructs in logic programming: Implementation problems and their solution?, submitted (1992)."},{"key":"CR20","first-page":"810","volume-title":"Fifth International Logic Programming Conference","author":"Gopalan Nadathur","year":"1988","unstructured":"Nadathur, Gopalan and Miller, Dale, ?An overview of ?Prolog?, in Kenneth A. Bowen and Robert A. Kowalski (Eds.),Fifth International Logic Programming Conference, pp. 810?827, Seattle, Washington, MIT Press (1988)."},{"issue":"4","key":"CR21","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":"CR22","doi-asserted-by":"crossref","unstructured":"Nadathur, Gopalan and Wilson, Debra Sue, ?A representation of lambda terms suitable for operations on their intensions?, inProceedings of the 1990 ACM Conference on Lisp and Functional Programming, pp. 341?348, ACM Press (1990).","DOI":"10.1145\/91556.91682"},{"key":"CR23","unstructured":"Paulson, Lawrence R., ?The representation of logics in higher-order logic?, Technical Report Number 113, University of Cambridge, Computer Laboratory, August 1987."},{"key":"CR24","doi-asserted-by":"crossref","unstructured":"Pfenning, Frank, ?Partial polymorphic type inference and higher-order unification?, inProceedings of the ACM Lisp and Functional Programming Conference, pp. 153?163, ACM Press (1988).","DOI":"10.1145\/62678.62697"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Shankar, Natarajan, ?Proof search in the intuitionistic sequent calculus?, in D. Kapur (Ed.),Proceedings of the Eleventh International Conference on Automated Deduction - CADE-11, pp. 522?536, Springer-Verlag (1992).","DOI":"10.1007\/3-540-55602-8_189"},{"issue":"4","key":"CR26","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"M. H. Emden van","year":"1976","unstructured":"van Emden, M. H. and Kowalski, R.H., ?The semantics of predicate logic as a programming language?,J. ACM 23(4), 733?742 (1976).","journal-title":"J. ACM"},{"key":"CR27","unstructured":"Wallen, Lincoln A.,Automated Proof Search in Non-Classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics, MIT Press (1990)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881902.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881902\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881902","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:30:03Z","timestamp":1586043003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881902"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":27,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881902"],"URL":"https:\/\/doi.org\/10.1007\/bf00881902","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}