A semi-numerical method for one-scale problems applied to the $\overline{\rm
MS}$-on-shell relation

Matteo Fael1, Fabian Lange1,2, Kay Schönwald1, Matthias Steinhauser1$\star$

1 Institut für Theoretische Teilchenphysik, Karlsruhe Institute of Technology
(KIT),

76128 Karlsruhe, Germany

2 Institut für Astroteilchenphysik, Karlsruhe Institute of Technology (KIT),

76344 Eggenstein-Leopoldshafen, Germany

*<EMAIL_ADDRESS>
15th International Symposium on Radiative Corrections:
Applications of Quantum Field Theory to Phenomenology,
FSU, Tallahasse, FL, USA, 17-21 May 2021 10.21468/SciPostPhysProc.

## Abstract

We discuss a practical approach to compute master integrals entering physical
quantities which depend on one parameter. As an example we consider four-loop
QCD corrections to the relation between a heavy quark mass defined in the
$\overline{\rm MS}$ and on-shell scheme in the presence of a second heavy
quark.

##  1 Introduction

At this conference a large number of very impressive and complicated
calculations to multi-loop and multi-leg processes have been presented. With
increasing number of scales and loops analytic results are more and more
difficult to obtain. It is thus often necessary to rely on numerical
approaches. As an intermediate step we present in this contribution a semi-
analytic method, which we discuss for a problem which depends on one
parameter, $x$, usually the ratio of two kinematic invariants. Semi-analytic
means that we construct numerical approximations for the master integrals
whereas all other steps of the calculation are analytic.

In contrast to many other methods on the market which have a similar aim (see,
e.g., Refs. [1, 2, 3, 4, 5, 6]) our approach is tailored to practical
applications as has been demonstrated in Ref. [7] where four-loop
contributions to the $\overline{\rm MS}$-on-shell relation with two mass
scales have been computed. We can treat systems which involve ${\cal O}(100)$
master integrals and obtain a precision of the final result which is
sufficient for phenomenological applications. At the moment our approach is
formulated for problems which depend only on one parameter. Furthermore, we do
not aim for a precision of hundreds of digits.

In these proceedings we review the findings of Ref. [7] and provide further
details on the calculation. In particular we discuss results for one non-
trivial four-loop master integral.

##  2 The method

The basic idea of our method is very simple: For a given set of master
integrals we establish the system of differential equations. Then we compute
the master integrals for a convenient value of $x=x_{0}$, which is not
necessarily physical, and use these results as boundary conditions to
construct a power-log expansion. Up to this point the calculation is in
general analytic. Let us assume we want to compute the master integrals at the
point $x=x_{1}$. This is achieved with the help of a power-log expansion
around $x=x_{1}$, which is again constructed with the help of the differential
equations. The boundary conditions are obtained at a suitable value of
$x=x_{01}$ between $x_{0}$ and $x_{1}$, where both expansions converge, by
evaluating numerically the first expansion around $x=x_{0}$. We call this step
numerical matching. This step can be repeated, if necessary several times, in
order to arrive at any desired value of $x$.

There are only few requirements, which have to be fulfilled to apply this
method. In particular, it is not necessary to derive a system of differential
equations in Fuchsian or even canonical form. One only has to avoid that
$1/\epsilon$ poles are present on the diagonal of the matrix obtained from the
differential equations. Furthermore, it is not necessary that the set of
master integrals is minimal. It is advantageous that the boundary conditions
at $x=x_{0}$ are analytic, however, in principle even they be can available in
numeric form. The major part of the CPU time is needed for deriving the linear
system of equations fulfilled by the series coefficients of the master
integrals, solving such linear system and performing the numerical matching.
In case one only has to deal with a simple Taylor expansion it only takes
several hours even in case a few dozens of expansion terms are considered. On
the other hand, in case one has a power-log expansion the complexity increases
significantly, in particular if two powers of logarithms appear for each new
order of $\epsilon$.

In the next Section we discuss eight colour factors for the $\overline{\rm
MS}$-on-shell relation. We consider four-loop two-scale integrals with
$x=m_{2}/m_{1}$ where for the external momentum $q$ we have $q^{2}=m_{1}^{2}$.
The mass $m_{2}$ appears in closed fermion loops. In the limit $m_{2}\gg
m_{1}$ an analytic evaluation is possible since one ends up with tadpole
integrals up to four loops and on-shell integral up to three loops. For these
kind of one-scale integrals both the reduction to master integrals and
analytic expressions of the latter are well known. We compute 50 terms for the
power-log expansion around $1/x=0$, which shows good convergence properties,
even down to $x\approx 1.5$. At this point we match to the Taylor expansion
around $x=1$. The expansion around $x=0$ is again a power-log expansion which
we match at $x=0.5$ to the $x=1$ expansion.

For our application it is indeed sufficient to construct only three
expansions. In general it might be that the differential equations contain
poles which limit the radius of convergence. In these cases on has to
introduce further matching points. In case these poles are spurious a simple
Taylor expansion is in general sufficient. For the cases where the poles have
a physical origin it might be that a power-log expansion is necessary.

##  3 Mass relation

|  |  |
---|---|---|---
(a) | (b) | (c) | (d)
|  |  |
(e) | (f) | (g) | (h)
Figure 1: Sample Feynman diagrams contributing to relation between the
$\overline{\rm MS}$ and on-shell mass. Straight and curly lines represent
quarks and gluons, respectively. Dashed and double lines represent massless
fermions and fermions with mass $m_{2}$, respectively.

The quark mass relation, which is considered in this section, involves
renormalized heavy quarks in the most important renormalization schemes: the
on-shell and the $\overline{\rm MS}$ scheme. In Ref. [8, 9] it has been
computed to four-loop order assuming that all lighter quarks have mass zero.
Analytic results for the contributions involving two different masses are only
known at three loops from Refs. [10, 11]. At four loops such corrections have
been considered for the first time in Ref. [7]. Results for the eight colour
factors111There are 16 colour factors in total.

$\displaystyle C_{F}T_{F}^{3}n_{m}n_{l}^{2},\quad
C_{F}T_{F}^{3}n_{m}n_{l}n_{h},\quad C_{F}T_{F}^{3}n_{m}n_{h}^{2},\quad
C_{F}T_{F}^{3}n_{m}^{2}n_{l},$ $\displaystyle
C_{F}T_{F}^{3}n_{m}^{2}n_{h},\quad C_{F}T_{F}^{3}n_{m}^{3},\quad
C_{F}^{2}T_{F}^{2}n_{m}n_{l},\quad C_{F}C_{A}T_{F}^{2}n_{m}n_{l},$ (1)

have been obtained using the method described in the previous Section. They
all either contain three closed fermion loops or two closed fermion loops
where one of them has the mass $m_{2}$ and the other is massless. Sample
Feynman diagrams are shown in Fig. 1. The numerical results, which are
available for any value of $x=m_{2}/m_{1}$, have been compared to the analytic
expressions, which have also been obtained in [7].

Figure 2:  Graphical representation of the master integral in Eq. (2). Dashed,
solid and double lines represent scalar propagators of mass 0, $m_{1}$ and
$m_{2}$.

For our calculation we have to consider 339 master integrals. In the following
we discuss in detail the seven-line master integral (see Fig. 2)

$\displaystyle J(x)$ $\displaystyle=$ $\displaystyle\verb|d4L456[1, 0, 0, 1,
1, 1, 1, 0, 0, 1, 1, 0, 0, 0]|\,,$ (2)

which starts at order $1/\epsilon^{4}$. In our calculation it is needed
including the ${\cal O}(\epsilon)$ terms. In Ref. [7] the expansion around
$x=0$, $1$ and $\infty$ have been computed using the approach discussed in the
previous Section. Furthermore, the analytic result could be obtained. Note,
however, that the ${\cal O}(\epsilon)$ term of $J(x)$ contains cyclotomic
harmonic polylogarithms up to weight 6, which cancel in the proper sum for the
quark mass relation. It is both a non-trivial task to compute them numerically
and to perform an analytic expansion. However, it is straightforward to obtain
its value at $x=0$:

$\displaystyle J(0)$ $\displaystyle=$
$\displaystyle-\frac{1}{12\epsilon^{4}}-\frac{13}{24\epsilon^{3}}+\frac{1}{\epsilon^{2}}\left(-\frac{15}{16}-\frac{13\pi^{2}}{36}\right)+\frac{1}{\epsilon}\left(\frac{1135}{96}-\frac{169\pi^{2}}{72}-\frac{86\zeta_{3}}{9}\right)$
(3)
$\displaystyle+\frac{28699}{192}-\frac{65\pi^{2}}{16}-\frac{559\zeta_{3}}{9}-\frac{149\pi^{4}}{90}+\epsilon\left(\frac{144429}{128}+\frac{14755\pi^{2}}{288}-\frac{227\zeta_{3}}{2}\right.$
$\displaystyle\left.-\frac{1937\pi^{4}}{180}-\frac{1118\pi^{2}\zeta_{3}}{27}-\frac{7604\zeta_{5}}{15}\right)+{\cal
O}(\epsilon^{2})\,.$

