# Finite-Choice Logic Programming

Robert J. Simmons<EMAIL_ADDRESS>0000-0003-2420-3067 UnaffiliatedUSA ,
Michael Arntzenius  0009-0002-0417-5636 RelationalAIUnited Kingdom and  Chris
Martens<EMAIL_ADDRESS>0000-0002-7026-0348 Northeastern
University360 Huntington AveBostonMassachusettsUSA02115

###### Abstract.

Logic programming, as exemplified by datalog, defines the meaning of a program
as the canonical smallest model derived from deductive closure over 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
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 collectively 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, called finite-choice logic programming, for which
the set of stable models can be characterized as the least fixed point of an
immediate consequence operator. Our formalism allows straightforward
expression of common idioms in both datalog and answer set programming, gives
meaning to a new and useful class of programs, enjoys a constructive and
direct operational semantics, and admits a predictive cost semantics, which we
demonstrate through our implementation.

Datalog, answer set programming, bottom-up evaluation

††copyright: none††conference: Make sure to enter the correct conference title
from your rights confirmation email; May 28; 2024††ccs: Computing
methodologies Logic programming and answer set programming††ccs: Theory of
computation Constraint and logic programming††ccs: Software and its
engineering Constraint and logic languages††ccs: Theory of computation
Denotational semantics

##  1\. Introduction

The generation of data according to structural and logical constraints is a
problem seeing growing uptake and interest over the last decade, exemplified
by applications like property-based random testing for typed functional
programs (Goldstein et al., 2023; Goldstein and Pierce, 2022; Paraskevopoulou
et al., 2022; Lampropoulos et al., 2017; Seidel et al., 2015; Claessen and
Hughes, 2011), procedural content generation in games (Short and Adams, 2017;
Shaker et al., 2016; Dormans and Bakkes, 2011), and reasoning about
nondeterministic computation in distributed systems (Alvaro et al., 2011b).
Answer set programming (ASP) (Gelfond and Lifschitz, 1988) is an approach to
this task based on logic programming that has seen considerable, ongoing
success in these and related domains (Smith and Mateas, 2011; Smith et al.,
2013; Smith and Bryson, 2014; Neufeld et al., 2015; Summerville et al., 2018;
Dabral and Martens, 2020; Dabral et al., 2023; Alvaro et al., 2011a),
especially in contexts where there is a desire to combine functional
constraints (e.g., well-typedness of a term, solvability of a puzzle, or
consistency of a distributed program trace) with a diverse range of
variability outside of those constraints.

To provide an expressive enough interface for programmers to represent
problems of interest while retaining an intuitive semantics, ASP reconciles
two incompatible intuitions about the meaning of logic programs. One
intuition, exemplified by datalog, concerns positive information only: from a
rule $p\leftarrow q_{1}\ldots q_{n}$, and a database containing $q_{1}\ldots
q_{n}$, deduce $p$, where $p$ and $q_{i}$ are all positive assertions. The
closure of deduction over such a program yields a single canonical model, the
smallest set of assertions closed under the given implications; any other
assertion is deemed false (Van Gelder et al., 1991).

The situation changes if we allow negative assertions such as
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>We can preserve the deductive mindset by taking this rule to mean that if
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>has no justification, then that suffices to justify
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>This program then has a single model that assigns
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to true and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to false, as obviously
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>has nothing to support its truth. Likewise, the canonical model of the logic
program containing the single rule
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>assigns
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to true and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to false. This intuition is cleanly captured by Przymusinski’s local
stratification (Przymusinski, 1988). Local stratification is a condition
sufficient to ensure the presence of a canonical model, and it is a satisfying
distillation of the interpretation that if a proposition has _no
justification_ it is _not true_. This intuition remains a successful one, and
is the foundation of almost all modern work on datalog and deductive
databases.

What about the program containing the two rules
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>There is no reasonable way for a canonical model to assign
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>or
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to true or false, so it would seem that, following the deductive mindset, we
must either reject this program outright or assign both
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>a third “indeterminate” value. But there’s a second intuition that says that
we should forego canonicity and accept two different models: the one where
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is true and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is false, and the one where
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is false and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is true. One’s first impulse may be to fall back on the satisfiability of
Boolean propositional formulas to explain this, but both these rules are
classically equivalent to
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\vee{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>which has an additional model where
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>are both true. Clark addresses this issue by defining the completion of a
program (Clark, 1978). The Clark completion of our little two rule program is
represented by the formulas
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftrightarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}\leftrightarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>These formulas are classically equivalent to to
$(\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\vee\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}})\wedge({\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\vee{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}})$,
which has precisely the two models we desire. The Clark completion is a
satisfying distillation of the intuition that every true proposition must have
some immediate justification.

