Denotational and operational semantics for prolog

Saumya K. Debray, Prateek Mishra

Research output: Contribution to journalArticlepeer-review

51 Scopus citations


The semantics of PROLOG programs is usually given in terms of the model theory of first-order logic. However, this does not adequately characterizethe computational behavior of PROLOG programs. PROLOG implementations typically use a sequential evaluation strategy based on the textual order of clauses and literals in a program, as well as nonlogical features like cut. In this work we develop a denotational semantics that captures thecomputational behavior of PROLOG. We present a semantics for "cut-free" PROLOG, which is then extended to PROLOG with cut. For each case we develop a congruence proof that relates the semantics to a standard operational interpreter. As an application of our denotational semantics, we show the correctness of some standard "folk" theorems regarding transformations on PROLOG programs.

Original languageEnglish (US)
Pages (from-to)61-91
Number of pages31
JournalThe Journal of Logic Programming
Issue number1
StatePublished - Mar 1988

ASJC Scopus subject areas

  • Logic


Dive into the research topics of 'Denotational and operational semantics for prolog'. Together they form a unique fingerprint.

Cite this