For this reason we perform in the following the comparison with the exact
results only for $x=0$. Note that our starting point is the $x\to\infty$
limit.

Figure 3:  ${\cal O}(\epsilon)$ term of the integral $J$. The solid red, green
and blue curves correspond to the expansions in $x$, $1-x$ and $1/x$. For the
dashed orange curve the expansion parameter $1-1/x$ has been used.

In Fig. 3 we show results for the ${\cal O}(\epsilon)$ term of $J(x)$ for
$0\leq x\leq 4$ where the red, green and blue solid curves correspond to the
expansions in $x$, $1-x$ and $1/x$, including 50 expansion terms. They are the
immediate results of our method and perfectly cover the whole $x$ range. The
dashed orange curve corresponds to the expansion in $1-1/x$ which is obtained
from the $1-x$ expansion. It is interesting to note that the green curve leads
to better results for $x<1$ whereas $(1-1/x)$ is the better choice for the
expansion parameter for $x>1$. In fact, in the plot there is no visible
difference between the blue and orange curve. Even for x=8 the deviation is
still below 10%.

Figure 4:  Difference of expansions. The number of digits on the $y$ axis is
given by “$-\log_{10}(\mbox{difference})$”.

Let us next discuss the numerical accuracy. We remark that we can reproduce
the analytic result for $x=0$ in Eq. (3) with a relative precision of
$10^{-13}$ for the ${\cal O}(\epsilon)$ term. The lower $\epsilon$ terms are
even more precise; for example, the ${\cal O}(\epsilon^{0})$ term has a
precision of $10^{-17}$. Remember that $J(0)$ is obtained from analytic
calculations at $x\to\infty$ and numerical matching for $x=0.5$ and $x=1.5$.
In order to quantify the quality of the approximations we consider in Fig. 4
differences of expansions of the ${\cal O}(\epsilon)$ term. The interesting
regions are around the matching points $x=0.5$ and $x=1.5$ where we observe
differences of order $10^{-12}$ to $10^{-13}$. Taking into account that the
${\cal O}(\epsilon)$ term itself is of order $10^{2}-10^{3}$ (cf. Fig. 3) we
can claim a relative precision of more than 14 digits. Away from the matching
points the respective expansion provides even better results.

In Fig. 4 we show two versions of the expansion around $x=1$. The cyan and red
curves use $(1-x)$ as expansion parameter and the pink and blue curves use
$(1-1/x)$. As already observed in Fig. 3 we again deduce that $(1-1/x)$ is a
better choice for $x>1$ whereas $(1-x)$ is better suited from $x<1$.

In Ref. [7] expansions for all 339 master integrals have been obtained and
then the mass relations for the eight colour factors of Eq. (1) have been
constructed. In Ref. [7] also (exact) analytic results for all 339 master
integrals have been computed. This allows for a comparison of the final
physical quantity. We could show that the agreement between the exact and
approximated results is at least 10 significant digits for the bare four-loop
quantity. For most colour factors this is also true for the renormalized
quantities. Due to logarithmic divergences (e.g., the colour structure
$C_{F}^{2}n_{l}n_{h}$ for $x\to 0$) one observes strong cancellations in some
regions of the parameters space. However, we still have 5 significant digits
in the final expression. For more details we refer to Ref. [7]. This is
promising for the remaining eight colour factors where most likely no analytic
results in terms of iterated integrals can be obtained.

##  4 Conclusion

In this contribution we have described a method which can be used to obtain
semi-analytic results for multi-loop problems which depend on one parameter
$x$. As an example four-loop corrections to the heavy quark mass relation with
two mass scales, $m_{1}$ and $m_{2}$, have been considered. Using analytic
results for $m_{2}\gg m_{1}$ it is possible to use the differential equations
for the master integrals to transfer the information to $x=0$. The comparison
to the known analytic result shows that a precision between 5 and 10 digits
can be obtained. Using deeper expansions and/or further intermediate matching
points even a higher accuracy can be achieved. Detailed result for one of the
master integrals has been presented in this contribution. For the results of
the mass relation we refer to Ref. [7].

## Acknowledgements

This research was supported by the Deutsche Forschungsgemeinschaft (DFG,
German Research Foundation) under grant 396021762 — TRR 257 “Particle Physics
Phenomenology after the Higgs Discovery”.

## References

  * [1] R. Boughezal, M. Czakon and T. Schutzmeier, “NNLO fermionic corrections to the charm quark mass dependent matrix elements in $\bar{B}\to X_{s}\gamma$,” JHEP 09 (2007), 072, 10.1088/1126-6708/2007/09/072, [arXiv:0707.3090 [hep-ph]].
  * [2] R. N. Lee, A. V. Smirnov and V. A. Smirnov, “Solving differential equations for Feynman integrals by expansions near singular points,” JHEP 03 (2018), 008, 10.1007/JHEP03(2018)008, [arXiv:1709.07525 [hep-ph]].
  * [3] X. Liu, Y.-Q. Ma and C.-Y. Wang, “A Systematic and Efficient Method to Compute Multi-loop Master Integrals,” Phys. Lett. B 779 (2018), 353-357, 10.1016/j.physletb.2018.02.026, [arXiv:1711.09572 [hep-ph]].
  * [4] J. Blümlein and C. Schneider, “The Method of Arbitrarily Large Moments to Calculate Single Scale Processes in Quantum Field Theory,” Phys. Lett. B 771 (2017), 31-36, 10.1016/j.physletb.2017.05.001, [arXiv:1701.04614 [hep-ph]].
  * [5] F. Moriello, “Generalised power series expansions for the elliptic planar families of Higgs + jet production at two loops,” JHEP 01 (2020), 150, 10.1007/JHEP01(2020)150, [arXiv:1907.13234 [hep-ph]].
  * [6] M. Hidding, “DiffExp, a Mathematica package for computing Feynman integrals in terms of one-dimensional series expansions,” Comput. Phys. Commun. 269 (2021), 108125, 10.1016/j.cpc.2021.108125, [arXiv:2006.05510 [hep-ph]].
  * [7] M. Fael, F. Lange, K. Schönwald and M. Steinhauser, “A semi-analytic method to compute Feynman integrals applied to four-loop corrections to the $\overline{\rm MS}$-pole quark mass relation,” JHEP 09 (2021), 152, https://doi.org/10.1007/JHEP09(2021)152 [arXiv:2106.05296 [hep-ph]].
  * [8] P. Marquard, A. V. Smirnov, V. A. Smirnov and M. Steinhauser, “Quark Mass Relations to Four-Loop Order in Perturbative QCD,” Phys. Rev. Lett. 114 (2015), 142002, 10.1103/PhysRevLett.114.142002, [arXiv:1502.01030 [hep-ph]].
  * [9] P. Marquard, A. V. Smirnov, V. A. Smirnov, M. Steinhauser and D. Wellmann, “$\overline{\rm MS}$-on-shell quark mass relation up to four loops in QCD and a general SU$(N)$ gauge group,” Phys. Rev. D 94 (2016), 074025, 10.1103/PhysRevD.94.074025, [arXiv:1606.06754 [hep-ph]].
  * [10] S. Bekavac, A. Grozin, D. Seidel and M. Steinhauser, “Light quark mass effects in the on-shell renormalization constants,” JHEP 10 (2007), 006, 10.1088/1126-6708/2007/10/006, [arXiv:0708.1729 [hep-ph]].
  * [11] M. Fael, K. Schönwald and M. Steinhauser, “Exact results for ${Z}_{m}^{\mathrm{OS}}$ and ${Z}_{2}^{\mathrm{OS}}$ with two mass scales and up to three loops,” JHEP 10 (2020), 087, 10.1007/JHEP10(2020)087, [arXiv:2008.01102 [hep-ph]].


# FO(FD): Extending Classical Logic with Rule-Based Fixpoint Definitions