Unfortunately, if we consider the program with two rules
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftarrow{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}\leftarrow{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>the Clark completion admits both the canonical model (where both
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>are false) and an additional model (where both
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>are true). As the intuition of logic programmers was formed in the context of
deductive closure, the extra solution admitted by Clark’s completion feels
like undesirably circular reasoning: the Clark completion is
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftrightarrow{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and in the non-canonical model
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is justifying
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and vice versa.

Gelfond and Lifschitz’s notion of the stable models of an answer set program
was successful at unifying these two intuitions. For locally stratified
programs, answer set programming assigns a unique canonical model that matches
the model suggested by local stratification. For programs without a canonical
model, it combines the intuitions of Clark completion with a rejection of
circular justification. Systems for computing the stable models of answer set
programs have fruitfully co-evolved with the advancements in Boolean
satisfiability solving, leading to sophisticated heuristics that make many
problems fast in practice (Gebser et al., 2017) and resulting in mature tools
(Gebser et al., 2011).

###  1.1. The compromise of stable models

Despite capturing programmer intuition so successfully, the actual semantic
interpretation of an answer set program is quite indirect.

The first level of indirection is that the standard definition of stable
models only applies to propositional logic programs without free variables.
Consider this rule, which derives a fact when two nodes in a graph are not
connected by an edge:

$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{notConnected}}(x,y)}}\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}(x)}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}(y)}},\neg{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(x,y)}}$

Answer set programming allows the illusion of rules containing free variables,
but given base facts
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}})}}$,
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}})}}$,
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}})}}$,
and
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}})}}$,
the stable models are only defined in terms of nine rules without free
variables, one for each of the assignments of the free variables $x$ and $y$
to the variable-free terms
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}}$,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}$,
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}$.
This is reflected in effectively all implementations of answer set
programming, which involve the interaction of a solver that only understands
variable-free rules and a grounder that generates variable-free rules, usually
incorporating heuristics to minimize the number of rules that the the solver
must deal with.

The second level of indirection is that even propositional answer set programs
do not directly have a semantics. The definition of stable models for answer
set programs first requires a syntactic transformation of an answer set
program into a logic program without negation (the reduct, see Section 3.2 or
(Gelfond and Lifschitz, 1988)). This transformation is defined with respect to
a candidate model. If the unique model of the reduct is the same as the
candidate model, the candidate model is accepted as an actual model. This
fixed-point-like definition is what the “stability” of stable models refers
to.

###  1.2. A constructive semantics based on mutually-exclusive choices

In this paper, we present finite-choice logic programming, an extension of
forward-chaining logic programming that incorporates mutually-exclusive
assignments of values to attributes. Facts take the form
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{v}}}$,
where
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}$
is the attribute and $v$ is the unique value assigned to that attribute, and a
set of facts (which we’ll call a database) must map each attribute to at most
one value. Concretely, a fact like
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edgeColor}}({{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{blue}}}}}$
would indicate that the edge from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}}$
to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}$
is assigned the color blue, and cannot be any other color. This is called a
_functional dependency_ : a relation is a (partial) function if it maps an
attribute to (at most) one value.

As we will see in Section 3, suitably choosing the domain of possible values
allows us to treat finite-choice logic programming as a generalization of
datalog without negation (if we restrict values to the single term
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}$)
or as a generalization of answer set programming without a grounding step (if
we restrict values to the two terms
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$).
But these are, fundamentally, the two most boring possible value domains!
Finite-choice logic programming opens a much more expressive set of
possibilities for logic programming.

Finite-choice logic programming specifies search problems through the
interplay of two kinds of rules, which very loosely correspond to those two
approaches:

  * •

A closed rule with the conclusion
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edgeColor}}({{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{green}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{yellow}}\\}}}}$
requires that the edge be either green or yellow if the rule’s premises are
satisfied.

  * •

An open rule with the conclusion
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edgeColor}}({{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{red}}}}}$
permits the edge to be red if the premises apply. If the premises apply, the
attribute
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edgeColor}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}})}}$
must take some value, but that value isn’t required to be
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{red}}$.

The interplay between open and closed rules is what allows finite-choice logic
programming to subsume answer set programming. An answer set program
containing the two rules
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>corresponds to the finite-choice logic program in Figure 1. The open rules 1
and 2 unconditionally permit
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>or
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to have the “false” value
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$,
and the closed rules 3 and 4 ensure that the assignment of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$
to either
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>or
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>will force the other attribute to take the “true” value
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}$.
The two solutions for this program are
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
and
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}$,
which correspond to the two solutions that answer set programming assigns to
the source program.

(1)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$ (2)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$ (3)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
(4)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
Figure 1. The finite-choice logic program corresponding to the two rules
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}\leftarrow\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>in ASP.

###  1.3. Contributions

The main contributions of this work include:

  * •

A straightforward definition of finite-choice logic programming that directly
accounts for the incremental construction of programs with multiple solutions
(Section 2).

  * •

A justification of answer set programming that doesn’t rely on rule grounding
(Section 3, in particular Section 3.2).

  * •

