First-order Logic as a Constraint Programming Language

TL;DR

This paper introduces a denotational semantics for first-order logic tailored for constraint programming, capturing both execution and constraint maintenance, and enabling sound evaluation and implementation strategies.

Contribution

It provides a formal semantics that integrates constraint management into first-order logic, facilitating sound evaluation policies and implementation in constraint programming.

Findings

Semantics is sound with respect to the truth definition

Supports various constraint management policies

Enables sound implementation of constraint maintenance

Abstract

We provide a denotational semantics for first-order logic that captures the two-level view of the computation process typical for constraint programming. At one level we have the usual program execution. At the other level an automatic maintenance of the constraint store takes place. We prove that the resulting semantics is sound with respect to the truth definition. By instantiating it by specific forms of constraint management policies we obtain several sound evaluation policies of first-order formulas. This semantics can also be used a basis for sound implementation of constraint maintenance in presence of block declarations and conditionals.