UNIFORM PROOFS AS A FOUNDATION FOR LOGIC PROGRAMMING

pages

English

Documents

Écrit par
Duke University

Publié par
chaeh

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

Niveau: Supérieur
UNIFORM PROOFS AS A FOUNDATION FOR LOGIC PROGRAMMING Dale Miller Computer and Information Science Department University of Pennsylvania, Philadelphia, PA 19104 Gopalan Nadathur Computer Science Department Duke University, Durham, NC 27706 Frank Pfenning Computer Science Department Carnegie Mellon University, Pittsburgh, PA 15213 Andre Scedrov Mathematics Department University of Pennsylvania, Philadelphia, PA 19104 Abstract: 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 inter- pretation 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.

variable names

primitives should

logic programming

order horn

higher-order versions

uniform proofs

existentially quantified variables

logical constants

horn clause

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

UNIFORM PROOFS AS A FOUNDATION FOR LOGIC PROGRAMMING

Dale MillerComputer and Information Science Department University of Pennsylvania, Philadelphia, PA 19104 Gopalan NadathurComputer Science Department Duke University, Durham, NC 27706 Frank PfenningComputer Science Department Carnegie Mellon University, Pittsburgh, PA 15213 Andre ScedrovMathematics Department University of Pennsylvania, Philadelphia, PA 19104

Abstract: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 xed search instructions. The operational semantics is formalized by the identication of a class of cut-free sequent proofs calleduniform proofs. A uniform proof is one that can be found by a goal-directed search that respects the inter-pretation of the logical connectives as search instructions. The concept of a uniform proof is used to dene the notion of anabstract logic programming language, and it is shown that rst-order and higher-order Horn clauses with classical provability are examples of such a language. Horn clauses are then generalized tohereditary Harrop formulasand it is shown that rst-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 signicance of the various generalizations to rst-order Horn clauses is briey discussed.

Appear inAnnals of Pure and Applied Logic, 1991 (51), 125–157.

Voir