A more involved definition of finite-choice logic programming that defines the
meaning of a finite-choice logic program as the least fixed point of a
monotonic immediate consequence operator that operates on sets of mutually
exclusive models (Section 5).

  * •

A methodology for predicting the behavior of finite-choice logic programs
based on the cost semantics for logic programs described by McAllester
(McAllester, 2002) (Section 6.4).

  * •

The Dusa implementation of finite-choice logic programming (Section 6.6).

###  1.4. Related Work

Functional dependencies are not a new feature in logic programming. Systems
like LogicBlox enforce invariants through functional dependencies, treating
conflicts as errors that invalidate a transaction (Aref et al., 2015). A
separate class of systems in the tradition of Krishnamurthy and Naqvi,
including Soufflé, use relations with functional dependencies to allow a
database to efficiently pick only one of a set of solutions (Krishnamurthy and
Naqvi, 1988; Giannotti et al., 2001; Greco and Zaniolo, 2001; Hu et al.,
2021). This is a very efficient approach when it is expressive enough, and we
conjecture that Soufflé programs using their nondeterminstic choice operator
can be faithfully translated into a finite-choice logic programs that only
have open rules. Without an analogue of the closed rules in finite-choice
logic programming, we believe these systems are unable to specify the search
problems necessary to generalize answer set programming.

There have also been other approaches to constructively and incrementally
generating stable models. Sacca and Zaniolo’s algorithm applied to general
answer set programs, though it was primarily used to justify the
nondeterminstic choice operation described above (Sacca and Zaniolo, 1990). We
interpret their _stable backtracking fixedpoint_ algorithm as potentially
giving a direct implementation for answer set programming without grounding,
though it seems to us that this significant fact was not noticed or exploited
by the authors or anyone else. There has also been a disjunctive extension to
datalog (Eiter et al., 1997) and characterizations of its stable models
(Przymusinski, 1991), and Leone et al. (Leone et al., 1997) present an
algorithm for incrementally deriving these stable models. Their approach is
based on initially creating a single canonical model by letting some
propositions be “partially true”. In these approaches to generating stable
models, the set of solutions is presented only as the output of an algorithm,
rather than denotationally. The _choice sets_ we introduce in Section 5.3 are
both foundational to our denotational semantics and to the implementation
strategy we discuss in Section 6.

Our denotational semantics for finite-choice logic programming describes a
domain-like structure for nondeterminism that draws inspiration from domain
theory writ large (Scott, 1982), particularly powerdomains for
nondeterministic lambda calculi and imperative programs (Plotkin, 1976; Smyth,
1976; Kennaway and Hoare, 1980). Our partial order relation on choice sets
matches the one used for Smyth powerdomains in particular (Smyth, 1976).
However, our construction requires certain completeness criteria on posets
that differ from these and other domain definitions we have found in the
literature.

##  2\. The operational meaning of a finite-choice logic program

In this section, we define finite-choice logic programming with a
nondeterministic operational semantics.

###  2.1. Programs

###### Definition 2.1 (Terms).

As common in logic programming settings, terms are Herbrand structures, either
variables $x,y,z,\ldots$ or uninterpreted functions
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{f}}(t_{1},\ldots,t_{n})$
where the arguments $t_{i}$ are terms. Constants are functions with no
arguments, and as usual we’ll leave the parentheses off and just write
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}$
or
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}$
instead of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}()$
or
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}()$.
We’ll often abbreviate sequences of terms $t_{1},\ldots,t_{n}$ as
$\overline{t}$ when the indices aren’t important.

###### Definition 2.2 (Facts).

A fact has the form
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({t_{1},\ldots,t_{n}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{v}}}$,
where
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>is a predicate and the $t_{i}$ and $v$ are variable-free (i.e.  _ground_)
terms. The first part,
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(t_{1},\ldots,t_{n})}}$,
is the fact’s attribute, and $v$ is the fact’s value. We’ll sometimes use $a$
to stand in for variable-free attributes
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}$.

###### Definition 2.3 (Rules).

Rules $H\leftarrow R$ have one of two forms, open and closed.

(open form rule)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{v}}}$
$\displaystyle\leftarrow F$ (closed form rule, $m\geq 1$)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{v_{1},\ldots,v_{m}\\}}}}$
$\displaystyle\leftarrow F$

In both cases, the formula $F$ is a conjunction of premises of the form
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{v}}}$,
which may contain variables. The rule’s conclusion (or head) $H$ is the part
to the left of the $\leftarrow$ symbol. Every variable appearing in the head
$H$ must also appear in the formula $F$.

###### Definition 2.4 (Programs).

A program $P$ is a finite set of rules.

###### Definition 2.5 (Substitutions).

A substitution $\sigma$ is a total function from variables to ground terms.
Applying a substitution to a term ($\sigma t$) or a formula ($\sigma F$)
replaces all variables $x$ in the term or formula with the term $\sigma(x)$.

