Access the full text.
Sign up today, get DeepDyve free for 14 days.
D. Miller, G. Nadathur, F. Pfenning, A. Scedrov (1991)
Uniform Proofs as a Foundation for Logic ProgrammingAnn. Pure Appl. Log., 51
Gopalan Nadathur, Dale Miller (1988)
Fifth International Logic Programming Conference
J. Hannan, D. Miller (1990)
Investigating a proof-theoretic meta-language for functional programs
D. Miller, G. Nadathur (1987)
A Logic Programming Approach to Manipulating Formulas and Programs
G. Nadathur, B. Jayaraman (1989)
Towards a WAM model for ?Prolog
L. McCarty (1988)
Clausal Intuitionistic Logic II - Tableau Proof ProceduresJ. Log. Program., 5
G. Huet (1975)
A Unification Algorithm for Typed lambda-CalculusTheor. Comput. Sci., 1
A. Martelli, U. Montanari (1982)
An Efficient Unification AlgorithmACM Trans. Program. Lang. Syst., 4
N. Shankar (1992)
Proof Search in the Intuitionistic Sequent Calculus
D. Miller (1992)
Unification Under a Mixed PrefixJ. Symb. Comput., 14
G. Nadathur, D. Miller (1988)
AN OVERVIEW OF PROLOG
(1970)
Investigations into Logical Deduction
Conal Elliott, F. Pfenning (1990)
A Semi-Functional Implementation of a Higher-Order Logic Programming Language
D. Miller (1991)
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
M. Fitting (1990)
First-Order Logic and Automated Theorem Proving
G. Nadathur, D. Wilson (1990)
A representation of Lambda terms suitable for operations on their intensions
F. Pfenning (1988)
Partial polymorphic type inference and higher-order unificationProceedings of the 1988 ACM conference on LISP and functional programming
G. Nadathur, D. Miller (1990)
Higher-order Horn clausesJ. ACM, 37
A. Felty, D. Miller (1988)
Specifying Theorem Provers in a Higher-Order Logic Programming Language
Amy Felty, Dale Miller (1988)
Ninth International Conference on Automated Deduction
Gérard Huet (1975)
A unification algorithm for typed ?-calculusTheoretical Computer Science, 1
M. Emden, R. Kowalski (1976)
The Semantics of Predicate Logic as a Programming LanguageJ. ACM, 23
B. Jayaraman, G. Nadathur (1991)
Implementation Techniques for Scoping Constructs in Logic Programming
D. Miller, G. Nadathur, A. Scedrov (1987)
Hereditary Harrop Formulas and Uniform Proof Systems
(1989)
eLP, a Common Lisp Implementation of Prolog. Implemented as part of the CMU ERGO project
Lawrence Paulson (1987)
The representation of logics in higher-order logic
D. Miller (1989)
Lexical Scoping as Universal Quantification
L. Wallen (1990)
Automated proof search in non-classical logics - efficient matrix proof methods for modal and intuitionistic logics
G. Nadathur, B. Jayaraman, Keehang Kwon (1995)
Scoping Constructs in Logic Programming: Implementation Problems and their SolutionsJ. Log. Program., 25
A proof procedure is presented for a class of formulas in intuitionistic logic. These formulas are the so-calledgoal formulas in the theory of hereditary Harrop formulas. Proof search in intuitionistic logic is complicated by the nonexistence of a Herbrand-like theorem for this logic: formulas cannot in general be preprocessed into a form such as the clausal form, and the construction of a proof is often sensitive to the order in which the connectives and quantifiers are analyzed. An interesting aspect of the formulas we consider here is that this analysis can be carried out in a relatively controlled manner in their context. In particular, the task of finding a proof can be reduced to one of demonstrating that a formula follows from a set of assumptions, with the next step in this process being determined by the structure of the conclusion formula. An acceptable implementation of this observation must utilize unification. However, since our formulas may contain universal and existential quantifiers in mixed order, care must be exercised to ensure the correctness of unification. One way of realizing this requirement involves labelling constants and variables and then using these labels to constrain unification. This form of unification is presented and used in a proof procedure for goal formulas in a first-order version of hereditary Harrop formulas. Modifications to this procedure for the relevant formulas in a higher-order logic are also described. The proof procedure that we present has a practical value in that it provides the basis for an implementation of the logic programming language λProlog.
Journal of Automated Reasoning – Springer Journals
Published: Dec 10, 2004
Read and print from thousands of top scholarly journals.
Already have an account? Log in
Bookmark this article. You can see your Bookmarks on your DeepDyve Library.
To save an article, log in first, or sign up for a DeepDyve account if you don’t already have one.
Copy and paste the desired citation format or use the link below to download a file formatted for EndNote
Access the full text.
Sign up today, get DeepDyve free for 14 days.
All DeepDyve websites use cookies to improve your online experience. They were placed on your computer when you launched this website. You can change your cookie settings through your browser.