Constraint Propagation for First-Order Logic and Inductive Definitions

TL;DR

This paper introduces a polynomial-time algorithm for constraint propagation in first-order logic and its extension with inductive definitions, enabling symbolic execution and broad reasoning applications.

Contribution

It presents a novel polynomial-time algorithm for constraint propagation in FO and FO(ID), with symbolic execution capabilities and practical applications.

Findings

Algorithm operates in polynomial time with respect to data complexity.

Constraint propagation can be represented by datalog programs.

Algorithm can be executed symbolically, independently of specific structures.

Abstract

Constraint propagation is one of the basic forms of inference in many logic-based reasoning systems. In this paper, we investigate constraint propagation for first-order logic (FO), a suitable language to express a wide variety of constraints. We present an algorithm with polynomial-time data complexity for constraint propagation in the context of an FO theory and a finite structure. We show that constraint propagation in this manner can be represented by a datalog program and that the algorithm can be executed symbolically, i.e., independently of a structure. Next, we extend the algorithm to FO(ID), the extension of FO with inductive definitions. Finally, we discuss several applications.