###  2.2. Operational semantics

###### Definition 2.6 (Database consistency).

A database $D$ is a set of facts. A database is consistent exactly when each
attribute
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}$
maps to at most one value $v$: if
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{v}}}\in
D$ and
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{v^{\prime}}}}\in
D$, then $v=v^{\prime}$.

###### Definition 2.7 (Satisfaction).

We say that a substitution $\sigma$ satisfies $F$ in the database $D$ when,
for each
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{v}}}$
in $F$,
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\sigma\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\sigma
v}}}$ is in $D$.

###### Definition 2.8 (Evolution).

The relation $D\operatorname{\Rightarrow}_{P}S$ relates a database to a set of
databases:

  * •

If $P$ contains the closed-form rule
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{v_{1},\ldots,v_{m}\\}}}}\leftarrow
F$ and $\sigma$ satisfies $F$ in $D$, then $D\operatorname{\Rightarrow}_{P}S$,
where $S$ is the set of every consistent database
$D\cup\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\sigma\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\sigma
v_{i}}}}\\}$ for $1\leq i\leq m$.

  * •

If $P$ contains the open-form rule
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({t_{1},\ldots,t_{n}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{v}}}\leftarrow
F$ and $\sigma$ satisfies $F$ in $D$, then $D\operatorname{\Rightarrow}_{P}S$,
where $S$ contains one or two elements. $S$ always contains $D$ and, if the
database
$D\cup\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\sigma\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\sigma
v}}}\\}$ is consistent, $S$ contains that database as well.

We say $D\operatorname{\leadsto}_{P}D^{\prime}$ if and only if
$D\operatorname{\Rightarrow}_{P}S$ and $D^{\prime}\in S$. The relation
$D\operatorname{\leadsto}^{*}_{P}D^{\prime}$ is the usual reflexive and
transitive closure of $D\operatorname{\leadsto}_{P}D^{\prime}$.

###### Definition 2.9 (Saturation).

A database $D$ is saturated under a program $P$ if it can only evolve under
the $\operatorname{\Rightarrow}_{P}$ relation to the singleton set containing
itself. In other words, $D$ is saturated under $P$ if, for all $S$ such that
$D\operatorname{\Rightarrow}_{P}S$, it is the case that $S=\\{D\\}$.

###### Definition 2.10 (Solutions).

A solution is a saturated database $D_{\textit{sol}}$ where
$\varnothing\operatorname{\leadsto}^{*}_{P}D_{\textit{sol}}$. A solution for a
consistent initial database $D_{\mathit{init}}$ is a saturated database
$D_{\textit{sol}}$ where
$D_{\mathit{init}}\operatorname{\leadsto}^{*}_{P}D_{\textit{sol}}$. Definition
2.8 ensures that $D_{\textit{sol}}$ must be consistent.

Definitions 2.9 and 2.10 are where we make critical use the fact that
$\operatorname{\Rightarrow}_{P}$ is a relation between databases and _sets_ of
databases: we need to be able to identify rules that force conflicts onto the
database. In a database
$D=\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}\\}$,
an applicable rule with the conclusion
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}}\\}}}}$
means that $D\operatorname{\Rightarrow}_{P}\varnothing$, and therefore $D$
cannot be a solution.

###  2.3. Examples

Let $P$ be the four rule program from Figure 1 in Section 1.2. We demonstrate
the operational semantics step-by-step, starting from the empty database
$D_{0}=\varnothing$. Two rules apply, so there are two $S_{i}$ such that
$\varnothing\operatorname{\Rightarrow}_{P}S_{i}$:

$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$ $\displaystyle\varnothing$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\varnothing,\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}\;\\}=S_{1}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$ $\displaystyle\varnothing$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\varnothing,\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}\;\\}=S_{2}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
rule does not apply
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
rule does not apply There are two possibilities for making progress. If we
pick
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
from $S_{1}$, three rules apply:
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}\;\\}=S_{3}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\},\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}\;\\}=S_{4}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
rule does not apply
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}\;\\}=S_{5}$
Again, there are two databases we can pick to make progress. If we pick
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
from $S_{4}$, we will find ourselves in trouble.
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}\;\\}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}\;\\}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
rule does not apply
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\varnothing$ The database
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
is _not_ saturated, because although there exist transitions to the singleton
set containing itself, our definition of saturation requires all possible
transitions to yield the singleton set containing itself. In particular, rule
4 requires the program to derive
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}$,
which conflicts with the existing fact
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$.
If instead choose
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}$
from $S_{5}$, we can see it is a solution:
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}\;\\}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}\;\\}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
rule does not apply
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}$
$\displaystyle\operatorname{\Rightarrow}_{P}\\{\;\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\\}\;\\}$

