Uniform proofs as a foundation for logic programming

Annals of Pure and Applied Logic 51 (1-2):125-157 (1991)
  Copy   BIBTEX


Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 125–157. A proof-theoretic characterization of logical languages that form suitable bases for Prolog-like programming languages is provided. This characterization is based on the principle that the declarative meaning of a logic program, provided by provability in a logical system, should coincide with its operational meaning, provided by interpreting logical connectives as simple and fixed search instructions. The operational semantics is formalized by the identification of a class of cut-free sequent proofs called uniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the interpretation of the logical connectives as search instructions. The concept of a uniform proof is used to define the notion of an abstract logic programming language, and it is shown that first-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized to hereditary Harrop formulas and it is shown that first-order and higher-order versions of this new class of formulas are also abstract logic programming languages if the inference rules are those of either intuitionistic or minimal logic. The programming language significance of the various generalizations to first-order Horn clauses is briefly discussed



    Upload a copy of this work     Papers currently archived: 76,419

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

26 (#449,520)

6 months
1 (#452,962)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Parsing/Theorem-Proving for Logical Grammar CatLog3.Glyn Morrill - 2019 - Journal of Logic, Language and Information 28 (2):183-216.
Focussing and proof construction.Jean-Marc Andreoli - 2001 - Annals of Pure and Applied Logic 107 (1-3):131-163.
Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
A focused approach to combining logics.Chuck Liang & Dale Miller - 2011 - Annals of Pure and Applied Logic 162 (9):679-697.

View all 25 citations / Add more citations

References found in this work

A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Investigations into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
Concerning formulas of the types a →b ∨c, a →(ex)b(X).Ronald Harrop - 1960 - Journal of Symbolic Logic 25 (1):27-32.

Add more references