Modelling Prolog Control

Roberto Barbuti, Michael Codish, Roberto Giacobazzi and Giorgio Levi   

Journal of Logic and Computation; 3 : 579--603, 1993


The goal of this paper is to construct a semantic basis for the abstract interpretation of Prolog programs. Prolog is a well-known logic programming language which applies a depth-first search strategy in order to provide a practical approximation of Horn clause logic. While pure logic programming has clean fixpoint, model-theoretic and operational semantics the situation for Prolog is different. Difficulties in capturing the declarative meaning of Prolog programs have led to various semantic definitions which attempt to encode the search strategy in different mathematical frameworks. However semantic based analyses of Prolog are typically achieved by abstracting the more simple but less precise declarative semantics of pure logic Programs. We propose instead to model Prolog control in a simple constraint logic language which is presented together with its declarative and operational semantics. This enables us to maintain the usual approach to declarative semantics of logic programs while capturing control aspects such as search strategy and selection rule.

Available:    bibtex entry   compressed postscript

Related sites:   The conference version

Michael Codish
The Department of Computer Science
Ben-Gurion University of the Negev
PoB 653, Beer-Sheva, 84105, Israel

© copyright notice