Symmetric reasoning applies to see that
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
is a solution. By inspection, no path exists to produce solutions where both
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>are assigned the same value.

####  2.3.1. Open versus closed rules

The two rule forms behave quite differently. Multiple closed rules end up
having an intersection-like behavior: the only solution for the following
program is
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}}}}$.

(5)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}\\}}}}$
$\displaystyle\leftarrow$ (6)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{d}}\\}}}}$
$\displaystyle\leftarrow$ (7)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{d}}\\}}}}$
$\displaystyle\leftarrow$

Multiple open rules, on the other hand, have a union-like behavior: the
following program has three solutions:
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}}}}\\}$,
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}\\}$,
and
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{d}}}}}\\}$.

(8)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}}}}$
$\displaystyle\leftarrow$ (9)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}$
$\displaystyle\leftarrow$ (10)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{d}}}}}$
$\displaystyle\leftarrow$

####  2.3.2. Default reasoning

When both closed and open rules are simultaneously active, the open rule
becomes effectively superfluous. It’s sometimes desirable to imagine open
rules as assigning some default value(s) that may be overridden by closed
rules. This will be the basis of the translation of answer set programs into
finite-choice logic programs, where open rules will permit attributes to take
the default
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$
value, and where closed rules will demand that attributes take the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}$
value.

##  3\. Connections

Concretely specifying the meaning of finite-choice logic programs in Section
2.2 allows for precise connections to be drawn between finite-choice logic
programming and other logic programming paradigms. In this section, we will
connect finite-choice logic programming with datalog without negation (Section
3.1) and with traditional answer set programming (Section 3.2). Then we will
show how finite-choice logic programming can directly give a meaning to answer
set programs without a grounding step (Section 3.3).

###  3.1. Connection to datalog

A datalog program without negation is a set of rules of the following form:

(datalog rule)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}}(\overline{t_{1}})}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}}(\overline{t_{n}})}}$

This is a generic use of “datalog,” as often people take “Datalog” to
specifically refer to “function-free” logic programs where term constants have
no arguments, a condition sufficient to ensure that every program has a finite
model. We will not require this here, but will generally only be interested in
datalog programs with finite models.

The canonical model of a datalog program is the least fixed point of datalog’s
immediate consequence operator. As in Definition 2.7, the premises of a rule
are satisfied by a substitution $\sigma$ in a set $X$ if, for each premise
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{i}}}(\overline{t_{i}})}}$
we have
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{i}}}(\sigma\overline{t_{i}})}}\in
X$. The set of immediate consequences of $X$ is the set
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\sigma\overline{t})}}$
where
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}$
is the conclusion of some rule and the rule’s premises are satisfied by
$\sigma$ in $X$.

Any datalog program $P$ can be translated to a finite-choice logic program
$\langle P\rangle$ by creating a unique new constant
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}$
and having that constant be the only value ever associated with any attribute.
The datalog rule above is rewritten as follows:

$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}}({\overline{t_{1}}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}}({\overline{t_{n}}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}}}}$

###### Theorem 3.1.

Let $P$ be a datalog program with a finite model, and let $\langle P\rangle$
be the interpretation of $P$ as a finite-choice logic program as above. Then
there is a unique solution $D$ to $\langle P\rangle$, and the model of $P$ is
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}\mid{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({\overline{t}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}}}}\in
D\\}$.

The proof of Theorem 3.1 is available in Section A.1. The straightforward
connection between datalog and finite-choice logic programming justifies using
value-free propositions
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(\overline{t})}}$
in finite-choice logic programming. Many relations, like
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}(x)}}$
representing the presence of a node in a graph, don’t have a meaningful value,
so we can write
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}})}}$
as syntactic shorthand for
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}({{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}}})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}}}}$.
If we wanted to assign colors to the nodes of a graph, for example, we could
write the following rule, which omits the implicit
“$\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unit}}$”
in the premise:

(11)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{nodeColor}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{red}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{green}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{blue}}\\}}}}\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}(x)}}$

###  3.2. Connection to answer set programming

Answer set programs are defined in terms of the stable model semantics
(Gelfond and Lifschitz, 1988). A rule in answer set programming has both non-
negated (positive) premises, which we’ll write as
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and negated (negative) premises, which we’ll write as
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>
(ASP rule)
$\displaystyle{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\leftarrow{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}},\ldots,{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}},\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{1}}},\ldots,\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>
Let $X$ denote a finite set of ground predicates. When modeling ASP, any
predicate in the set is treated as true, and any predicate not in the set is
false. To explain what a stable model is, the ASP literature (Gelfond and
Lifschitz, 1988; Lifschitz, 2019) first defines $P^{X}$, the reduct of a
program $P$ over $X$ obtained by:

  1. (1)

removing any rules where a negated premise appears in $X$

  2. (2)

removing all the negated premises from rules that weren’t removed in step 1

