Kripke semantics for higher-order type theory applied to constraint logic programming languages

Abstract Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this article, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking.

Download Full-text

Constraint logic programming languages

Communications of the ACM ◽

10.1145/79204.79209 ◽

1990 ◽

Vol 33 (7) ◽

pp. 52-68 ◽

Cited By ~ 143

Author(s):

Jacques Cohen

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Constraint Logic Programming ◽

Logic Programming Languages

Download Full-text

Higher-Order Logic Programming

Handbook of Logic in Artificial Intelligence and Logic Programming: Volume 5: Logic Programming ◽

10.1093/oso/9780198537922.003.0011 ◽

1998 ◽

Author(s):

Gopalan Nadathur ◽

Dale Miller

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Functional Programming ◽

Ad Hoc ◽

Order Type ◽

Higher Order ◽

Order Logic ◽

Higher Order Logic ◽

Functional Programming Languages ◽

Logical Basis

Modern programming languages such as Lisp, Scheme and ML permit procedures to be encapsulated within data in such a way that they can subsequently be retrieved and used to guide computations. The languages that provide this kind of an ability are usually based on the functional programming paradigm, and the procedures that can be encapsulated in them correspond to functions. The objects that are encapsulated are, therefore, of higher-order type and so also are the functions that manipulate them. For this reason, these languages are said to allow for higher-order programming. This form of programming is popular among the users of these languages and its theory is well developed. The success of this style of encapsulation in functional programming makes is natural to ask if similar ideas can be supported within the logic programming setting. Noting that procedures are implemented by predicates in logic programming, higher-order programming in this setting would correspond to mechanisms for encapsulating predicate expressions within terms and for later retrieving and invoking such stored predicates. At least some devices supporting such an ability have been seen to be useful in practice. Attempts have therefore been made to integrate such features into Prolog (see, for example, [Warren, 1982]), and many existing implementations of Prolog provide for some aspects of higher-order programming. These attempts, however, are unsatisfactory in two respects. First, they have relied on the use of ad hoc mechanisms that are at variance with the declarative foundations of logic programming. Second, they have largely imported the notion of higher-order programming as it is understood within functional programming and have not examined a notion that is intrinsic to logic programming. In this chapter, we develop the idea of higher-order logic programming by utilizing a higher-order logic as the basis for computing. There are, of course, many choices for the higher-order logic that might be used in such a study. If the desire is only to emulate the higher-order features found in functional programming languages, it is possible to adopt a “minimalist” approach, i.e., to consider extending the logic of first-order Horn clauses— the logical basis of Prolog—in as small a way as possible to realize the additional functionality.

Download Full-text