Meta-Logics for Logic Programming
Marianne Kalsbeek
Abstract:
Meta-Logics for Logic Programming
Marianne Kalsbeek
This dissertation consists of three separate parts, each of which can be read independently. In each part, a theme in Logic Programming (or rather, the practice of Logic Programming) is taken up and investigated from a logical point of view.
Part I is inspired by the observation that, although Logic Programming is based on ﬁrst order predicate logic, in many applications and implementations, such as Prolog, meta-logic programming, and databases, a syntax is employed that stretches far beyond ﬁrst order predicate logic. Ambivalent Logic, essentially ﬁrst order predicate logic with a very liberal syntax, is developed in Part I; a series of formal results justify the current Logic Programming practice of using liberal versions of ﬁrst order predicate logic syntax.
In Part II, the focus is on Vanilla meta-programming, where the meta- program takes object programs as input and imitates their execution. Typically, ambivalent syntax is employed here. Various correctness proofs for the standard Vanilla metainterpreter are discussed and compared.
Part III is based on the observation that in implementations of Logic Programming, the added control affects the procedural meaning of programs. In particular, the standard top-down processing of program clauses induces substructural effects. Substructural (Gentzen style) sequent calculi corresponding to various implementation styles, among them standard Prolog, are investigated here.