The reduct $P^{X}$ is always a regular datalog program with a unique finite
model. If the model of $P^{X}$ is exactly $X$, then $X$ is a stable model for
the ASP program $P$.

The translation of a single ASP rule of the form above produces $m+1$ rules in
the resulting finite-choice logic program. These introduced rules use two new
program-wide introduced constants,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$,
which represent the answer set program’s assignment of truth or falsehood,
respectively, to the relevant predicate:

$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{2}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\ldots$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{m}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{m-1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p_{n}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},\ldots,{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{m-1}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q_{m}}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$

The relationship between ASP programs and finite-choice logic programs is
described by Theorem 3.2, and the proof is available in Section A.2.

###### Theorem 3.2.

Let $P$ be an ASP program, and let $\langle P\rangle$ be the interpretation of
$P$ as a finite-choice logic program as defined above.

  * •

For all stable models $X$ of $P$, the set
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\mid{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>X\\}$ is a solution to $\langle P\rangle$.

  * •

For all solutions $D$ of $\langle P\rangle$, the set
$\\{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}\mid{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}\in
D\\}$ is a stable model of $P$.

###  3.3. Connection to answer set programming with lazy grounding

In the previous section, the connection between answer set programming and
finite-choice logic programming was established in terms of variable-free
programs, as that is how answer set programming is defined. But we can also
translate non-ground answer set programs to finite-choice logic programs under
a straightforward generalization of the translation in Section 3.2. The key
idea is that, whenever a negative premise is encountered in a rule, we want to
introduce an open rule that expresses the possible falsity of that premise if
the previous premises hold.

As an example, consider the following ASP rule:

$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(x,y)}}\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}(x)}},\neg{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(x,x)}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}(y,x)}},\neg{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}(y)}}$

This rule translates to three finite-choice logic program rules, one for the
“main” rule and an additional rule for each negated premise.

(12)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({x,x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}$
(13)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}({y})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({x,x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({y,x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}$
(14)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({x,y})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({x,x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}({y,x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}({y})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$

In order for the translation to be a valid finite-choice logic program, all
the variables in a negated premise must appear in a previous premise, but this
is a common requirement for answer set programming languages.

Under this translation, we can give a reasonable interpretation to many logic
programs that cannot be evaluated by mainstream ASP implementations. A simple
example is the following.

$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})}}$
$\displaystyle\leftarrow$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}(n))}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{more}}(n)}}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{stop}}(n)}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}(n)}},\neg{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{more}}(n)}}$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{more}}(n)}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}(n)}},\neg{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{stop}}(n)}}$

This program has a reasonable set of stable models: each finite stable model
can be interpreted as a process that counts up from zero until, at some point,
it stops.

$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})}},$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{stop}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})}}\\}$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}}))}},$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{more}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}}))}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{stop}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}}))}}\\}$
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}}))}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{visit}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})))}},$
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{more}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}}))}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{more}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}}))}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{stop}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{s}}({\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{z}})))}}\\}$
$\displaystyle\cdots$

Mainstream answer set programming languages operate in two phases. First, they
replace the program with a logically equivalent set of variable free rules
(this step is called grounding). Then they find the stable models of that
ground program (this step is called solving). This two-step process only works
if the grounder can proactively characterize all possible solutions with a
finite number of rules, and this is not the case for the program above.

Within the literature on answer set programming, lazy grounding systems have
been explored as ways to avoid the strict ground-then-solve approach (Dal Palù
et al., 2009; Lefévre et al., 2017; Dao-Tran et al., 2012; Weinzierl, 2017),
and at least one implementation of ASP with lazy grounding, Alpha, is able to
return solutions to the example above. However, work on lazy grounding
generally has not considered expressiveness: lazy grounding is trying to
circumvent exponential blowup frequently encountered in grounders, not the
outright non-termination engendered by our example above. The only work we’re
aware of that uses lazy grounding to solve programs with no finite grounding
is recent work by Comploi-Taupe et al. (Comploi-Taupe et al., 2023).

##  4\. finite-choice logic programming by example

We present the following examples to demonstrate common idioms that arise
naturally in writing and reasoning about finite-choice logic programs.

###  4.1. Spanning tree creation

(15)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(x,y)}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(y,x)}}$
(16)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{root}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{x}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(x,y)}}$
(17)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{parent}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{x\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{root}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{x}}}$
(18)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{parent}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{y}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(x,y)}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{parent}}({y})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{z}}}$
Figure 2. A finite-choice logic program that determines spanning trees for
undirected graphs.

Seeded with an
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>relation, the finite-choice logic program in Figure 2 will pick an arbitrary
node and construct a spanning tree rooted at that node. The structure of this
program is such that it’s not possible to make forward progress that
indirectly leads to conflicts: rule 16 can only apply once in a series of
deductions, and rules 17 and 18 cannot fire at all until some root is chosen.
A node can only be added to the tree once, with a parent that already exists
in the tree, so this is effectively a declarative description of Prim’s
algorithm without weights.