PING HOU  BROES DE CAT and MARC DENECKER
Department of Computer Science  K.U.Leuven  Belgium
{ping.hou, broes.decat<EMAIL_ADDRESS>
###### Abstract

We introduce fixpoint definitions, a rule-based reformulation of fixpoint
constructs. The logic FO(FD), an extension of classical logic with fixpoint
definitions, is defined. We illustrate the relation between FO(FD) and FO(ID),
which is developed as an integration of two knowledge representation
paradigms. The satisfiability problem for FO(FD) is investigated by first
reducing FO(FD) to difference logic and then using solvers for difference
logic. These reductions are evaluated in the computation of models for FO(FD)
theories representing fairness conditions and we provide potential
applications of FO(FD).

##  1 Introduction

Two mainstream knowledge representation paradigms of the moment are on the one
hand, classical logic-based approaches such as description logics [Baader et
al. (2003)], and on the other hand, rule-based approaches from logic
programming and extensions such as Answer Set Programming and Abductive Logic
Programming [Baral (2003), Kakas et al. (1992)]. The latter disciplines are
rooted in the discipline of Non-Monotonic Reasoning [McCarthy (1986)]. FO(ID)
[Denecker and Ternovska (2008)] integrates both paradigms in a tight,
conceptually clean manner. The key to integrate “rules” into classical logic
(FO) is the observation that natural language, or more precisely, the informal
language of mathematicians, has an informal rule-based construct: the
construct of inductive/recursive definitions (IDs). FO(ID) extends FO not only
with an inductive definition construct but also with an expressive and precise
non-monotonic reasoning principle. It is an extension of FO with inductive
definitions and an integration of FO and LP. It integrates monotonic and non-
monotonic logics. The inductive definition construct of FO(ID) formally
generalizes Datalog [Abiteboul et al. (1995)]. FO(ID) is also strongly related
to fixpoint logics. Monotone definitions in FO(ID) are a different rule-based
syntactic sugar of the fixpoint formulas of Least Fixpoint Logic (LFP) [Park
(1969)]. Last but not least, FO(ID), being a clear, well-founded integration
of rules into classical logic, might play a unifying role in the current
attempts of extending FO-based description logics with rules [Vennekens and
Denecker (2009)]. It thus appears that FO(ID) occupies quite a central
position in the spectrum of computational and knowledge representation logics.

The work in this paper is inspired by work on FO(ID) to integrate LP-style
rules into fixpoint constructs. The resulting constructs are called fixpoint
definitions (FDs). Fixpoint definitions use the rule-based format which will
enable us to more easily link fixpoint constructs with the rule-based
knowledge representation paradigm and the FO(ID) formalism. We define the
logic FO(FD), which is an extension of classical logic with fixpoint
definitions. In FO(FD), almost all kinds of inductions can be expressed in a
natural way. The study of FO(FD) contributes to the understanding of rule-
based systems and thus, to the study of the relation between non-monotonic
inductive definitions and fixpoint definitions, to the study of the
correspondence between well-founded and fixpoint semantics and to the
integration of classical logic-based and rule-based approaches for knowledge
representation.

We investigate the connection between FO(FD) and FO(ID) by presenting
equivalence preserving transformations from FO(ID) to FO(FD). It turns out
that all kinds of inductive definitions in FO(ID) can be expressed in FO(FD).
Meanwhile, due to the allowance of the nesting of least and greatest fixpoint
constructs in FO(FD), the nesting of induction and coinduction can be
represented in FO(FD). Thus, some concepts, e.g., infinite structures and the
nesting of recursion and corecursion [Barwise and Moss (1996)], which can not
be defined in FO(ID) in a well-founded way, can be handled naturally in
FO(FD). We show that in general, FO(FD) is strictly more expressive than
FO(ID).

On the computational level, the satisfiability problem for FO(FD), deciding
the satisfiability of FO(FD) theories, is a major research topic. One research
direction is towards developing solvers for extensions of propositional logic,
e.g., SMT. Difference logic [Nieuwenhuis and Oliveras (2005)] can be seen as
an instance of an SMT framework where propositional logic is extended with
simple linear constraints. Efficient implementation techniques for difference
logic are emerging in the SMT domain [Nieuwenhuis and Oliveras (2005), Cotton
and Maler (2006)], which makes it a good choice as base technology. In this
paper, we develop translations from FO(FD) to difference logic, based on
similar reductions of logic programs presented in [Janhunen et al. (2009),
Niemelä (2008)]. The translations reduce the satisfiability check of FO(FD)
theories to finding satisfying interpretations of difference logic theories.
This provides a novel approach to model expansion for FO(FD). We also present
experimental results.

The paper is organized as follows. In Section 2, we introduce fixpoint
definitions and the logic FO(FD). FO(ID) and the relationship between FO(FD)
and FO(ID) are presented in Section 3. We investigate the satisfiability
problem for FO(FD) by providing the reductions from FO(FD) to difference logic
in Section 4. The reductions are evaluated experimentally in Section 5. In
Section 6, we present some potential applications of FO(FD) and a conclusion
follows in Section 7.

##  2 FO(FD): A logic of fixpoint definitions

In this section, we extend first-order logic (FO) with an alternative rule-
based fixpoint construct: the construct of fixpoint definitions (FDs), to
formalize a new logic FO(FD), which can be viewed as an extension of first-
order logic with mixed induction and coinduction.

###  2.1 Syntax

We assume familiarity with classical logic. A vocabulary $\Sigma$ consists of
a set of predicate and function symbols. Terms and FO formulae are defined as
usual, and are built inductively from variables, constant and function
symbols, logical connectives ($\neg$, $\land$, $\lor$) and quantifiers
($\forall$, $\exists$). Note that predicate symbols occurring in a fixpoint
definition are viewed as predicate constants but not predicate variables.

A rule over a vocabulary $\Sigma$ is an expression of the form
$\forall\overline{x}(P(\overline{x})\leftarrow\varphi[\overline{x}])$, where
$P$ is a predicate symbol of $\Sigma$ and $\varphi[\overline{x}]$ is an
arbitrary first-order formula over $\Sigma$. Atomic formula $P(\overline{x})$
is known as the head of the rule and $\varphi[\overline{x}]$ is known as the
body of the rule. The defined predicate of the rule is $P$. The connective
$\leftarrow$ is called definitional implication and is to be distinguished
from material implication $\supset$, an abbreviation for $\lnot body\lor
head$. We say that a predicate symbol occurs positively (negatively) in a
formula if it occurs in the scope of an even (odd) number of negations. A rule
is positive in a set of predicate symbols if these symbols occur only
positively in $\varphi$.

For a set $\mathcal{R}$ of rules, we denote $\mbox{def}(\mathcal{R})$ as the
set of defined predicates of its rules, and we denote
$\mbox{open}(\mathcal{R})$ as the set of all other symbols occurring in
$\mathcal{R}$.

Without loss of generality, we assume from now on, that rule sets contain for
each of its defined predicates exactly one rule of the form
$\forall\overline{x}(P(\overline{x})\leftarrow\varphi_{P}[\overline{x}])$.
Indeed, any set of rules
$\\{\forall\bar{x}(P(\bar{x})\leftarrow\varphi_{1}[\overline{x}]),\ldots,\forall\bar{x}(P(\bar{x})\leftarrow\varphi_{n}[\overline{x}])\\}$
can be transformed into a single rule
$\forall\bar{x}(P(\bar{x})\leftarrow\varphi_{1}[\overline{x}]\lor\ldots\lor\varphi_{n}[\overline{x}])$.

###### Definition 2.1

We define a least fixpoint definition (LFD), respectively greatest fixpoint
definition (GFD) over vocabulary $\Sigma$ by simultaneous induction, as a
finite expression $\mathcal{D}$ of the form

$\left\lfloor\begin{array}[]{l}\mathcal{R},\Delta_{1},\dots,\Delta_{m},\nabla_{1},\dots,\nabla_{n}\end{array}\right\rfloor\mbox{,
respectively}\left\lceil\begin{array}[]{l}\mathcal{R},\Delta_{1},\dots,\Delta_{m},\nabla_{1},\dots,\nabla_{n}\end{array}\right\rceil$

with $0\leq n,m$ such that:

  1. 1.

$\mathcal{R}$ is a set of rules over $\Sigma$.

  2. 2.

Each $\Delta_{i}$ is a least fixpoint definition and each $\nabla_{j}$ is a
greatest fixpoint definition.

To express the remaining conditions, we need some auxiliary concepts and
notations. For such an expression $\mathcal{D}$, we say that a rule $r$ is
locally defined in $\mathcal{D}$ if $r\in\mathcal{R}$, and that a predicate
$P$ is locally defined in $\mathcal{D}$ if $P\in\mbox{def}(\mathcal{R})$, and
that $P$ is defined in $\mathcal{D}$ if $P$ is locally defined in
$\mathcal{D}$ or defined in any of its subdefinitions
$\Delta_{1},\dots,\nabla_{n}$. The set of defined predicates of $\mathcal{D}$
is denoted $\mbox{def}(\mathcal{D})$. A symbol is open in $\mathcal{D}$ if it
occurs in $\mathcal{D}$ and is not defined in it. The set of open symbols of
$\mathcal{D}$ is denoted $\mbox{open}(\mathcal{D})$.

  1. 3.

Every defined symbol of $\mathcal{D}$ has only positive occurrences in the
bodies of rules in $\mathcal{D}$.

  2. 4.

Each symbol $P\in\mbox{def}(\mathcal{D})$ has exactly one local definition in
$\mathcal{D}$. Formally,
$\\{\mbox{def}(\mathcal{R}),\mbox{def}(\Delta_{1}),\dots,\mbox{def}(\nabla_{n})\\}$
is a partition of $\mbox{def}(\mathcal{D}).$

  3. 5.

For every subdefinition $\mathcal{D}^{\prime}$ of $\mathcal{D}$,
$\mbox{open}(\mathcal{D}^{\prime})\subseteq\mbox{open}(\mathcal{D})\cup\mbox{def}(\mathcal{R})$.
In particular, a symbol defined in another subdefinition
$\mathcal{D}^{\prime\prime}\neq\mathcal{D}^{\prime}$, does not occur in
$\mathcal{D}^{\prime}$.

A fixpoint definition is either a least fixpoint definition or a greatest
fixpoint definition. We allow arbitrary nesting of least and greatest fixpoint
definitions.

An FO(FD) formula is either an FO formula or a fixpoint definition. An FO(FD)
theory is a set of fixpoint definitions and FO sentences.

###### Example 2.2

Assume a binary predicate $T$ denoting a transition graph on a set of
vertices, representing the states. Assume a property on states $R$, i.e., a
unary predicate on vertices. The set of states $P$ that have an (infinite)
path passing an infinite number of times through a state satisfying $R$, is
defined by:

$\left\lceil\begin{array}[]{l}\forall x\ (P(x)\leftarrow Q(x))\\\
\left\lfloor\begin{array}[]{l}\forall x\ (Q(x)\leftarrow R(x)\land\exists
y(T(x,y)\land P(y)))\\\ \forall x\ (Q(x)\leftarrow\exists y(T(x,y)\land
Q(y)))\end{array}\right\rfloor\end{array}\right\rceil$

###  2.2 Semantics

The semantics of FO(FD) is an integration of standard FO semantics with
fixpoint semantics of definitions. We start by defining the fixpoint
semantics.

Given two disjoint first-order vocabularies $\Sigma$ and $\Sigma^{\prime}$, a
$\Sigma$-interpretation $I$ and a $\Sigma^{\prime}$-interpretation
$I^{\prime}$, the $\Sigma\cup\Sigma^{\prime}$-interpretation mapping each
element $e$ of $\Sigma$ to $e^{I}$ and each $e\in\Sigma^{\prime}$ to
$e^{I^{\prime}}$ is denoted by $I+I^{\prime}$. When
$\Sigma^{\prime}\subseteq\Sigma$, we denote the restriction of a
$\Sigma$-interpretation $I$ to the symbols of $\Sigma^{\prime}$ by
${{I}\rvert_{\Sigma^{\prime}}}$. For a $\Sigma$-interpretation $I$ and a tuple
of domain elements $\overline{d}$, we denote by $I[\overline{x}/\overline{d}]$
the interpretation that has the same domain as $I$, interprets
$\overline{x}=(x_{1},\ldots,x_{n})$ by $\overline{d}=(d_{1},\ldots,d_{n})$,
and coincides with $I$ on all other symbols.

With a set $\mathcal{R}$ of rules over $\Sigma$ and a (partial) two-valued
$\Sigma$-interpretation $I$ interpreting at least all open symbols and no
defined symbols, i.e., $\Sigma\cap\mbox{def}(\mathcal{R})=\emptyset$ and
$\mbox{open}(\mathcal{R})\subseteq\Sigma$, there is a standard way of
associating an operator $\Gamma_{I}^{\mathcal{R}}$ on the set of
$\mbox{def}(\mathcal{R})$-interpretations with the domain of $I$. For two such
interpretations $J,K$, we define $\Gamma_{I}^{\mathcal{R}}(J)=K$ if for every
$\forall\overline{x}(P(\overline{x})\leftarrow\varphi_{P}[\overline{x}])\in\mathcal{R}$,
$P^{K}=\\{\overline{d}|(I+J)[\overline{x}/\overline{d}]\models\varphi_{P}[\overline{x}]\\}$.

If each defined symbol in $\mbox{def}(\mathcal{R})$ has only positive
occurrences in the body of a rule in $\mathcal{R}$, the operator
$\Gamma_{I}^{\mathcal{R}}$ is monotone with respect to the standard truth
order on interpretations and hence, it has least and greatest fixpoints in
this set denoted $\mbox{lfp}(\Gamma_{I}^{\mathcal{R}})$, respectively
$\mbox{gfp}(\Gamma_{I}^{\mathcal{R}})$. Importantly, if $P^{I}\leq
P^{I^{\prime}}$ for every symbol $P\in\mbox{open}(\mathcal{R})$ with only
positive occurrences in rule bodies of $\mathcal{R}$, then
$\mbox{lfp}(\Gamma_{I}^{\mathcal{R}})\leq\mbox{lfp}(\Gamma_{I^{\prime}}^{\mathcal{R}})$
and
$\mbox{gfp}(\Gamma_{I}^{\mathcal{R}})\leq\mbox{gfp}(\Gamma_{I^{\prime}}^{\mathcal{R}})$.

Given an expression $\mathcal{D}$ which might be an LFD or a GFD, and an
$\mbox{open}(\mathcal{D})$-interpretation $I$ interpreting at least all open
symbols of $\mathcal{D}$ and no defined ones. We define an operator
$\Gamma_{I}^{\mathcal{D}}$ on the set of
$\mbox{def}(\mathcal{D})$-interpretations with domain $dom(I)$. This operator
is monotone with respect to the standard truth order on interpretations and
hence, it has least and greatest fixpoints in this set. We define
$\Gamma_{I}^{\mathcal{D}}(J)$ inductively as the interpretation $K+K^{\prime}$
where

  * •

$K$ is the
$(\mbox{def}(\mathcal{D})\setminus\mbox{def}(\mathcal{R}))$-interpretation
such that, for $J^{\prime}=I+J|_{\mbox{def}(\mathcal{R})}$:

    * –

$K|_{\mbox{def}(\Delta_{i})}=\mbox{lfp}(\Gamma_{J^{\prime}}^{\Delta_{i}})$ for
all $i=1,\ldots,m$.

    * –

$K|_{\mbox{def}(\nabla_{j})}=\mbox{gfp}(\Gamma_{J^{\prime}}^{\nabla_{j}})$ for
all $j=1,\ldots,n$.

Observe that $J^{\prime}$ interprets all open symbols in every subdefinition
of $\mathcal{D}$.

  * •

$K^{\prime}$ is the $\mbox{def}(\mathcal{R})$-interpretation
$\Gamma_{I+K}^{\mathcal{R}}(J|_{\mbox{def}(\mathcal{R})})$.

######  Definition 2.3 (Model of $\mathcal{D}$)

Let $\mathcal{D}$ be a fixpoint definition and $I$ a two-valued
$\Sigma$-interpretation such that $\Sigma$ contains all symbols in
$\mathcal{D}$. If $\mathcal{D}$ is an LFD, then $I$ satisfies $\mathcal{D}$,
or $I$ is a model of $\mathcal{D}$, iff
$I|_{\mbox{def}(\mathcal{D})}=\mbox{lfp}(\Gamma_{I|_{\mbox{open}(\mathcal{D})}}^{\mathcal{D}})$.
If $\mathcal{D}$ is a GFD, then $I$ satisfies $\mathcal{D}$, or $I$ is a model
of $\mathcal{D}$, iff
$I|_{\mbox{def}(\mathcal{D})}=\mbox{gfp}(\Gamma_{I|_{\mbox{open}(\mathcal{D})}}^{\mathcal{D}})$.
As usual, this is denoted $I\models\mathcal{D}$.

######  Example 2.4 (Continued 2.2)

Semantically, the fixpoint definition in Example 2.2 has the following
meaning: the relationship $P$ is the result of iteratively computing a least
(for $P$) and a greatest fixpoint (for $Q$). In the $n$-th iteration of the
outer fixpoint, $P$ will contain a vertex iff it has a (finite) path that goes
through at least $n$ times through vertices with property $R$. At fixpoint,
$P$ (and $Q$) will contain a vertex iff it has a path that infinitely often
reaches a vertex with property $R$.

######  Definition 2.5 (Model of an FO(FD) theory)

Let $T$ be an FO(FD) theory over $\Sigma$ and $I$ a two-valued
$\Sigma$-interpretation. Then $I$ is a model of $T$, denoted by $I\models T$,
iff $I\models\varphi$ for every $\varphi\in T$.

######  Definition 2.6 (Equivalence)

A theory $T_{1}$ with vocabulary $\Sigma_{1}$ is equivalent to a theory
$T_{2}$ with vocabulary $\Sigma_{2}$ iff each model $M_{1}$ of $T_{1}$
restricted to $\Sigma_{2}$ can be extended to a model $M_{2}$ of $T_{2}$ and
vice versa.

###  2.3 PC(FD)

In this section, we introduce PC(FD), the propositional fragment of FO(FD). We
assume familiarity with propositional logic.

A propositional vocabulary $\Sigma$ is a set of propositional atoms. A literal
is an atom $p$ or its negation $\neg p$. An atom $p$ is called a positive
literal, $\neg p$ a negative one. For a literal $l$, we identify $\neg\neg l$
with $l$.

A propositional fixpoint definition is a fixpoint definition such that all
symbols occurring in it are propositional symbols.

###### Example 2.7

Consider the propositional fixpoint definition

$\mathcal{D}=\left\lfloor\begin{array}[]{l}p\leftarrow q\lor r\\\ q\leftarrow
p\\\ \left\lceil\begin{array}[]{l}r\leftarrow p\\\ s\leftarrow t\lor a\\\
t\leftarrow s\end{array}\right\rceil\end{array}\right\rfloor$

It is obvious that $a$ is the only open atom in this fixpoint definition.
There are only two interpretations satisfying $\mathcal{D}$, namely,
$I_{1}=\\{a\mapsto\mbox{f},p\mapsto\mbox{f},q\mapsto\mbox{f},r\mapsto\mbox{f},s\mapsto\mbox{t},t\mapsto\mbox{t}\\}$
and
$I_{2}=\\{a\mapsto\mbox{t},p\mapsto\mbox{f},q\mapsto\mbox{f},r\mapsto\mbox{f},s\mapsto\mbox{t},t\mapsto\mbox{t}\\}$.
The construction of $I_{1}$ is illustrated as follows:
$I_{1}^{1}=\\{a\mapsto\mbox{f},p\mapsto\mbox{f},q\mapsto\mbox{f},r\mapsto\mbox{t},s\mapsto\mbox{t},t\mapsto\mbox{t}\\}$
and, because the body of the only rule for $r$ is false,
$I_{1}^{2}=\\{a\mapsto\mbox{f},p\mapsto\mbox{f},q\mapsto\mbox{f},r\mapsto\mbox{f},s\mapsto\mbox{t},t\mapsto\mbox{t}\\}$,
which is the limit of the iterations and thus, $I_{1}$ = $I_{1}^{2}$.

A propositional fixpoint definition $\mathcal{D}$ is in definitional normal
form (DefNF) if for any $p\in\Sigma$, the fixpoint definition contains at most
one rule $p\leftarrow\varphi_{p}$, and either $\varphi_{p}=\bigvee B_{p}$ or
$\varphi_{p}=\bigwedge B_{p}$, where $B_{p}$ is a set of literals called the
body literals. Any propositional fixpoint definition can be transformed into
DefNF in polynomial time using Tseitin transformation [Tseitin (1968)]. Hence
without loss of generality, we can from now on assume that propositional
fixpoint definitions are in DefNF.

A PC(FD) theory is a set of propositional formulas and propositional fixpoint
definitions. An interpretation $I$ satisfies a PC(FD) theory if it satisfies
every formula and every definition of the theory.

##  3 A comparison of FO(FD) and FO(ID)

FO(ID) is an extension of first-order logic with a new construct, namely
generalized inductive definitions, for representing definitions that occur
often in mathematics, but in general cannot be expressed in first-order logic.
It was originally introduced in [Denecker (2000)], and further developed in
[Denecker and Ternovska (2008)]. In this section, we compare FO(FD) to FO(ID)
by providing transformations from generalized inductive definitions to
alternating fixpoint definitions and showing that in general, the FO(FD)
formalism is strictly more expressive than the FO(ID).

###### Definition 3.1

Let $\Sigma$ be a vocabulary. A (generalized) inductive definition (GID) $D$
over $\Sigma$ is a finite set of rules over $\Sigma$. Its sets of defined
symbols $\mbox{def}(D)$, respectively open symbols $\mbox{open}(D)$ are
defined as usual.

We do not insist on defined predicates to occur positively in rule bodies in a
generalized inductive definition, but allow non-monotone inductive
definitions.

An FO(ID) formula is a Boolean combination of FO formulas and generalized
inductive definitions. An FO(ID) theory is a set of generalized inductive
definitions and FO sentences. A model of a generalized inductive definition is
a two-valued well-founded model [Denecker and Ternovska (2008)]. The semantics
of FO(ID) is an integration of standard two-valued FO semantics with the well-
founded semantics of generalized inductive definitions.

###### Example 3.2

Consider the following non-monotone inductive definition of even and odd
numbers over the structure of the natural numbers with zero and the successor
function:

$\left\\{\begin{array}[]{l}\forall x(Even(x)\leftarrow x=0\lor\exists
y(x=s(y)\land\neg Even(y)))\\\ \forall x(Odd(x)\leftarrow\exists y(x=s(y)\land
Even(y)))\end{array}\right\\}$

We begin our comparison of FO(FD) and FO(ID) by presenting equivalence
preserving transformations from generalized inductive definitions to
alternating fixpoint definitions. New symbols may be introduced to the
original vocabulary $\Sigma$.

###### Definition 3.3

Let $D$ be a generalized inductive definition. For each defined predicate $P$
of $D$, we introduce a new predicate symbol $P^{\neg}$ of the same arity of
$P$. For each formula $\varphi$, let $\overline{\varphi}$ denote the formula
obtained by substituting each negative occurrence $P(\bar{t})$ of a defined
predicate $P$ in $\varphi$ by $\lnot P^{\neg}(\bar{t})$. We define two sets of
rules:
$\mathcal{R}_{D}=\\{\forall\bar{x}(P(\bar{x})\leftarrow\overline{\varphi_{P}[\bar{x}]})\mid
P\in\mbox{def}(D)\\}$ and
$\mathcal{R}^{\neg}_{D}=\\{\forall\bar{x}(P^{\neg}(\bar{x})\leftarrow\overline{\neg\varphi_{P}[\bar{x}]})\mid
P\in\mbox{def}(D)\\}$. Now define $\Delta_{D}$ as
$\left\lfloor\begin{array}[]{l}\mathcal{R}_{D},\left\lceil\begin{array}[]{l}\mathcal{R}^{\neg}_{D}\end{array}\right\rceil\end{array}\right\rfloor$.

Let $D$ be a generalized inductive definition over $\Sigma$. Then $\Delta_{D}$
is a least fixpoint definition over $\Sigma^{\prime}=\Sigma\cup\\{P^{\neg}\mid
P\in\mbox{def}(D)\\}$. Note that $\mbox{open}(D)=\mbox{open}(\Delta_{D})$.

######  Example 3.4 (Continued 3.2)

Translating the previous FO(ID) formula into FO(FD) leads to

$\left\lfloor\begin{array}[]{l}\forall x(Even(x)\leftarrow x=0\lor\exists
y(x=s(y)\land{Even}^{\neg}(y)))\\\ \forall x(Odd(x)\leftarrow\exists
y(x=s(y)\land Even(y)))\\\ \left\lceil\begin{array}[]{l}\forall
x({Even}^{\neg}(x)\leftarrow x\not=0\land\forall y(x=s(y)\supset Even(y)))\\\
\forall x({Odd}^{\neg}(x)\leftarrow\forall
y(x=s(y)\supset{Even}^{\neg}(y)))\end{array}\right\rceil\end{array}\right\rfloor$

###### Theorem 3.5

Let $D$ be a generalized inductive definition over $\Sigma$. Then there exists
a one-to-one mapping between the $\Sigma$-models $I$ of $D$ and the
$\Sigma^{\prime}$-models $I^{\prime}$ of $\Delta_{D}$ such that the domain of
$I$ is the same as that of $I^{\prime}$, $I^{\prime}|_{\Sigma}=I$ and
$(P^{\neg})^{I^{\prime}}$ is the (relative) complement of $P^{I}$ for each
$P\in\mbox{def}(D)$.

In the following we show that in general, FO(FD) and FO(ID) do not have the
same expressive power.

Theorem 4.4 in [Schlipf (1995)], for the well-founded semantics, states that a
relation is definable in the well-founded semantics iff it is inductively
($\Pi_{1}^{1}$) definable over the natural numbers. However, on the other
hand, Theorem 10 in [Bradfield (1996)] presents that the FO(FD) alternation
hierarchy, the hierarchy of alternating LFD and GFD expressions (ordered along
the number of alternations) in any fixpoint definitions, is strict. A
consequence is the following result.

###### Corollary 3.6

FO(ID) is strictly less expressive than FO(FD) on infinite structures.

##  4 Satisfiability of FO(FD)

The second part of this paper presents an approach to _finite model expansion_
for FO(FD), the inference task consisting of, given a theory $T$, generating a
model for the theory. As a declarative problem solving technique, model
generation for FO(FD) allow to represent e.g. temporal properties in an
application, increasing its general applicability to among others program
verification.

Finite model expansion is equivalent to checking the satisfiability of a
Boolean formula, the satisfiability problem, solved by _SAT solvers_. One
approach to check the satisfiability of FO theories, taken by many state-of-
the-art solvers, is by reducing the theory to propositional logic (a
transformation called _grounding_) and using a SAT solver afterwards.
Grounding generally consists of replacing all variables in a formula by all
possible substitutions, but intelligent techniques exist that greatly reduce
the size of such a grounding, see e.g. [Wittocx et al. (2008)].

Satisfiability checking of FO(FD) theories can be done in a similar way. First
the FO(FD) theory is grounded to a PC(FD) theory. Afterwards, the PC(FD)
theory is reduced to _difference logic_ [Nieuwenhuis and Oliveras (2005)],
propositional logic extended with linear constraints, and a difference logic
solver is used to check the satisfiability of the resulting theory. In the
domain of SMT, efficient difference logic solvers have been developed, see
e.g. [Cotton and Maler (2006)].

_Difference logic_ , denoted PC(DL), is the extension of propositional logic
with linear difference constraints of the form $x+c<y$, where $x,~{}y$ and $c$
are integer variables, of which $c$ is known. Syntactically, a linear
constraint can occur in the same positions as an atom. An interpretation of a
difference logic theory assigns truth values to atoms and integer values to
variables.

We first introduce the grounding of FO(FD) to a variable free form. Then, we
address the reductions of PC(FD) to difference logic.

Without loss of generality, we only consider theories in function free FO(FD)
for the rest of the paper (any FO(FD) theory can be transformed into a
function free theory in polynomial time).

###  4.1 Grounding FO(FD)

The reduction of an FO(FD) theory $T$ to a PC(FD) theory is defined by:

###### Definition 4.1

Given an FO(FD) theory $T$ and a finite domain $\mathfrak{D}$. To allow
grounding of quantified formulas, we introduce a new constant $c_{d}$ for each
domain element $d\in\mathfrak{D}$, which maps to $d$ in every interpretation
$I$. The grounding of $T$ according to domain $\mathfrak{D}$, denoted $G(T)$,
consists of all $G(\varphi)$ where $\varphi\in T$ and $\varphi$ is either an
FO sentence or a fixpoint definition, and $G(\varphi)$ is defined as:

$G(\varphi)=\begin{cases}\bigwedge_{d\in\mathfrak{D}}G(\psi[x/c_{d}])&\text{if
}\varphi:=\forall x\ \psi[x]\\\
\bigvee_{d\in\mathfrak{D}}G(\psi[x/c_{d}])&\text{if }\varphi:=\exists x\
\psi[x]\\\ G(\psi_{1})\wedge G(\psi_{2})&\text{if
}\varphi:=\psi_{1}\wedge\psi_{2}\\\ G(\psi_{1})\vee G(\psi_{2})&\text{if
}\varphi:=\psi_{1}\vee\psi_{2}\\\
\left\lfloor\begin{array}[]{l}G(\psi)\end{array}\right\rfloor&\text{if
}\varphi:=\left\lfloor\begin{array}[]{l}\psi\end{array}\right\rfloor\\\ \neg
G(\psi)&\text{if }\varphi:=\neg\psi\\\
\left\lceil\begin{array}[]{l}G(\psi)\end{array}\right\rceil&\text{if
}\varphi:=\left\lceil\begin{array}[]{l}\psi\end{array}\right\rceil\\\
p\leftarrow G(\psi)&\text{if }\varphi:=p\leftarrow\psi\text{ and $p$ is an
atom}\\\ \psi&\text{if }\psi\text{ is an atom}\\\ \end{cases}$

###### Proposition 4.2

An interpretation $I$ is a model of an FO(FD) theory $T$ iff it is a model of
$G(T)$.

###  4.2 Reduction to difference logic

The aim is to reduce a PC(FD) theory $G(T)$ to an _equivalent_ theory $DL(T)$
in difference logic. The reduction of FO sentences to a PC(DL) theory
coincides with their grounding, so for each FO sentence $\varphi\in T$,
$DL(T)$ contains a sentence $G(\varphi)$. The reduction of fixpoint
definitions consists of the _completion_ and _level mapping_ constraints.

####  4.2.1 Completion

The _completion_ , introduced by [Clark (1978)] for logical rules, expresses
in FO the consistency between the truth value of the head and the body of a
rule.

The completion of a propositional rule $r=p\leftarrow\varphi_{p}$, denoted
$Comp(r)$, is given by the formula $p\equiv\varphi_{p}$. The completion of a
propositional fixpoint definition $\mathcal{D}$, denoted by
$Comp(\mathcal{D})$, is $\bigcup_{r\in\mathcal{D}}Comp(r)$.

An important property is that $I\models\mathcal{D}$ implies $I\models
Comp(\mathcal{D})$. The converse is not true, $\mathcal{D}$ generally has
fewer models than $Comp(\mathcal{D})$.

###### Example 4.3

Consider the propositional fixpoint definition

$\mathcal{D}=\left\lfloor\begin{array}[]{l}p\leftarrow p\lor a\\\
\left\lceil\begin{array}[]{l}q\leftarrow q\land
p\end{array}\right\rceil\end{array}\right\rfloor$

Then $Comp(\mathcal{D})=(p\equiv p\lor a)\land(q\equiv q\land p)$.
$\mathcal{D}$ has two models:
$\\{a\mapsto\mbox{f},p\mapsto\mbox{f},q\mapsto\mbox{f}\\}$ and
$\\{a\mapsto\mbox{t},p\mapsto\mbox{t},q\mapsto\mbox{t}\\}$;
$Comp(\mathcal{D})$ has the same two models, and the additional three models:
$\\{a\mapsto\mbox{f},p\mapsto\mbox{t},q\mapsto\mbox{t}\\}$,
$\\{a\mapsto\mbox{f},p\mapsto\mbox{t},q\mapsto\mbox{f}\\}$ and
$\\{a\mapsto\mbox{t},p\mapsto\mbox{t},q\mapsto\mbox{f}\\}$.

####  4.2.2 Level mappings

To obtain equivalence of $T$ and $DL(T)$, it is necessary to ensure that only
interpretations consistent with the operator $\Gamma_{I}^{\mathcal{D}}$ are
models of $DL(T)$. We take a _level mapping_ approach to characterize the
models of the fixpoint operator. This is an extension of the technique
presented in [Janhunen et al. (2009), Niemelä (2008)], where stable model
generation of logic programs is obtained by reduction to difference logic.

######  Definition 4.4 (level mapping)

Given a fixpoint definition $\mathcal{D}$, define a function
$l_{\mathcal{D}}:\mbox{def}(\mathcal{D})\rightarrow\mathbb{N}$, with
$\mbox{def}(\mathcal{D})$ the set of all defined atoms in $\mathcal{D}$.
Function $l$ is then the _level mapping_ function and $l_{\mathcal{D}}(p)$ is
the _level_ of defined atom $p$ for fixpoint definition $\mathcal{D}$.

A level mapping function $l_{\mathcal{D}}$ is introduced for each (nested)
fixpoint definition $\mathcal{D}$ in $G(T)$. In ground form, for each fixpoint
definition $\mathcal{D}$ and for each defined atom $p$ in $\mathcal{D}$, we
introduce an integer variable, denoted $l_{\mathcal{D}}^{p}$.

The level mapping should ensure that the truth of a least fixpoint relation or
the falsity of a greatest fixpoint relation can always be _finitely justified_
in terms of locally defined atoms or open ones.

####  4.2.3 Level mapping constraints

We introduce PC(DL) formulas which, as part of $DL(T)$, act as constraints on
the relation between the levels of different defined atoms within one fixpoint
definition. Theory $DL(T)$ will be satisfiable iff such a finite justification
exists.

As mentioned earlier, all rules are considered to be in DefNF. For a given
rule $r$ in fixpoint definition $\mathcal{D}$, $h$ denotes the head and
$body(r)$ is the set of all literals occurring in the body of $r$. The sets
$BL_{def}(\mathcal{D},r)$ and $BL_{open}(\mathcal{D},r)$ denote the set of
defined, respectively open body literals(BL)

$\displaystyle BL_{def}(\mathcal{D},r)$
$\displaystyle=\\{d|d\in\mbox{def}(\mathcal{D})\cup\lnot\mbox{def}(\mathcal{D})\
\text{and}\ d\in body(r)\\}$ (1) $\displaystyle BL_{open}(\mathcal{D},r)$
$\displaystyle=\\{o|o\in\mbox{open}(\mathcal{D})\cup\lnot\mbox{open}(\mathcal{D})\
\text{and}\ o\in body(r)\\}$ (2)

We now introduce the constraints.

No justification is necessary for an atom defined in a GFD if it is true, nor
for an atom defined in an LFD which is false. Formally represented by the
constraints:

if $\mathcal{D}$ is a GFD: $\displaystyle\qquad a\supset
l_{\mathcal{D}}^{h}=0$ (3) if $\mathcal{D}$ is an LFD:
$\displaystyle\quad\lnot a\supset l_{\mathcal{D}}^{h}=0$ (4)

When an atom defined in a GFD is not true or an atom defined in an LFD is not
false, a _justification_ is necessary. A justification is a set of body
literals of a rule sufficient to derive the head in a given interpretation.
Although looping is allowed over literals defined in lower fixpoints, it has
to be possible to construct a justification which does not loop over literals
in the same level.

Deriving that the head of a rule with a disjunctive body in an LFD is true
requires only one body atom to be true. If it were a rule with a conjunctive
body, all body literals would be necessary as justification. This also holds
for the relation between their levels: in the disjunctive rule, the minimal
level of all true body literals can act as the level of the justification. In
the conjunctive case, the level is the maximum level of all body literals.

These ideas can be generalized and formalized as constraints. For clarity, the
constraints are not in PC(DL), but we introduce $min\\{\\}$ and $max\\{\\}$
notation to represent respectively the minimum and maximum of a set of levels.
Assume an interpretation $I$ to further simplify the aggregate notation. All
aggregates can be translated out easily, independent of $I$ (see further).
Also assume a fixpoint definition $\mathcal{D}$ with a locally defined atom
$h$ in a rule $r$.

  1. 1.

If $\mathcal{D}$ is an LFD and $r$ has a conjunctive body, the translation of
$r$ is:

$h\supset l_{\mathcal{D}}^{h}>max\\{l_{\mathcal{D}}^{d}|d\in
BL_{def}(\mathcal{D},r)\ \text{and}\ I(d)=\mbox{t}\\}$ (5)

  2. 2.

If $\mathcal{D}$ is an LFD and $r$ has a disjunctive body, the translation of
$r$ is:

$\begin{split}h\supset&(l_{\mathcal{D}}^{h}>min\\{l_{\mathcal{D}}^{d}|d\in
BL_{def}(\mathcal{D},r)\ \text{and}\ I(d)=\mbox{t}\\}\\\ &\lor\bigvee_{d\in
BL_{def}(\mathcal{D},r)}d\ \lor\bigvee_{o\in
BL_{open}(\mathcal{D},r)}o)\end{split}$ (6)

  3. 3.

If $\mathcal{D}$ is a GFD and $r$ has a disjunctive body, the translation of
$r$ is:

$\lnot h\supset l_{\mathcal{D}}^{h}>max\\{l_{\mathcal{D}}^{d}|d\in
BL_{def}(\mathcal{D},r)\ \text{and}\ I(d)=\mbox{f}\\}$ (7)

  4. 4.

If $\mathcal{D}$ is a GFD and $r$ has a conjunctive body, the translation of
$r$ is:

$\begin{split}\lnot
h\supset&(l_{\mathcal{D}}^{h}>min\\{l_{\mathcal{D}}^{d}|d\in
BL_{def}(\mathcal{D},r)\ \text{and}\ I(d)=\mbox{f}\\}\\\ &\lor\bigvee_{d\in
BL_{def}(\mathcal{D},r)}\lnot d\ \lor\bigvee_{o\in
BL_{open}(\mathcal{D},r)}\lnot o)\end{split}$ (8)

Similar constraints apply for the level of the head $h$ of rules defined in a
subdefinition of $\mathcal{D}$, but the inequality
$l_{\mathcal{D}}^{h}>\ldots$ is relaxed to $l_{\mathcal{D}}^{h}\geq\ldots$

###### Proposition 4.5

The truth value of a higher defined atom can only be justified by finite
looping over literals in the same definition or infinite looping over literals
in lower definitions. This is expressed by using similar constraints for
locally defined rules and for rules defined in subdefinitions, but dropping
the strict order requirement on the second, effectively allowing infinite
looping over literals defined in subdefinitions.

###### Example 4.6

In the following fixpoint definition, using only strict ordering would lead to
a contradiction, although a model exists.

$\left\lfloor\begin{array}[]{l}a\leftarrow c\\\
\left\lceil\begin{array}[]{l}c\leftarrow d\\\ d\leftarrow
c\end{array}\right\rceil\end{array}\right\rfloor$

###### Theorem 4.7

If an FO(FD) theory is transformed using the presented reduction to PC(DL) via
PC(FD), the resulting PC(DL) theory will be satisfiable iff the FO(FD) theory
is satisfiable. Any model of the PC(DL) theory can be transformed into a model
of the FO(FD) theory.

####  4.2.4 Aggregate reduction

To obtain PC(DL) constraints, the aggregates $min$ and $max$ have to be
transformed into difference constraints, which can be done in the following
fashion:

$\begin{array}[]{ll}\text{Replace
}&l_{\mathcal{D}}^{h}>max(\\{l_{\mathcal{D}}^{d}|d\in BL_{def}(\mathcal{D},r)\
\text{and}\ I(d)=\mbox{t}\\})\\\ \text{by }&\bigwedge_{d\in
BL_{def}(\mathcal{D},r)}(l_{\mathcal{D}}^{h}>l_{\mathcal{D}}^{d}\lor\lnot
d)\\\ &\\\ \text{Replace }&l_{\mathcal{D}}^{h}>min(\\{l_{\mathcal{D}}^{d}|d\in
BL_{def}(\mathcal{D},r)\ \text{and}\ I(d)=\mbox{t}\\})\\\ \text{by
}&\bigvee_{d\in
BL_{def}(\mathcal{D},r)}(l_{\mathcal{D}}^{h}>l_{\mathcal{D}}^{d}\land
d)\end{array}$

For a condition $I(d)=\mbox{f}$ instead of $I(d)=\mbox{t}$, the literal $d$ is
replaced with $\lnot d$.

####  4.2.5 Optimization: partial level mapping

Level mappings constraints are used to enforece dependencies between defined
atoms. Often, a preprocessing step (before PC(DL) reduction) allows to deduce
that certain atoms will never depend on each other. In that case, less mapping
constraints are necessary. A simple example are non-cyclic dependencies, for
which no level mapping constraints are necessary
($Comp(\mathcal{D})\models\mathcal{D}$). These dependencies can be obtained by
calculating the _strongly connected components_ [Tarjan (1972)] on the
_dependency graph_ of the fixpoint definition, a general technique used among
others in stable model generation [Syrjänen and Niemelä (2001)].

The _dependency graph_ consists of all edges $h\leadsto b$, for each rule $r$
in $\mathcal{D}$ with head $h$ and for each body literal $b$ of $r$ that is
defined in $\mathcal{D}$ or in a parent of $\mathcal{D}$. A _strongly
connected component_ of a directed graph is a maximal subset in which a path
exists between any two nodes in the set.

###### Proposition 4.8

Only defined atoms that are in a strongly connected component with
$\|nodes\|\geq 2$ or have recursion over themselves (e.g. $h\leadsto h$) need
a level mapping. Body atoms that are not in the same strongly connected
component as the head can be treated as open instead of defined atoms.

To implement this idea, the set of open body literals
$BL_{open}(\mathcal{D},r)$ is redefined: for a rule $r$, a body literal of $r$
is considered open if it is not defined, defined in an ancestor of the
definition of $r$ or if it is not in the same strongly connected component as
the head of $r$. The set $BL_{def}(\mathcal{D},r)$ contains all remaining body
literals.

####  4.2.6 Optimization: stronger constraints

The presented constraints are _weak_ : infinitely many models of the PC(DL)
reduction exist that are equivalent (modulo shared vocabulary) to one model of
the FO(FD) theory. Exact one-to-one mapping is not possible because
expressions of the form $x=c$, where $c$ is a known integer constant, cannot
be expressed in difference logic. By expressing all constraints in terms of
one integer variable, which acts as a floating ground, we can greatly reduce
the number of redundant models.

The presented constraints can be adapted to obtain such _stronger_ constraints
by enforcing that the level of the head of a rule is the minimum allowed by
its associated constraint, adapted from in [Janhunen et al. (2009), Niemelä
(2008)]. For example for a rule with a conjunctive body in a least fixpoint,
which is subject to the constraint expressed by equation 5, a second
constraint is added of the form:

$h\supset\bigvee_{d\in
BL_{def}(\mathcal{D},r)}(l_{\mathcal{D}}^{h}=l_{\mathcal{D}}^{d}+1\land d)$
(9)

##  5 Implementation and experiments

In this section, we report our first experiments, on model checking of
fairness conditions, with a prototype implementation of the reductions from
FO(FD) to difference logic. We used the $\mu$-calculus fairness expression
presented in [Liu et al. (1998)]:

$\nu X.\mu Y.[-](\langle a\rangle X)\lor Y$ (10)

It expresses that a state in the transition system is fair if on all possible
paths, an $a$-labeled edge is infinitely often taken. Translated into an
FO(FD) theory:

$\left\lceil\begin{array}[]{l}\forall x\ (P(x)\leftarrow Q(x))\\\
\left\lfloor\begin{array}[]{l}\forall x\ (Q(x)\leftarrow\forall y\
(Edge(x,y)\supset(L(y,a)\land P(y))\lor
Q(y)))\end{array}\right\rfloor\end{array}\right\rceil$

where the relations $P$ and $Q$ contain states from which infinitely often a
state labelled $a$ will be reached. The predicate $L$ is the labelling
relation, expressing that a state has a certain label. The predicate $Edge$ is
the transition relation.

The task consists of doing model expansion, where the transitions and
labellings are known, to decide which nodes are fair. Both weak and strong
constraints were tested. The experiments were done on the graph depicted in
Figure 1. The results of these experiments are as shown in Table 1, grounding
times are included. The machine used is a dual-core 2.4 GHz with 4 Gb RAM,
with Ubuntu 8.04 OS. Yices2 was used as difference logic solver.

Figure 1: A transition graph $\|nodes\|$ | weak(sec) | strong(sec)
---|---|---
503 | 0.011 | 0.004
1503 | 0.21 | 0.09
2503 | 20.51 | 14.19
|  |
Table 1: Model checking results

From these preliminary results, we conclude that fairness conditions can be
evaluated efficiently using our reduction to difference logic. Strong
constraints are significantly faster due to their fewer degrees of freedom,
which presumably allow more propagation and pruning of the search space. In
[Keinänen and Niemelä (2004)], similar results were obtained with the same
experiment.

##  6 Applications

Many applications can be found on the use of fixpoint expressions. Most of
them focus on inductive and coinductive definitions (which have nesting depth
1), used e.g. for expressing transitive closure (reachability), bisimulation
and situation calculus. One important application domain for nested fixpoint
definitions is the verification of automata. Temporal logics like CTL* allow
to express time-variant properties of automata, e.g. fairness. The
$\mu$-calculus, a superset logic of those temporal logics bound on fixpoint
expressions, can be transformed into fixpoint definitions. So any application
of model checking or model generation of temporal logics can be expressed in
FO(FD). Another application domain are so-called _parity games_ , which are
infinite games played on a graph with priority-annotated nodes. For more
information we refer to [Friedmann and Lange (2009)]. Parity games can be
expressed in fixpoint logic, the nesting increasing polynomially with the
number of priorities.

##  7 Conclusions and related work

In this paper, we have introduced fixpoint definitions, an alternative rule-
based expression of fixpoint constructs, and the logic FO(FD), which is an
extension of classical logic with fixpoint definitions. We have compared
FO(FD) and FO(ID) by providing equivalence preserving transformations of non-
monotone inductive definitions to alternating fixpoint definitions and showed
that FO(FD) is strictly more expressive than FO(ID) on infinite structures. We
have investigated the satisfiability problem for FO(FD) by developing
reductions from FO(FD) to difference logic. Hence, SMT solvers supporting
difference logic can be used for computing fixpoint models of FO(FD) theories
without any modifications. We have implemented these reductions and evaluated
the resulting solver in the computation of models of FO(FD) theories. In
general, our transformation to difference logic is exponential in the nesting
depth of a fixpoint definition, but for most practical applications they prove
compact and efficient.

$\mu\text{MALL}^{=}$, which is the logic obtained by extending MALL
(multiplicative, additive linear logic) with equality, quantification (via
$\forall$ and $\exists$) and mixed least and greatest fixpoint constructors,
was introduced in [Baelde and Miller (2007)]. It seems that
$\mu\text{MALL}^{=}$ has the same expressive power as FO(FD). However,
$\mu\text{MALL}^{=}$ is developed from a proof theory standpoint whereas
FO(FD) is developed from a model theory point of view.

Gupta et al. in [Gupta et al. (2007)] introduced coinduction, corresponding to
the greatest fixpoint constructor, into logic programming to obtain
coinductive logic programming. Discussed applications are verification, model
checking, non-monotonic reasoning, etc. However, in coinductive logic
programming, naively mixing coinduction and induction leads to contradictions
while arbitrary cyclical nesting of least and greatest fixpoint constructs is
allowed in FO(FD). Another difference is on the computational level. The main
computational task for FO(FD) is model generation in the context of a finite
domain. However, model generation in coinductive logic programming is applied
to constructs of an infinite Herbrand model based on an infinite Herbrand
universe.

Niemelä, Janhunen et al. in [Janhunen et al. (2009), Niemelä (2008)]
introduced stable model generation of general logic programs via reductions to
difference logic. They also used stable model generation to find solutions to
Boolean equation systems [Keinänen and Niemelä (2004)]. This is a related
fixpoint formalism, in which among others $\mu$-calculus can be expressed.

There are several other solvers for solving the satisfiability and validity
problems for fixpoint logics, e.g., [Friedmann and Lange (2009)]. Our
reduction is based on SMT solver technology, whereas referenced works are
based on characterizations of satisfiability through infinite (cyclic)
tableaux. Well-foundedness for unfoldings of least fixpoints is then checked
using deterministic parity automata.

## References

  * Abiteboul et al. (1995) Abiteboul, S., Hull, R., and Vianu, V. 1995\.  Foundations of Databases.  Addison-Wesley.
  * Baader et al. (2003) Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., and Patel-Schneider, P. F., Eds. 2003.  The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press.
  * Baelde and Miller (2007) Baelde, D. and Miller, D. 2007\.  Least and greatest fixed points in linear logic.  In LPAR, N. Derschowitz and A. Voronkov, Eds. LNCS, vol. 4790\. Springer, 92–106.
  * Baral (2003) Baral, C. 2003\.  Knowledge Representation, Reasoning and Declarative Problem Solving.  Cambridge University Press.
  * Barwise and Moss (1996) Barwise, J. and Moss, L. S., Eds. 1996.  Vicious Circles: On the mathematics of Non-Wellfounded Phenomena.  University of Chicago Press.
  * Bradfield (1996) Bradfield, J. C. 1996\.  The modal mu-calculus alternation hierarchy is strict.  In CONCUR, U. Montanari and V. Sassone, Eds. LNCS, vol. 1119\. Springer, 233–246.
  * Clark (1978) Clark, K. L. 1978\.  Negation as failure.  In Logic and Data Bases. Plenum Press, 293–322.
  * Cotton and Maler (2006) Cotton, S. and Maler, O. 2006\.  Fast and flexible difference constraint propagation for DPLL(T).  In SAT, A. Biere and C. P. Gomes, Eds. LNCS, vol. 4121. Springer, 170–183.
  * Denecker (2000) Denecker, M. 2000\.  Extending classical logic with inductive definitions.  In CL, J. W. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, Eds. LNCS, vol. 1861. Springer, 703–717.
  * Denecker and Ternovska (2008) Denecker, M. and Ternovska, E. 2008\.  A logic of nonmonotone inductive definitions.  ACM Transactions on Computational Logic (TOCL) 9, 2, Article 14.
  * Friedmann and Lange (2009) Friedmann, O. and Lange, M. 2009\.  Solving parity games in practice.  In ATVA, Z. Liu and A. P. Ravn, Eds. LNCS, vol. 5799. Springer, 182–196.
  * Gupta et al. (2007) Gupta, G., Bansal, A., Min, R., Simon, L., and Mallya, A. 2007\.  Coinductive logic programming and its applications.  In ICLP, V. Dahl and I. Niemelä, Eds. LNCS, vol. 4670\. Springer, 27–44.
  * Janhunen et al. (2009) Janhunen, T., Niemelä, I., and Sevalnev, M. 2009\.  Computing stable models via reductions to difference logic.  In LPNMR, E. Erdem, F. Lin, and T. Schaub, Eds. LNCS, vol. 5753. Springer, 142–154.
  * Kakas et al. (1992) Kakas, A. C., Kowalski, R. A., and Toni, F. 1992\.  Abductive logic programming.  J. Log. Comput. 2, 6, 719–770.
  * Keinänen and Niemelä (2004) Keinänen, M. and Niemelä, I. 2004\.  Solving alternating boolean equation systems in answer set programming.  In INAP/WLP, D. Seipel, M. Hanus, U. Geske, and O. Bartenstein, Eds. LNCS, vol. 3392. Springer, 134–148.
  * Liu et al. (1998) Liu, X., Ramakrishnan, C. R., and Smolka, S. A. 1998\.  Fully local and efficient evaluation of alternating fixed points (extended abstract).  In TACAS, B. Steffen, Ed. LNCS, vol. 1384. Springer, 5–19.
  * McCarthy (1986) McCarthy, J. 1986\.  Applications of circumscription to formalizing common-sense knowledge.  Artificial Intelligence 28, 1, 89–116.
  * Niemelä (2008) Niemelä, I. 2008\.  Stable models and difference logic.  Ann. Math. Artif. Intell. 53, 1-4, 313–329.
  * Nieuwenhuis and Oliveras (2005) Nieuwenhuis, R. and Oliveras, A. 2005\.  DPLL(T) with exhaustive theory propagation and its application to difference logic.  In CAV, K. Etessami and S. K. Rajamani, Eds. LNCS, vol. 3576\. Springer, 321–334.
  * Park (1969) Park, D. 1969\.  Fixpoint induction and proofs of program properties.  Machine Intelligence 5, 59–78.
  * Schlipf (1995) Schlipf, J. S. 1995\.  The expressive powers of the logic programming semantics.  J. Comput. Syst. Sci. 51, 1, 64–86.
  * Syrjänen and Niemelä (2001) Syrjänen, T. and Niemelä, I. 2001\.  The smodels system.  In LPNMR, T. Eiter, W. Faber, and M. Truszczyński, Eds. LNCS, vol. 2173. Springer, 434–438.
  * Tarjan (1972) Tarjan, R. E. 1972\.  Depth-first search and linear graph algorithms.  SIAM Journal on Computing 1, 2, 146–160.
  * Tseitin (1968) Tseitin, G. S. 1968\.  On the complexity of derivation in propositional calculus.  In Studies in Constructive Mathematics and Mathematical Logic II, A. O. Slisenko, Ed. Consultants Bureau, N.Y., 115–125.
  * Vennekens and Denecker (2009) Vennekens, J. and Denecker, M. 2009\.  FO(ID) as an extension of DL with rules.  In ESWC, L. Aroyo, P. Traverso, F. Ciravegna, P. Cimiano, T. Heath, E. Hyvönen, R. Mizoguchi, E. Oren, M. Sabou, and E. P. B. Simperl, Eds. LNCS, vol. 5554. Springer, 384–398.
  * Wittocx et al. (2008) Wittocx, J., Mariën, M., and Denecker, M. 2008\.  Grounding with bounds.  In AAAI, D. Fox and C. P. Gomes, Eds. AAAI Press, 572–577.