Abstract
Miller, D., G. Nadathur, F. Pfenning and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic 51 (1991) 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.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 125-157 |
| Number of pages | 33 |
| Journal | Annals of Pure and Applied Logic |
| Volume | 51 |
| Issue number | 1-2 |
| DOIs | |
| State | Published - Mar 14 1991 |
| Externally published | Yes |
Bibliographical note
Funding Information: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 * A preliminary version of this paper appeared as [21]. Theorem 3 of that paper is incorrect. It is corrected by the material in Sections 5 and 6 of the current paper. ** Supported by NSF grant CCR-87-05596 and DARPA grant NOOO-14-85-K-0018. *** Supported by NSF grant IRI-8805696 and AR0 Contract DAAL03-88-K-0082. ‘Supported by The Office of Naval Research under contract NOOO14-84-K-0415a nd by the Defense Advanced Research Projects Agency (DOD), ARPA Order No. 5404, monitored by the Office of Naval Research under the same contract. O”S upported by NSF grants DMS85-01522 and CCR-87-05596, by ONR contract NOOO14-88-K-0635, and by the University of Pennsylvania Natural Sciences Association Young Faculty Award.