The creation of an arbitrary spanning tree for an undirected graph is a common
first benchmark for datalog extensions that admit multiple solutions. Most
previous work makes a selection greedily and either discards any future
contradictory selections (Krishnamurthy and Naqvi, 1988; Giannotti et al.,
2001; Greco and Zaniolo, 2001; Hu et al., 2021), or else avoids contradictory
deductions by having the first deduction consume a linear resource (Simmons
and Pfenning, 2008).

###  4.2. Appointing canonical representatives

When we want to check whether two nodes in an undirected graph are in the same
connected component, one option is to compute the transitive closure of the
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>relation. However, in a sparse graph, that can require computing $O(n^{2})$
facts for a graph with $n$ edges.

(19)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(x,y)}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(y,x)}}$
(20)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{representative}}({x})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{x}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{node}}(x)}}$
(21)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{representative}}({y})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{z\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{edge}}(x,y)}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{representative}}({y})}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{z}}}$
Figure 3. A finite-choice logic program that appoints canonical
representatives for connected components of an undirected graph.

An alternative is to appoint an arbitrary member of each connected component
as the canonical representative of that connected component: then, two nodes
are in the same connected component if and only if they have the same
canonical representative. This is the purpose of the program in Figure 3. In
principle, it’s quite possible for this program to get stuck in dead ends: if
nodes
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}$
are connected by an edge, then rule 20 could appoint both nodes as a canonical
representative, and rule 17 would then prevent any extension of that database
from being a solution. In the greedy-choice languages mentioned in the
previous section, this would be a problem for correctness: incorrectly firing
an analogue of rule 20 would mean that a final database might contain two
canonical representatives in a connected component. In finite-choice logic
programming, because closed rules can lead to the outright rejection of a
database, this is merely a problem of efficiency: we would like to avoid going
down these dead ends.

We can reason about avoiding certain dead ends, and thereby finite-choice
logic programs like this one as predictable algorithmic specifications, by
assuming a mode of execution that we call deduce, then choose. The deduce-
then-choose strategy dictates that a transition which only allows a single
database evolution ($D\operatorname{\Rightarrow}_{P}\\{D^{\prime}\\}$ with
$D\neq D^{\prime}$) will always be favored over a transition that has two or
more resulting databases.

Endowed with the deduce-then-choose execution strategy, this program will
never make deductions that indirectly lead to conflicts. First, rule 19 will
ensure that the edge relation is symmetric. Once that is complete, execution
will be forced to choose some canonical representative using rule 20 in order
to make forward progress. Once a representative is chosen, rule 21 will
exhaustively assign that newly-appointed representative to every other node in
the connected component, at which point rule 20 may fire again for a node in
another connected component.

###  4.3. Satisfiability

The previous two examples focus on techniques for avoiding reaching databases
that are not solutions. However, the full expressive power of finite-choice
logic programming comes from the ability to represent problems where that
avoidance is not always possible. Since answer set programming generalizes
boolean satisfiability, it should be no surprise that boolean satisfiability
problems can be represented straightforwardly in finite-choice logic
programming.

A Boolean satisfiability problem in conjunctive normal form is a conjunction
of clauses, where each clause is a a disjunction of propositions
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>and negated propositions
$\neg{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>We represent a CNF-SAT instance in finite-choice logic programming by
explicitly assigning each proposition to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}$
or
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$
by a closed rule, and adding a rule for each clause that causes a value
conflict for the
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>predicate if the clause’s negation holds: see Figure 4 for an example. The
deduce-then-choose execution strategy doesn’t give any advantages for a
finite-choice logic program like this, because the only meaningful deduction
is observing inconsistencies that result from already-selected choices.

(22)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}\\}}}}$
$\displaystyle\leftarrow$ (23)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}\\}}}}$
$\displaystyle\leftarrow$ (24)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{r}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}\\}}}}$
$\displaystyle\leftarrow$ (25)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{assignment}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{consistent}}\\}}}}$
$\displaystyle\leftarrow$ (26)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{assignment}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{inconsistent}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}$
(27)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{assignment}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{inconsistent}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{r}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
Figure 4. A finite-choice logic program representing the SAT instance
$(p\vee\neg q)\wedge(\neg p\vee q\vee r)$.

##  5\. The denotational meaning of a finite-choice logic program

We presented the semantics in Section 2 as a concise operational definition
for finite-choice logic programs. It does not provide a good basis for
implementation. Consider the following program $P$:

(28)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{a}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}\\}}}}$
$\displaystyle\leftarrow$ (29)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}\\}}}}$
$\displaystyle\leftarrow$ (30)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is?}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}$
$\displaystyle\leftarrow$ (31)
$\displaystyle{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}\\}}}}$
$\displaystyle\leftarrow{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{x}}}$

