Finite-Choice Logic Programming

TL;DR

Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain.

Abstract

Logic programming, as exemplified by datalog, defines the meaning of a program as its unique smallest model: the deductive closure of its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models for logic programs with negation has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables. We propose a new formalism, finite-choice logic programming, that uses choice, not negation, to admit multiple solutions. Finite-choice logic programming contains all the expressive power of the stable model semantics, gives meaning to a new and useful class of programs, and enjoys a least-fixed-point interpretation over a novel domain. We present an algorithm for exploring the solution space and prove it correct with respect to our semantics. Our implementation, the Dusa logic programming language, has performance that compares favorably with state-of-the-art answer set solvers and exhibits more predictable scaling with problem size.

Figures (29)

• Figure 1: The finite-choice logic program corresponding to the two rules ${\color{gray}\mathit{p}} \leftarrow \neg {\color{gray}\mathit{q}}$ and ${\color{gray}\mathit{q}} \leftarrow \neg {\color{gray}\mathit{p}}$ in ASP.
• Figure 2: Calculating a spanning tree over an undirected graph.
• Figure 3: Appointing a canonical representative for each connected component in an undirected graph.
• Figure 4: At left, an answer set program with no finite grounding. At right, the translation of this program to a finite-choice logic program.
• Figure 5: A finite-choice logic program representing the SAT instance $(p \vee \neg q) \wedge (\neg p \vee q \vee r)$.

Theorems & Definitions (56)

• definition 1: Terms
• definition 2: Facts
• definition 3: Rules
• definition 4: Programs
• definition 5: Substitutions
• definition 6: Databases
• definition 7: Satisfaction
• definition 8: Fact-set evolution
• definition 9: Steps
• definition 10: Saturation