Compositional Semantics for the Procedural Interpretation of Logic

TL;DR

This paper develops a compositional semantics for logic programs by completing their abstract syntax, enabling a mathematical composition of meanings, and compares it with Tarski's algebraization of predicate logic.

Contribution

It introduces a complete abstract syntax for logic programs and defines a compositional semantics based on it, filling a gap in procedural interpretation.

Findings

Semantics characterized by equivalence with the immediate-consequence operator

Complete abstract syntax for logic programs proposed

Comparison with Tarski's algebraization of predicate logic

Abstract

Semantics of logic programs has been given by proof theory, model theory and by fixpoint of the immediate-consequence operator. If clausal logic is a programming language, then it should also have a compositional semantics. Compositional semantics for programming languages follows the abstract syntax of programs, composing the meaning of a unit by a mathematical operation on the meanings of its constituent units. The procedural interpretation of logic has only yielded an incomplete abstract syntax for logic programs. We complete it and use the result as basis of a compositional semantics. We present for comparison Tarski's algebraization of first-order predicate logic, which is in substance the compositional semantics for his choice of syntax. We characterize our semantics by equivalence with the immediate-consequence operator.