Under the operational semantics in Section 2, the following sequence of steps
lets us derive
$\varnothing\operatorname{\leadsto}^{*}_{P}\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$:

(by 29) $\displaystyle\varnothing$
$\displaystyle\operatorname{\leadsto}_{P}\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}\\}$
(by 30)
$\displaystyle\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}\\}$
$\displaystyle\operatorname{\leadsto}_{P}\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}\\}$

The result is not a solution and cannot be extended to a solution. The first
step led us to a dead end — a database $D$ where there is no solution
$D^{\prime}$ such that $D\operatorname{\leadsto}^{*}_{P}D^{\prime}$. The
second transition would be avoided by the deduce-then-choose execution
strategy introduced in Section 4.2, but even then, deriving
${{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{tt}}}}}$
by rule 31 only leads us further into the dead end.

Some dead ends are unavoidable when the conflicting assignments only occur
down significant chains of deduction: that’s part of what gives finite-choice
logic programming its expressive power. In this program, though, the conflict
was in some sense immediate: we always had enough information to know that
rule 28 and rule 29 both apply, and the overlap of these closed rules means
that
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>can only be given the value
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{b}}$.

The primary objective in this section is defining a well-behaved immediate
consequence operator $T_{P}(D)$ that captures global information about how a
database may evolve under simultaneous rule applications. A key part of this
development revisits how we represent the choice presented by open rules:
according to the semantics in Section 2, when we apply rule 30 to the database
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}}\\}$,
we are presented with a choice to either accept the assignment of
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$
or to make no changes to the database. Instead, here, we represent the choice
as accepting or rejecting the assignment. This means that the database must
track negative information about what values an attribute does not have in
addition to positive information about what value an attribute has. That is,
the first choice is represented by evolving to the database
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}}}}\\}$
as before, but the other option is represented as
$\\{{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{p}}}\operatorname{{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\underline{\textrm{{is}}}}}}{{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{c}}}}},{{{\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color@gray@fill{.5}\mathit{q}}}\operatorname{{\color[rgb]{.5,0,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,0,.5}{\underline{\textrm{{isnot}}}}}}{{\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}\\}}}}\\}$,
a database that rejects the assignment of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{ff}}$
to
${\color[rgb]{.5,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{.5,.5,.5}\pgfsys@color@gray@stroke{.5}\pgfsys@color<EMAIL_ADDRESS>
While the immediate consequence operator requires a fair amount of technical
development, it has two significant benefits: first, it allows us to define
the meaning of finite-choice logic program programs the same way the we define
the meaning of datalog programs: as the least fixed point of an immediate
consequence function. Additionally, the technical developments in this section
are fundamental for how we reason about the implementation we present in
Section 6.

###  5.1. Bounded-complete posets

In Section 2, we define databases as sets with an auxiliary definition of
consistency. Here, we introduce a semilattice-like structure and generalize
consistency to a broader notion of compatibility.

###### Definition 5.1.

If $\mathscr{D}$ is a set equipped with a partial order $\leq$, then a subset
$X\subseteq\mathscr{D}$ is _compatible_ when it has an upper bound, i.e.
$\exists y\mathop{\in}\mathscr{D}\ \forall x\mathop{\in}X.\ x\leq y$. We write
${\parallel}X$ to assert that $X$ is compatible and ${\not\parallel}X$ for its
negation. As a binary operator $x\parallel y={\parallel}\\{x,y\\}$ and
$x\not\parallel y={\not\parallel}\\{x,y\\}$.

###### Definition 5.2.

A _bounded-complete poset_
$(\mathscr{D},\leq_{\mathscr{D}},\bot_{\mathscr{D}},{\bigvee}_{\mathscr{D}})$
is a poset with a least element where all compatible subsets have least upper
bounds. In detail:

  1. (1)

${\leq}_{\mathscr{D}}\subseteq\mathscr{D}\times\mathscr{D}$ is a partial order
(a reflexive, transitive, antisymmetric relation).

  2. (2)

$\bot_{\mathscr{D}}\in\mathscr{D}$ is the least element: $\forall
x\in\mathscr{D}.\ \bot\leq x$.

  3. (3)

${\bigvee}_{\mathscr{D}}:\\{X\subseteq\mathscr{D}:{\parallel}X\\}\rightarrow\mathscr{D}$
finds the least upper bound of a compatible set of elements: $(\forall x\in
X.\ x\leq z)\implies\bigvee_{\mathscr{D}}X\leq z$. As a binary operator,
$x\vee_{\mathscr{D}}y=\bigvee_{\mathscr{D}}\\{x,y\\}$.

###  5.2. Constraints

Databases no longer act just as maps from attributes to values: in this new
semantics, databases map attributes to a data structure we refer to as a
_constraint_.

###### Definition 5.3.

A _constraint,_ $c\in\mathit{Constraint}$, is either
${\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}{\mathsf{just}}}(t)$
for some ground term $t$ or