11institutetext: Vrije Universiteit Amsterdam, The Netherlands
22institutetext: Department of Mathematical Sciences, Stellenbosch University,
South Africa 33institutetext: Department of Mathematics and Applied
Mathematics, University of Johannesburg, South Africa

# Non-distributive description logic††thanks: This paper is partially funded
by the EU MSCA (grant No. 101007627). The first author is funded by the
National Research Foundation of South Africa (grant No. 140841). The third and
fourth authors are partially funded by the NWO grant KIVI.2019.001.

Ineke van der Berg 1122 0000-0003-2220-1383 Andrea De Domenico 11
0000-0002-8973-7011 Giuseppe Greco 11 0000-0002-4845-3821 Krishna B. Manoorkar
11 0000-0003-3664-7757 Alessandra Palmigiano 1133 0000-0001-9656-7527 Mattia
Panettiere 11 0000-0002-9218-5449

###### Abstract

We define LE-$\mathcal{ALC}$, a generalization of the description logic
$\mathcal{ALC}$ based on the propositional logic of general (i.e. not
necessarily distributive) lattices, and semantically interpreted on relational
structures based on formal contexts from Formal Concept Analysis (FCA). The
description logic LE-$\mathcal{ALC}$ allows us to formally describe databases
with objects, features, and formal concepts, represented according to FCA as
Galois-stable sets of objects and features. We describe ABoxes and TBoxes in
LE-$\mathcal{ALC}$, provide a tableaux algorithm for checking the consistency
of LE-$\mathcal{ALC}$ knowledge bases with acyclic TBoxes, and show its
termination, soundness and completeness. Interestingly, consistency checking
for LE-$\mathcal{ALC}$ is in PTIME for acyclic and completely unravelled
TBoxes, while the analogous problem in the classical $\mathcal{ALC}$ setting
is PSPACE-complete.
Keywords: Description logic, Tableaux algorithm, Formal Concept Analysis, LE-
logics.

##  1 Introduction

Description Logic (DL) [2] is a class of logical formalisms, typically based
on classical first-order logic, and widely used in Knowledge Representation
and Reasoning to describe and reason about relevant concepts in a given
application domain and their relationships. Since certain laws of classical
logic fail in certain application domains, in recent years, there has been a
growing interest in developing versions of description logics on weaker (non-
classical) propositional bases. For instance, in [20], an intuitionistic
version of the DL $\mathcal{ALC}$ has been introduced for resolving some
inconsistencies arising from the classical law of excluded middle when
applying $\mathcal{ALC}$ to legal domains. In [6, 19], many-valued (fuzzy)
description logics have been introduced to account for uncertainty and
imprecision in processing information in the Semantic Web, and recently,
frameworks of non-monotonic description logics have been introduced [14, 18,
15].

One domain of application in which there is no consensus as to how classical
logic should be applied is Formal Concept Analysis (FCA). In this setting,
formal concepts arise from formal contexts $\mathbb{P}=(A,X,I)$, where $A$ and
$X$ are sets (of objects and features respectively), and $I\subseteq A\times
X$. Specifically, formal concepts are represented as Galois-stable tuples
$(B,Y)$ such that $B\subseteq A$ and $Y\subseteq X$ and $B=\\{a\in
A\mid\forall y(y\in Y\Rightarrow aIy)\\}$ and $Y=\\{x\in X\mid\forall b(b\in
B\Rightarrow bIx)\\}$. The formal concepts arising from a formal context are
naturally endowed with a partial order (the sub-concept/super-concept
relation) as follows: $(B_{1},Y_{1})\leq(B_{2},Y_{2})$ iff $B_{1}\subseteq
B_{2}$ iff $Y_{2}\subseteq Y_{1}$. This partial order is a complete lattice,
which is in general non-distributive. The failure of distributivity in the
lattice of formal concepts introduces a tension between classical logic and
the natural logic of formal concepts in FCA. This failure motivated the
introduction of lattice-based propositional (modal) logics as the (epistemic)
logics of formal concepts [10, 9]. Complete relational semantics of these
logics is given by enriched formal contexts (cf. Section 2.2), relational
structures $\mathbb{F}=(\mathbb{P},\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$
based on formal contexts.
In this paper, we introduce LE-$\mathcal{ALC}$, a lattice-based version of
$\mathcal{ALC}$ which stands in the same relation to the lattice-based modal
logic of formal concepts [12] as classical $\mathcal{ALC}$ stands in relation
to classical modal logic: the language and semantics of LE-$\mathcal{ALC}$ is
based on enriched formal contexts and their associated modal algebras. Thus,
just like the language of $\mathcal{ALC}$ can be seen as a hybrid modal logic
language interpreted on Kripke frames, the language of LE-$\mathcal{ALC}$ can
be regarded as a hybrid modal logic language interpreted on enriched formal
contexts.

FCA and DL are different and well known approaches in the formal
representation of concepts (or categories). They have been used together for
several purposes [1, 4, 17]. Thus, providing a DL framework which allows us to
describe formal contexts (possibly enriched, e.g. with additional relations on
them) would be useful in relating these frameworks both at a theoretical and
at a practical level. Proposals to connect FCA and DL have been made, in which
concept lattices serve as models for DL concepts. Shilov and Han [21]
interpret the positive fragment of $\mathcal{ALC}$ concepts over concept
lattices and show that this interpretation is compatible with standard Kripke
models for $\mathcal{ALC}$. A similar approach is used by Wrum [22] in which
complete semantics for the (full) Lambek calculus is defined on concept
lattices. The approach of the present paper for defining and interpreting non-
distributive description logic and modal logic in relation with concept
lattices with operators differs from the approaches mentioned above in that it
is based on duality-theoretic insights (cf. [10]). This allows us not only to
show that the DL framework introduced in the present paper is consistent with
the standard DL setting and its interpretation on Kripke models, but also to
show that several properties of these logics and the meaning of their formulas
can also be “lifted” from the classical (distributive) to non-distributive
settings (cf. [7, 12, 8] for extended discussions).

The main technical contribution of this paper is a tableaux algorithm for
checking the consistency of LE-$\mathcal{ALC}$ ABoxes. We show that the
algorithm is terminating, sound and complete. Interestingly, this algorithm
has a polynomial time complexity, compared to the complexity of the
consistency checking of classical $\mathcal{ALC}$ ABoxes which is PSPACE-
complete. This means that the consistency checking problem for completely
unravelled TBoxes (cf. Subsection 2.1) for our logic is in PTIME. The
algorithm also constructs a model for the given ABox which is polynomial in
size. Thus, it also implies that the corresponding hybrid modal logic has the
finite model property.
Structure of the paper. In Section 2, we give the necessary preliminaries on
the DL $\mathcal{ALC}$, lattice-based modal logics and their relational
semantics. In Section 3, we introduce the syntax and the semantics of
LE-$\mathcal{ALC}$. In Section 4, we introduce a tableaux algorithm for
checking the consistency of LE-$\mathcal{ALC}$ ABoxes and show that it is
terminating, sound and complete. In Section 5, we conclude and discuss some
future research directions.

##  2 Preliminaries

###  2.1 Description logic $\mathcal{ALC}$

Let $\mathcal{C}$ and $\mathcal{R}$ be disjoint sets of primitive or atomic
concept names and role names. The set of concept descriptions over
$\mathcal{C}$ and $\mathcal{R}$ are defined recursively as follows.

$C\colonequals A\mid\top\mid\bot\mid C\wedge C\mid C\vee C\mid\neg
C\mid\exists r.C\mid\forall r.C$

where $A\in\mathcal{C}$ and $r\in\mathcal{R}$. An interpretation is a tuple
$\mathrm{I}=(\Delta^{\mathrm{I}},\cdot^{\mathrm{I}})$ s.t.
$\Delta^{\mathrm{I}}$ is a non-empty set and $\cdot^{\mathrm{I}}$ maps every
concept $A\in\mathcal{C}$ to a set
$A^{\mathrm{I}}\subseteq\Delta^{\mathrm{I}}$, and every role name
$r\in\mathcal{R}$ to a relation
$r^{\mathrm{I}}\subseteq\Delta^{\mathrm{I}}\times\Delta^{\mathrm{I}}$. This
mapping extends to all concept descriptions as follows:

$\top^{\mathrm{I}}$ | = | $\Delta^{\mathrm{I}}$ |  | $\bot^{\mathrm{I}}$ | = | $\varnothing$
---|---|---|---|---|---|---
$(C\wedge D)^{\mathrm{I}}$ | = | $C^{\mathrm{I}}\cap D^{\mathrm{I}}$ |  | $(C\vee D)^{\mathrm{I}}$ | = | $C^{\mathrm{I}}\cup D^{\mathrm{I}}$
$(\exists r.C)^{\mathrm{I}}$ | = | $\\{d\in\Delta^{\mathrm{I}}\mid\exists e((d,e)\in r^{\mathrm{I}}\ \&\ e\in C^{\mathrm{I}}\\}$ |  | $(\neg C)^{\mathrm{I}}$ | = | $\Delta^{\mathrm{I}}\setminus C^{\mathrm{I}}$
$(\forall r.C)^{\mathrm{I}}$ | = | $\\{d\in\Delta^{\mathrm{I}}\mid\forall e((d,e)\in r^{\mathrm{I}}\Rightarrow e\in C^{\mathrm{I}}\\}$ |  |  |  |

Let $\mathcal{S}$ be a set of individual names disjoint from $\mathcal{C}$ and
$\mathcal{R}$, such that for every $a$ in $\mathcal{S}$,
$a^{\mathrm{I}}\in\Delta^{\mathrm{I}}$. For any $a,b\in\mathcal{S}$, any
$C\in\mathcal{C}$ and $r\in\mathcal{R}$, an expression of the form $a:C$
(resp. $(a,b):r$) is an $\mathcal{ALC}$ concept assertion (resp. role
assertion). A finite set of $\mathcal{ALC}$ concept and role assertions is an
$\mathcal{ALC}$ ABox. An assertion $a:C$ (resp. $(a,b):r$) is satisfied in an
interpretation ${\mathrm{I}}$ if $a^{\mathrm{I}}\in C^{\mathrm{I}}$ (resp. if
$(a^{\mathrm{I}},b^{\mathrm{I}})\in r^{\mathrm{I}}$). An $\mathcal{ALC}$ TBox
is a finite set of expressions of the form $C_{1}\equiv C_{2}$. An
interpretation ${\mathrm{I}}$ satisfies $C_{1}\equiv C_{2}$ iff
$C_{1}^{\mathrm{I}}=C_{2}^{\mathrm{I}}$. An $\mathcal{ALC}$ knowledge base is
a tuple $(\mathcal{A},\mathcal{T})$, where $\mathcal{A}$ is an $\mathcal{ALC}$
ABox, and $\mathcal{T}$ is an $\mathcal{ALC}$ TBox. An interpretation
${\mathrm{I}}$ is a model for a knowledge base $(\mathcal{A},\mathcal{T})$ iff
it satisfies all members of $\mathcal{A}$ and $\mathcal{T}$. A knowledge base
$(\mathcal{A},\mathcal{T})$ is consistent if there is a model for it. An ABox
$\mathcal{A}$ (resp. TBox $\mathcal{T}$) is consistent if the knowledge base
$(\mathcal{A},\varnothing)$ (resp. $(\varnothing,\mathcal{T})$) is consistent.

An $\mathcal{ALC}$ concept deﬁnition in $T$ is an expression of the form
$A\equiv C$ where $A$ is an atomic concept. We say that $A$ directly uses $B$
if there is a concept deﬁnition $A\equiv C$ in $\mathcal{T}$ such that $B$
occurs in $C$. We say that $A$ uses $B$ if $A$ directly uses $B$, or if there
is a concept name $B^{\prime}$ such that $A$ uses $B^{\prime}$ and
$B^{\prime}$ directly uses $B$. A finite set $\mathcal{T}$ of concept
definitions is an acyclic TBox if

1\. there is no concept in $\mathcal{T}$ that uses itself,

2\. no concept occurs more than once on the left-hand side of a concept
deﬁnition in $\mathcal{T}$.

A finite set $\mathcal{T}$ of concept definitions is a completely unravelled
TBox if it is acyclic and no atomic concept occurring on the left-hand side of
a concept definition in $\mathcal{T}$ is also present in some other concept
definition on the right-side.

Checking the consistency of a knowledge base is a key problem in description
logics, usually solved via tableaux algorithms. In the $\mathcal{ALC}$ case,
checking the consistency of any knowledge base is EXPTIME-complete while
checking the consistency of a knowledge base with acyclic TBoxes is PSPACE-
complete [2].

###  2.2 Basic normal non-distributive modal logic and its semantics

The logic introduced in this section is part of a family of lattice-based
logics, sometimes referred to as LE-logics (cf. [11]), which have been studied
in the context of a research program on the logical foundations of
categorization theory [10, 9, 8, 12]. Let $\mathsf{Prop}$ be a (countable) set
of atomic propositions. The language $\mathcal{L}$ is defined as follows:

$\varphi\colonequals\bot\mid\top\mid
p\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\Box\varphi\mid\Diamond\varphi,$

where $p\in\mathsf{Prop}$, and $\Box\in\mathcal{G}$ and
$\Diamond\in\mathcal{F}$ for finite sets $\mathcal{F}$ and $\mathcal{G}$ of
unary $\Diamond$-type (resp. $\Box$-type) modal operators. The basic, or
minimal normal $\mathcal{L}$-logic is a set $\mathbf{L}$ of sequents
$\varphi\vdash\psi$, with $\varphi,\psi\in\mathcal{L}$, containing the
following axioms for every $\Box\in\mathcal{F}$ and $\Diamond\in\mathcal{G}$:

$p\vdash p$ |  | $\bot\vdash p$ |  | $p\vdash p\vee q$ |  | $p\wedge q\vdash p$ |  | $\top\vdash\Box\top$ |  | $\Box p\wedge\Box q\vdash\Box(p\wedge q)$
---|---|---|---|---|---|---|---|---|---|---
|  | $p\vdash\top$ |  | $q\vdash p\vee q$ |  | $p\wedge q\vdash q$ |  | $\Diamond\bot\vdash\bot$ |  | $\Diamond(p\vee q)\vdash\Diamond p\vee\Diamond q$

and closed under the following inference rules:

$\displaystyle\frac{\varphi\vdash\chi\quad\chi\vdash\psi}{\varphi\vdash\psi}\
\
\frac{\varphi\vdash\psi}{\varphi\left(\chi/p\right)\vdash\psi\left(\chi/p\right)}\
\ \frac{\chi\vdash\varphi\quad\chi\vdash\psi}{\chi\vdash\varphi\wedge\psi}\ \
\frac{\varphi\vdash\chi\quad\psi\vdash\chi}{\varphi\vee\psi\vdash\chi}\ \
\frac{\varphi\vdash\psi}{\Box\varphi\vdash\Box\psi}\ \
\frac{\varphi\vdash\psi}{\Diamond\varphi\vdash\Diamond\psi}$

Note that unlike in classical modal logic, we cannot assume that $\Box$ and
$\Diamond$ are inter-definable in LE-logics, hence we take all connectives as
primitive.

Relational semantics. The following notation, notions and facts are from [8,
12]. For any binary relation $T\subseteq U\times V$, and any
$U^{\prime}\subseteq U$ and $V^{\prime}\subseteq V$, we let $T^{c}$ denote the
set-theoretic complement of $T$ in $U\times V$, and

$T^{(1)}[U^{\prime}]\colonequals\\{v\mid\forall u(u\in U^{\prime}\Rightarrow
uTv)\\}\quad\quad T^{(0)}[V^{\prime}]\colonequals\\{u\mid\forall v(v\in
V^{\prime}\Rightarrow uTv)\\}.$ (1)

In what follows, we fix two sets $A$ and $X$, and use $a,b$ (resp. $x,y$) for
elements of $A$ (resp. $X$), and $B,C,A_{j}$ (resp. $Y,W,X_{j}$) for subsets
of $A$ (resp. of $X$).

A polarity or formal context (cf. [13]) is a tuple $\mathbb{P}=(A,X,I)$, where
$A$ and $X$ are sets, and $I\subseteq A\times X$ is a binary relation.
Intuitively, formal contexts can be understood as abstract representations of
databases [13], so that $A$ and $X$ represent collections of objects and
features, and for any object $a$ and feature $x$, the tuple $(a,x)$ belongs to
$I$ exactly when object $a$ has feature $x$.

As is well known, for every formal context $\mathbb{P}=(A,X,I)$, the pair of
maps

$(\cdot)^{\uparrow}:\mathcal{P}(A)\to\mathcal{P}(X)\quad\mbox{ and
}\quad(\cdot)^{\downarrow}:\mathcal{P}(X)\to\mathcal{P}(A),$

defined by the assignments $B^{\uparrow}\colonequals I^{(1)}[B]$ and
$Y^{\downarrow}\colonequals I^{(0)}[Y]$, form a Galois connection, and hence
induce the closure operators $(\cdot)^{\uparrow\downarrow}$ and
$(\cdot)^{\downarrow\uparrow}$ on $\mathcal{P}(A)$ and on $\mathcal{P}(X)$
respectively. The fixed points of $(\cdot)^{\uparrow\downarrow}$ and
$(\cdot)^{\downarrow\uparrow}$ are the Galois-stable sets. A formal concept of
a polarity $\mathbb{P}=(A,X,I)$ is a tuple $c=(B,Y)$ such that $B\subseteq A$
and $Y\subseteq X$, and $B=Y^{\downarrow}$ and $Y=B^{\uparrow}$. The subset
$B$ (resp. $Y$) is the extension (resp. the intension) of $c$ and is denoted
by $[\\![{c}]\\!]$ (resp. $(\\![{c}]\\!)$). It is well known (cf. [13]) that
the sets $B$ and $Y$ are Galois-stable, and that the set of formal concepts of
a polarity $\mathbb{P}$, with the order defined by

$c_{1}\leq
c_{2}\quad\text{iff}\quad[\\![{c_{1}}]\\!]\subseteq[\\![{c_{2}}]\\!]\quad\text{iff}\quad(\\![{c_{2}}]\\!)\subseteq(\\![{c_{1}}]\\!)$,

forms a complete lattice $\mathbb{P}^{+}$, namely the concept lattice of
$\mathbb{P}$.

For the language $\mathcal{L}$ defined above, an enriched formal
$\mathcal{L}$-context is a tuple
$\mathbb{F}=(\mathbb{P},\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$, where
$\mathcal{R}_{\Box}=\\{R_{\Box}\subseteq A\times X\mid\Box\in\mathcal{G}\\}$
and $\mathcal{R}_{\Diamond}=\\{R_{\Diamond}\subseteq X\times
A\mid\Diamond\in\mathcal{F}\\}$ are sets of $I$-compatible relations, that is,
for all $\Box\in\mathcal{G}$, $\Diamond\in\mathcal{F}$, $a\in A$, and $x\in
X$, the sets $R_{\Box}^{(0)}[x]$, $R_{\Box}^{(1)}[a]$,
$R_{\Diamond}^{(0)}[a]$, $R_{\Diamond}^{(1)}[x]$ are Galois-stable in
$\mathbb{P}$. For each $\Box\in\mathcal{G}$ and $\Diamond\in\mathcal{F}$,
their associated relations $R_{\Box}$ and $R_{\Diamond}$ provide their
corresponding semantic interpretations as operations $[R_{\Box}]$ and $\langle
R_{\Diamond}\rangle$ on the concept lattice $\mathbb{P}^{+}$ defined as
follows: For any $c\in\mathbb{P}^{+}$,
$[R_{\Box}]c=(R_{\Box}^{(0)}[(\\![{c}]\\!)],I^{(1)}[R_{\Box}^{(0)}[(\\![{c}]\\!)]])\quad\text{and}\quad\langle
R_{\Diamond}\rangle
c=(I^{(0)}[R_{\Diamond}^{(0)}[[\\![{c}]\\!]]],R_{\Diamond}^{(0)}[[\\![{c}]\\!]]).$

We refer to the algebra
$\mathbb{F}^{+}=(\mathbb{P}^{+},\\{[R_{\Box}]\\}_{\Box\in\mathcal{G}},\\{\langle
R_{\Diamond}\rangle\\}_{\Diamond\in\mathcal{F}})$ as the complex algebra of
$\mathbb{F}$.

A valuation on such an $\mathbb{F}$ is a map
$V\colon\mathsf{Prop}\to\mathbb{P}^{+}$. For each $p\in\mathsf{Prop}$, we let
$[\\![{p}]\\!]\colonequals[\\![{V(p)}]\\!]$ (resp.
$(\\![{p}]\\!)\colonequals(\\![{V(p)}]\\!)$) denote the extension (resp.
intension) of the interpretation of $p$ under $V$.

A model is a tuple $\mathbb{M}=(\mathbb{F},V)$ where
$\mathbb{F}=(\mathbb{P},\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$ is an
enriched formal context and $V$ is a valuation on $\mathbb{F}$. For every
$\varphi\in\mathcal{L}$, we let
$[\\![{\varphi}]\\!]_{\mathbb{M}}\colonequals[\\![{V(\varphi)}]\\!]$ (resp.
$(\\![{\varphi}]\\!)_{\mathbb{M}}\colonequals(\\![{V(\varphi)}]\\!)$) denote
the extension (resp. intension) of the interpretation of $\varphi$ under the
homomorphic extension of $V$. The following ‘forcing’ relations can be
recursively defined as follows:

$\mathbb{M},a\Vdash p$ |  iff $a\in[\\![{p}]\\!]_{\mathbb{M}}$ | $\mathbb{M},x\succ p$ |  iff $x\in(\\![{p}]\\!)_{\mathbb{M}}$
---|---|---|---
$\mathbb{M},a\Vdash\top$ | always | $\mathbb{M},x\succ\top$ |  iff $aIx$ for all $a\in A$
$\mathbb{M},x\succ\bot$ | always | $\mathbb{M},a\Vdash\bot$ |  iff $aIx$ for all $x\in X$
$\mathbb{M},a\Vdash\varphi\wedge\psi$ |  iff $\mathbb{M},a\Vdash\varphi$ and $\mathbb{M},a\Vdash\psi$ | $\mathbb{M},x\succ\varphi\wedge\psi$ |  iff $(\forall a\in A)$ $(\mathbb{M},a\Vdash\varphi\wedge\psi\Rightarrow aIx)$
$\mathbb{M},x\succ\varphi\vee\psi$ |  iff $\mathbb{M},x\succ\varphi$ and $\mathbb{M},x\succ\psi$ | $\mathbb{M},a\Vdash\varphi\vee\psi$ |  iff $(\forall x\in X)$ $(\mathbb{M},x\succ\varphi\vee\psi\Rightarrow aIx)$.

As to the interpretation of modal formulas, for every $\Box\in\mathcal{G}$ and
$\Diamond\in\mathcal{F}$:

$\mathbb{M},a\Vdash\Box\varphi$ |  iff $(\forall x\in X)(\mathbb{M},x\succ\varphi\Rightarrow aR_{\Box}x)$ |  | $\mathbb{M},x\succ\Box\varphi$ |  iff $(\forall a\in A)(\mathbb{M},a\Vdash\Box\varphi\Rightarrow aIx)$
---|---|---|---|---
$\mathbb{M},x\succ\Diamond\varphi$ |  iff for all $a\in A$, if $\mathbb{M},a\Vdash\varphi$ then $xR_{\Diamond}a$ |  | $\mathbb{M},a\Vdash\Diamond\varphi$ |  iff $(\forall x\in X)(\mathbb{M},x\succ\Diamond\varphi\Rightarrow aIx)$

The definition above ensures that, for any $\mathcal{L}$-formula $\varphi$,

$\mathbb{M},a\Vdash\varphi$ iff $a\in[\\![{\varphi}]\\!]_{\mathbb{M}}$, and
$\mathbb{M},x\succ\varphi$ iff $x\in(\\![{\varphi}]\\!)_{\mathbb{M}}$.

$\mathbb{M}\models\varphi\vdash\psi$ iff
$[\\![{\varphi}]\\!]_{\mathbb{M}}\subseteq[\\![{\psi}]\\!]_{\mathbb{M}}$ iff
$(\\![{\psi}]\\!)_{\mathbb{M}}\subseteq(\\![{\varphi}]\\!)_{\mathbb{M}}$.

The interpretation of the propositional connectives $\vee$ and $\wedge$ in the
framework described above reproduces the standard notion of join and the meet
of formal concepts used in FCA. The interpretation of the operators $\Box$ and
$\Diamond$ is motivated by algebraic properties and duality theory for modal
operators on lattices (cf. [12, Section 3] for an expanded discussion). In [8,
Proposition 3.7], it is shown that the semantics of LE-logics is compatible
with Kripke semantics for classical modal logic, and thus, LE-logics are
indeed generalizations of classical modal logic. This interpretation is
further justified in [8, Section 4] by noticing that, under the
interpretations of the relation $I$ as $aIx$ iff “object $a$ has feature $x$”
and $R=R_{\Box}=R^{-1}_{\Diamond}$ as $aRx$ iff “there is evidence that object
$a$ has feature $x$”, then, for any concept $c$, the extents of concepts $\Box
c$ and $\Diamond c$ can be interpreted as “the set of objects which certainly
belong to $c$” (upper approximation), and “the set of objects which possibly
belong to $c$” (lower approximation) respectively. Thus, the interpretations
of $\Box$ and $\Diamond$ have similar meaning in the LE-logic as in the
classical modal logic. A similar justification regarding similarity of
epistemic interpretations of $\Box$ in classical and lattice-based modal
logics is discussed in [9]. This transfer of meaning of modal axioms from
classical modal logic to LE-logics has been investigated as a general
phenomenon in [7, Section 4.3], [12].

##  3 LE Description logic

In this section, we introduce the non-classical DL LE-$\mathcal{ALC}$, so that
LE-$\mathcal{ALC}$ will be in same relation with LE-logic as $\mathcal{ALC}$
is with classical modal logic. This similarity extends to the models we will
introduce for LE-$\mathcal{ALC}$: in the same way as Kripke models of
classical modal logic are used as models of $\mathcal{ALC}$, enriched formal
contexts, which provide complete semantics for LE-logic, will serve as models
of LE-$\mathcal{ALC}$. In this specific respect, LE-$\mathcal{ALC}$ can be
seen as a generalization of the positive fragment (i.e. the fragment with no
negations in concepts) of $\mathcal{ALC}$ in which we do not assume
distributivity laws to hold for concepts. Consequently, the language of
LE-$\mathcal{ALC}$ contains individuals of two types, usually interpreted as
the objects and features of the given database or categorization. Let
$\mathsf{OBJ}$ and $\mathsf{FEAT}$ be disjoint sets of individual names for
objects and features.

The set $\mathcal{R}$ of the role names for LE-$\mathcal{ALC}$ is the union of
three disjoint sets of relations: (1) the single relation
$I\subseteq\mathsf{OBJ}\times\mathsf{FEAT}$ (2) a set $\mathcal{R}_{\Box}$
such that for any $R_{\Box}\in\mathcal{R}_{\Box}$m,
$R_{\Box}\subseteq\mathsf{OBJ}\times\mathsf{FEAT}$; (3) a set
$\mathcal{R}_{\Diamond}$ such that for any
$R_{\Diamond}\in\mathcal{R}_{\Box}$m,
$R_{\Diamond}\subseteq\mathsf{FEAT}\times\mathsf{OBJ}$. While $I$ is intended
to be interpreted as the incidence relation of formal concepts, and encodes
information on which objects have which features, the relations in
$\mathcal{R}_{\Box}$ and $\mathcal{R}_{\Diamond}$ encode additional
relationships between objects and features (cf. [8] for an extended
discussion).

For any set $\mathcal{C}$ of atomic concept names, the language of
LE-$\mathcal{ALC}$ concepts is:

$C\colonequals D\ |\ C_{1}\wedge C_{2}\ |\ C_{1}\vee C_{2}\ |\ \langle
R_{\Diamond}\rangle C\ |\ [R_{\Box}]C$

where $D\in\mathcal{C}$, $R_{\Box}\in\mathcal{R}_{\Box}$ and
$R_{\Diamond}\in\mathcal{R}_{\Diamond}$. This language matches the language of
LE-logic, and has an analogous intended interpretation on the complex algebras
of enriched formal contexts (cf. Section 2.2). As usual, $\vee$ and $\wedge$
are to be interpreted as the smallest common superconcept and the greatest
common subconcept as in FCA. The constants $\top$ and $\bot$ are to be
interpreted as the largest and the smallest concept, respectively. We do not
include $\neg C$ as a valid concept in our language, since there is no
canonical and natural way to interpret negations in non-distributive settings.

The concepts $\langle R_{\Diamond}\rangle C$ and $[R_{\Box}]C$ in
LE-$\mathcal{ALC}$ are intended to be interpreted as the operations $\langle
R_{\Diamond}\rangle$ and $[R_{\Box}]$ defined by the interpretations of their
corresponding role names in enriched formal contexts, analogously to the way
in which $\exists r$ and $\forall r$ in $\mathcal{ALC}$ are interpreted on
Kripke frames. We do not use the symbols $\forall r$ and $\exists r$ in the
context of LE-$\mathcal{ALC}$ because, as discussed in Section 2.2, the
semantic clauses of modal operators in LE-logic use universal quantifiers, and
hence using the same notation verbatim would be ambiguous or misleading.

TBox assertions in LE-$\mathcal{ALC}$ are of the shape $C_{1}\equiv C_{2}$,
where $C_{1}$ and $C_{2}$ are concepts defined as above.111As is standard in
DL (cf. [2] for more details), general concept inclusion of the form
$C_{1}\sqsubseteq C_{2}$ can be rewritten as concept definition $C_{1}\equiv
C_{2}\wedge C_{3}$, where $C_{3}$ is a new atomic concept name. The ABox
assertions are of the form:

$aR_{\Box}x,\quad xR_{\Diamond}a,\quad aIx,\quad a:C,\quad
x::C,\quad\neg\alpha,$

where $\alpha$ is any of the first five ABox terms, and $C$ is any concept in
the language of LE-$\mathcal{ALC}$. We refer to the terms of first three types
as relational terms. The interpretations of the terms $a:C$ and $x::C$ are:
“object $a$ is a member of concept $C$”, and “feature $x$ is in the
description of concept $C$”, respectively.

An interpretation for LE-$\mathcal{ALC}$ is a tuple
$\mathrm{I}=(\mathbb{F},\cdot^{\mathrm{I}})$, where
$\mathbb{F}=(\mathbb{P},\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$ is an
enriched formal context, and $\cdot^{\mathrm{I}}$ maps:

1\. individual names $a\in\mathsf{OBJ}$ (resp. $x\in\mathsf{FEAT}$), to some
$a^{\mathrm{I}}\in A$ (resp. $x^{\mathrm{I}}\in X$);

2\. relation names $I$, $R_{\Box}$ and $R_{\Diamond}$ to relations
$I^{\mathrm{I}}$, $R_{\Box}^{\mathrm{I}}$ and $R_{\Diamond}^{\mathrm{I}}$ in
$\mathbb{F}$;

3\. any atomic concept name $D$ to $D^{\mathrm{I}}\in\mathbb{F}^{+}$, and
other concepts as follows:

$(C_{1}\wedge C_{2})^{\mathrm{I}}=C_{1}^{\mathrm{I}}\wedge C_{2}^{\mathrm{I}}$ | $(C_{1}\vee C_{2})^{\mathrm{I}}=C_{1}^{\mathrm{I}}\vee C_{2}^{\mathrm{I}}$
---|---
$([R_{\Box}]C)^{\mathrm{I}}=[R_{\Box}^{\mathrm{I}}]C^{\mathrm{I}}$ | $(\langle R_{\Diamond}\rangle C)^{\mathrm{I}}=\langle R_{\Diamond}^{\mathrm{I}}\rangle C^{\mathrm{I}}$

where the operators $[R^{\mathrm{I}}_{\Box}]$ and $\langle
R^{\mathrm{I}}_{\Diamond}\rangle$ are defined as in Section 2.2.

The satisfiability relation for an interpretation $\mathrm{I}$ is defined as
follows:

1\. $\mathrm{I}\models C_{1}\equiv C_{2}$ iff
$[\\![{C_{1}^{\mathrm{I}}}]\\!]=[\\![{C_{2}^{\mathrm{I}}}]\\!]$ iff
$(\\![{C_{2}^{\mathrm{I}}}]\\!)=(\\![{C_{1}^{\mathrm{I}}}]\\!)$.

2\. $\mathrm{I}\models a:C$ iff $a^{\mathrm{I}}\in[\\![{C^{\mathrm{I}}}]\\!]$
and $\mathrm{I}\models x::C$ iff
$x^{\mathrm{I}}\in(\\![{C^{\mathrm{I}}}]\\!)$.

3\. $\mathrm{I}\models aIx$ (resp. $aR_{\Box}x$, $xR_{\Diamond}a$) iff
$a^{\mathrm{I}}I^{\mathrm{I}}x^{\mathrm{I}}$ (resp.
$a^{\mathrm{I}}R_{\Box}^{\mathrm{I}}x^{\mathrm{I}}$,
$x^{\mathrm{I}}R_{\Diamond}^{\mathrm{I}}a^{\mathrm{I}}$).

4\. $\mathrm{I}\models\neg\alpha$, where $\alpha$ is any ABox term, iff
$\mathrm{I}\not\models\alpha$.

An interpretation $\mathrm{I}$ is a model  for an LE-$\mathcal{ALC}$ knowledge
base $(\mathcal{A},\mathcal{T})$ if $\mathrm{I}\models\mathcal{A}$ and
$\mathrm{I}\models\mathcal{T}$. An LE-$\mathcal{ALC}$ knowledge base
$(\mathcal{A},\mathcal{T})$ (resp. TBox $\mathcal{T}$, resp. ABox
$\mathcal{A}$) is said to be inconsistent if it has no model.

The framework of LE-$\mathcal{ALC}$ formally brings FCA and DL together in two
important ways: (1) the concepts of LE-$\mathcal{ALC}$ are naturally
interpreted as formal concepts in FCA; (2) the language of LE-$\mathcal{ALC}$
is designed to represent knowledge and reasoning in the setting of enriched
formal contexts.

##  4 Tableaux algorithm for ABox of LE-$\mathcal{ALC}$

In this section, we define a tableaux algorithm for checking the consistency
of LE-$\mathcal{ALC}$ ABoxes. An LE-$\mathcal{ALC}$ ABox $\mathcal{A}$
contains a clash iff it contains both $\beta$ and $\neg\beta$ for some
relational term $\beta$. The expansion rules below are designed so that the
expansion of $\mathcal{A}$ will contain a clash iff $\mathcal{A}$ is
inconsistent. The set $sub(C)$ of sub-formulas of any LE-$\mathcal{ALC}$
concept $C$ is defined as usual.

A concept $C^{\prime}$ occurs in $\mathcal{A}$ (in symbols:
$C^{\prime}\in\mathcal{A}$) if $C^{\prime}\in sub(C)$ for some $C$ such that
one of the terms $a:C$, $x::C$, $\neg a:C$, or $\neg x::C$ is in
$\mathcal{A}$. A constant $b$ (resp. $y$) occurs in $\mathcal{A}$
($b\in\mathcal{A}$, or $y\in\mathcal{A}$), iff some term containing $b$ (resp.
$y$) occurs in it.

The tableaux algorithm below constructs a model
$(\mathbb{F},\cdot^{\mathrm{I}})$ for every consistent $\mathcal{A}$, where
$\mathbb{F}=(\mathbb{P},\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$ is such
that, for any $C\in\mathcal{A}$, some $a_{C}\in A$ and $x_{C}\in X$ exist such
that, for any $a\in A$ (resp. any $x\in X$), $a\in[\\![{C^{\mathrm{I}}}]\\!]$
(resp. $x\in(\\![{C}]\\!)^{\mathrm{I}}$) iff $aIx_{C}$ (resp. $a_{C}Ix$). We
call $a_{C}$ and $x_{C}$ the classifying object and the classifying feature of
$C$, respectively. To make our notation more easily readable, we will write
$a_{\Box C}$, $x_{\Box C}$ (resp. $a_{\Diamond C}$, $x_{\Diamond C}$) instead
of $a_{[R_{\Box}]C}$, $x_{[R_{\Box}]C}$ (resp. $a_{\langle R_{\Diamond}\rangle
C}$, $x_{\langle R_{\Diamond}\rangle C}$) Moreover, for every
$R_{\Box}\in\mathcal{R}_{\Box}$ and $R_{\Diamond}\in\mathcal{R}_{\Diamond}$,
we will also impose the condition that $a\in[\\![{[R_{\Box}]C}]\\!]$ (resp.
$x\in(\\![{\langle R_{\Diamond}\rangle C}]\\!)$) iff $aR_{\Box}x_{C}$ (resp.
$xR_{\Diamond}a_{C}$), where $a_{C}$ and $x_{C}$ are the classifying object
and the classifying feature of $C$, respectively. Note that we can always
assume w.l.o.g. that any consistent ABox $\mathcal{A}$ is satisfiable in a
model with classifying objects and features (cf. Theorem 4.3).

Algorithm 1 tableaux algorithm for checking LE-$\mathcal{ALC}$ ABox
consistency

Input: An LE-$\mathcal{ALC}$ ABox $\mathcal{A}$. Output: whether $\mathcal{A}$
is inconsistent.

1:if there is a clash in $\mathcal{A}$ then return “inconsistent”.

2:pick any applicable expansion rule $R$, apply $R$ to $\mathcal{A}$ and
proceed recursively.

3:if no expansion rule is applicable return “consistent”.

Below, we list the expansion rules. The commas in each rule are metalinguistic
conjunctions, hence every tableau is non-branching.

Creation rule | Basic rule
---|---
For any $C\in\mathcal{A}$ create $a_{C}:C$, $x_{C}::C$ |

Rules for the logical connectives |  $I$-compatibility rules
---|---
$b:C_{1}\wedge C_{2}$ $\wedge_{A}$ $b:C_{1},$ $b:C_{2}$ |  $bI\blacksquare y$ $\blacksquare y$ $yR_{\Diamond}b$ |
$b:[R_{\Box}]C,$ $y::C$ $\Box$ $bR_{\Box}y$ |  $\blacklozenge bIy$ $\blacklozenge b$ $bR_{\Box}y$ |
inverse rules for the lattice connectives
---
$b:C_{1}$, $b:C_{2}$, $C_{1}\wedge C_{2}\in\overline{\mathcal{A}}$ $\wedge_{A}^{-1}$ $b:C_{1}\wedge C_{2}$ |  $y::C_{1}$, $y::C_{2}$, $C_{1}\vee C_{2}\in\overline{\mathcal{A}}$ $\vee_{X}^{-1}$ $y::C_{1}\vee C_{2}$

Adjunction rules
---
$bR_{\Box}y$ $R_{\Box}$ $\blacklozenge bIy,$ $bI\Box y$ |  $yR_{\Diamond}b$ $R_{\Diamond}$ $\Diamond bIy,$ $bI\blacksquare y$

Basic rules for negative assertions | Appending rules
---|---
$\neg(b:C)$ $\neg b$ $\neg(bIx_{C})$ |  $a_{C}Iy$ $a_{C}$ $y::C$ |

In the adjunction rules the individuals $\blacklozenge b$, $\Diamond b$, $\Box
y$, and $\blacksquare y$ are new and unique for each relation $R_{\Box}$ and
$R_{\Diamond}$, except for $\Diamond a_{C}=a_{\Diamond C}$ and $\Box
x_{C}=x_{\Box C}$. Side conditions for rules $\wedge_{A}^{-1}$, and
$\vee_{X}^{-1}$ ensure we do not add new joins or meets to concepts.

It is easy to check that the following rules are derivable in the calculus.
$b:C_{1}\vee C_{2},$ $y::C_{1},$ $y::C_{2}$ $\vee_{A}$ $bIy$ $y::C_{1}\wedge
C_{2},$ $b:C_{1},$ $b:C_{2}$ $\wedge_{X}$ $bIy$ $\blacklozenge b:C$
$adj_{\Box}$ $b:[R_{\Box}]C$ $\blacksquare y::C$ $adj_{\Diamond}$ $y::\langle
R_{\Diamond}\rangle C$

The basic rule and the logical rules for the connectives encode the semantics
of the logical connectives in LE-$\mathcal{ALC}$. The creation rule makes sure
that, whenever successful, the algorithm outputs models with classifying
object $a_{C}$ and feature $x_{C}$ for every concept $C\in\mathcal{A}$. The
adjunction rules and $I$-compatibility rules imply that every
$R_{\Box}\in\mathcal{R}_{\Box}$ and $R_{\Diamond}\in\mathcal{R}_{\Diamond}$
are $I$-compatible. Appending and negative assertion rules encode the defining
property of classifying objects and features of concepts.

###### Example 1

Let
$\mathcal{A}=\\{b:[R_{\Box}][R_{\Box}]C_{1},b:[R_{\Box}][R_{\Box}]C_{2},y::[R_{\Box}](C_{1}\wedge
C_{2}),\neg(bR_{\Box}y)\\}$. It is easy to check that $\mathcal{A}$ has no
LE-$\mathcal{ALC}$ model. The algorithm applies on $\mathcal{A}$ as follows
(we only do the partial expansion to show that the clash exists):

Rule | Premises | Added terms |
---|---|---|---
Creation |  |  $x_{\Box C_{1}}\\!::\\![R_{\Box}]C_{1}$, $x_{\Box C_{2}}\\!::\\![R_{\Box}]C_{2}$, $x_{C_{1}\wedge C_{2}}::C_{1}\wedge C_{2}$ |
$\Box$ |  $x_{\Box C_{i}}\\!::\\![R_{\Box}]C_{i}$, $b\\!:\\![R_{\Box}][R_{\Box}]C_{i}$ | $bR_{\Box}x_{\Box C_{i}}$ | $i=1,2$
$R_{\Box}$ | $bR_{\Box}x_{\Box C_{i}}$ | $\blacklozenge bIx_{\Box C_{i}}$ | $i=1,2$
Appending | $\blacklozenge bIx_{\Box C_{i}}$ | $\blacklozenge b:[R_{\Box}]C_{i}$ | $i=1,2$

By applying the same process to $\blacklozenge b:[R_{\Box}]C_{1}$,
$\blacklozenge b:[R_{\Box}]C_{2}$ and $x_{\Box C_{1}}::[R_{\Box}]C_{1}$,
$x_{\Box C_{2}}::[R_{\Box}]C_{2}$, we add the terms
$\blacklozenge\blacklozenge b:C_{1}$ and $\blacklozenge\blacklozenge b:C_{2}$
to the tableau. Then the further tableau expansion is as follows:

Rule | Premises | Added terms |
---|---|---|---
$\wedge_{X}$ |  $x_{C_{1}\wedge C_{2}}::C_{1}\wedge C_{2}$, $\blacklozenge\blacklozenge b:C_{1}$, $\blacklozenge\blacklozenge b:C_{2}$, $\blacklozenge\blacklozenge b:C_{1}$ | $\blacklozenge\blacklozenge bIx_{C_{1}\wedge C_{2}}$ |
Appending | $\blacklozenge\blacklozenge bIx_{C_{1}\wedge C_{2}}$ | $\blacklozenge\blacklozenge b:C_{1}\wedge C_{2}$ |
$adj_{\Box}$ (twice) | $\blacklozenge\blacklozenge b:C_{1}\wedge C_{2}$ | $b:[R_{\Box}][R_{\Box}](C_{1}\wedge C_{2})$ |
$\Box$ |  $b:[R_{\Box}][R_{\Box}](C_{1}\wedge C_{2})$, $y::[R_{\Box}](C_{1}\wedge C_{2})$ | $bR_{\Box}y$ |

Thus, there is a clash between $\neg(bR_{\Box}y)$ and $bR_{\Box}y$ in the
expansion.

###### Example 2

Let $\mathcal{A}=\\{\neg(bIy),y::C_{1},\neg(b:C_{2}),b:C_{1}\vee
C_{2},bR_{\Box}y\\}$. The following table shows the tableau expansion for
$\mathcal{A}$. Let $\mathcal{W}\coloneqq\\{C_{1},C_{2},C_{1}\vee C_{2}\\}$.

Rule | Premises | Added terms
---|---|---
Creation |  |  $a_{C}:C$, $x_{C}::C$, $C\in\mathcal{W}$
Basic |  $a_{C}:C$, $x_{C}::C$, $C\in\mathcal{W}$ |  $a_{C}Ix_{C}$, $C\in\mathcal{W}$
Appending |  $a_{C_{1}}Ix_{C_{1}\vee C_{2}}$, $a_{C_{2}}Ix_{C_{1}\vee C_{2}}$ |  $a_{C_{1}}:C_{1}\vee C_{2}$, $a_{C_{2}}:C_{1}\vee C_{2}$
$\vee_{X}$ | $x_{C_{1}\vee C_{2}}::C_{1}\vee C_{2}$ |  $x_{C_{1}\vee C_{2}}::C_{1}$, $x_{C_{1}\vee C_{2}}::C_{2}$
Basic |  $a_{C_{1}}::C_{1}\vee C_{2}$, $x_{C_{1}\vee C_{2}}::C_{1}$ | $a_{C_{1}}Ix_{C_{1}\vee C_{2}}$
Basic |  $a_{C_{2}}::C_{1}\vee C_{2}$, $x_{C_{1}\vee C_{2}}::C_{1}$ | $a_{C_{2}}Ix_{C_{1}\vee C_{2}}$
$R_{\Box}$ | $bR_{\Box}y$ |  $\blacklozenge bIy$, $bI\Box y$
$\neg_{b}$ | $\neg(b:C_{2})$ | $\neg(bIx_{C_{2}})$

Note that no expansion rule is applicable anymore. It is clear that the
tableau does not contain any clashes. Thus, this ABox has a model. By the
procedure described in Section 4.2, this model is given by
$\mathcal{R}_{\Box}=\\{R_{\Box}\\},\mathcal{R}_{\Diamond}=\\{R_{\Diamond}\\},A=\\{a_{C_{1}},a_{C_{2}},a_{C_{1}\vee
C_{2}},b,\blacklozenge b\\}$, $X=\\{x_{C_{1}},x_{C_{2}},x_{C_{1}\vee
C_{2}},y,\Box y\\}$, $I=\\{(a_{C},x_{C})_{C\in\mathcal{W}},\\\
(a_{C_{1}},x_{C_{1}\vee C_{2}}),(a_{C_{2}},x_{C_{1}\vee C_{2}}),(\blacklozenge
b,y),(b,\Box y)\\}$, $R_{\Box}=\\{(b,y)\\}$, $R_{\Diamond}=\varnothing$.

###  4.1 Termination of the tableaux algorithm

In this section, we show that Algorithm 1 always terminates for any finite
LE-$\mathcal{ALC}$ ABox $\mathcal{A}$. Since no rule branches, we only need to
check that the number of new individuals added by the expansion rules is
finite. Note that the only rules for adding new individuals are the creation
and adjunction rules. The creation rules add one new object and feature for
every concept $C$ occurring in the expansion of $\mathcal{A}$. Thus, it is
enough to show that the number of individuals and new concepts added by
applying adjunction rules is finite. To do so, we will show that any
individual constant introduced by means of any adjunction rule will contain
only finitely many modal operators applied to a constant occurring in
$\mathcal{A}$ or added by the creation rule and any new concept added will
contain finitely many $\Box$ and $\Diamond$ operators applied to a concept
occurring in $\mathcal{A}$.

###### Definition 1

The $\Diamond$-depth $\Diamond_{\mathcal{D}}$ and $\Box$-depth
$\Box_{\mathcal{D}}$ of $C$ is defined as follows:

1\. If $C$ is an atomic concept, then
$\Diamond_{\mathcal{D}}(C)=\Box_{\mathcal{D}}(C)=0$;

2\. $\Diamond_{\mathcal{D}}(\langle R_{\Diamond}\rangle
C)=\Diamond_{\mathcal{D}}(C)+1$ and $\Box_{\mathcal{D}}(\langle
R_{\Diamond}\rangle C)=\Box_{\mathcal{D}}(C)$;

3\. $\Diamond_{\mathcal{D}}([R_{\Box}]C)=\Diamond_{\mathcal{D}}(C)$ and
$\Box_{\mathcal{D}}([R_{\Box}]C)=\Box_{\mathcal{D}}(C)+1$;

4\. $\Diamond_{\mathcal{D}}(C_{1}\vee
C_{2})=\max(\Diamond_{\mathcal{D}}(C_{1}),\Diamond_{\mathcal{D}}(C_{2}))$ and
$\Box_{\mathcal{D}}(C_{1}\wedge
C_{2})=\max(\Box_{\mathcal{D}}(C_{1}),\Box_{\mathcal{D}}(C_{2}))$;

5\. $\Diamond_{\mathcal{D}}(C_{1}\wedge
C_{2})=\min(\Diamond_{\mathcal{D}}(C_{1}),\Diamond_{\mathcal{D}}(C_{2}))$ and
$\Box_{\mathcal{D}}(C_{1}\vee
C_{2})=\min(\Box_{\mathcal{D}}(C_{1}),\Box_{\mathcal{D}}(C_{2}))$.

###### Definition 2

The $\Box$-depth $\Box_{\mathcal{D}}$ and $\Diamond$-depth
$\Diamond_{\mathcal{D}}$ of any constants $b$ and $y$ are:

1\. if $b,y\in\mathcal{A}$,
$\Box_{\mathcal{D}}(b)=\Diamond_{\mathcal{D}}(b)=\Box_{\mathcal{D}}(y)=\Diamond_{\mathcal{D}}(y)=0$;

2\. $\Box_{\mathcal{D}}(a_{C})=0$, $\Diamond_{\mathcal{D}}(x_{C})=0$,
$\Box_{\mathcal{D}}(x_{C})=-\Box_{\mathcal{D}}(C)$, and
$\Diamond_{\mathcal{D}}(a_{C})=-\Diamond_{\mathcal{D}}(C)$;

3\. $\Box_{\mathcal{D}}(\blacklozenge b)=\Box_{\mathcal{D}}(b)+1$,
$\Box_{\mathcal{D}}(\Diamond b)=\Box_{\mathcal{D}}(b)$,
$\Diamond_{\mathcal{D}}(\blacklozenge b)=\Diamond_{\mathcal{D}}(b)$,
$\Diamond_{\mathcal{D}}(\Diamond b)=\Diamond_{\mathcal{D}}(b)-1$;

4\. $\Box_{\mathcal{D}}(\Box y)=\Box_{\mathcal{D}}(y)-1$,
$\Diamond_{\mathcal{D}}(\Box y)=\Diamond_{\mathcal{D}}(y)$,
$\Box_{\mathcal{D}}(\blacksquare y)=\Box_{\mathcal{D}}(y)$,
$\Diamond_{\mathcal{D}}(\blacksquare y)=\Diamond_{\mathcal{D}}(y)+1$.

###### Definition 3

The $\Box$-depth (resp. $\Diamond$-depth) of an ABox $\mathcal{A}$ is
$\Box_{\mathcal{D}}(\mathcal{A})\coloneqq\max\\{\Box_{\mathcal{D}}(C^{\prime})\
|\ C^{\prime}\in\mathcal{A}$} (resp.
$\Diamond_{\mathcal{D}}(\mathcal{A})\coloneqq\max\\{\Diamond_{\mathcal{D}}(C^{\prime})\
|\ C^{\prime}\in\mathcal{A}$}).

The following Lemma bounds the length of concept and individual names
appearing in a tableaux.

###### Lemma 1

For any individual names $b$, and $y$, and concept $C$ added during tableau
expansion of ${\mathcal{A}}$,

$\Box_{\mathcal{D}}(C)\leq\Box_{\mathcal{D}}(\mathcal{A})+1\,\mbox{ and
}\,\Diamond_{\mathcal{D}}(C)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1,$ (2)

$-\Diamond_{\mathcal{D}}(\mathcal{A})-1\leq\Diamond_{\mathcal{D}}(b)\,\mbox{
and }\,\Box_{\mathcal{D}}(b)\leq\Box_{\mathcal{D}}(\mathcal{A})+1,$ (3)

$-\Box_{\mathcal{D}}(\mathcal{A})-1\leq\Box_{\mathcal{D}}(y)\,\mbox{ and
}\,\Diamond_{\mathcal{D}}(y)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$ (4)

###### Proof

We prove a stronger property of $\overline{\mathcal{A}}$, obtained from
$\mathcal{A}$ after any finite number of expansion steps.

1\. For any term $bIy\in\overline{\mathcal{A}}$,
$\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(y)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and
$\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

2\. For any term $bR_{\Box}y\in\overline{\mathcal{A}}$,
$\Box_{\mathcal{D}}(b)+1-\Box_{\mathcal{D}}(y)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and
$\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

3\. For any term $yR_{\Diamond}b\in\overline{\mathcal{A}}$,
$\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(y)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and
$\Diamond_{\mathcal{D}}(y)+1-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

4\. For any term $b:C\in\overline{\mathcal{A}}$,
$\Box_{\mathcal{D}}(b)+\Box_{\mathcal{D}}(C)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and $-\Diamond_{\mathcal{D}}(b)-\Diamond_{\mathcal{D}}(C)\leq 0$.

5\. For any term $y::C\in\overline{\mathcal{A}}$,
$-\Box_{\mathcal{D}}(y)-\Box_{\mathcal{D}}(C)\leq 0$, and
$\Diamond_{\mathcal{D}}(y)+\Diamond_{\mathcal{D}}(C)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

The proof is by simultaneous (over all the claims) induction on the number of
expansion rules applied. The base case is immediate from the definitions as
every individual name in the original ABox has $\Box$-depth and
$\Diamond$-depth zero, and $\Box$-depth and $\Diamond$-depth are positive and
bounded by $\Box_{\mathcal{D}}(\mathcal{A})$ and
$\Diamond_{\mathcal{D}}(\mathcal{A})$, respectively. The inductive steps are
proved below:

creation rule: it follows immediately from the definitions.

Basic rule $I$: in this case the new term $bIy$ is added from the terms $b:C$,
and $y::C$. We need to show that item 1 holds for the term $bIy$. Using
induction on $b:C$ and $y::C$, by items 4 and 5, we have
$\Box_{\mathcal{D}}(b)+\Box_{\mathcal{D}}(C)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and $-\Box_{\mathcal{D}}(y)-\Box_{\mathcal{D}}(C)\leq 0$. By adding these
inequalities, we get
$\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(y)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$.
Similarly, by items 4 and 5, we have
$\Diamond_{\mathcal{D}}(y)+\Diamond_{\mathcal{D}}(C)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$,
and $-\Diamond_{\mathcal{D}}(b)-\Diamond_{\mathcal{D}}(C)\leq 0$. By adding
these inequalities, we get
$\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

Rules $\wedge_{A}$, $\wedge_{X}$, $\wedge_{A}^{-1}$, $\wedge_{X}^{-1}$:
immediate from the definitions and the induction hypothesis.

$I$-compatibility rules: we only give a proof for the rule $\Box y$. The other
proofs are analogous. We need to prove that item 2 holds for the newly added
term $bR_{\Box}y$. By induction applied to the term $bI\Box y$ from item 1, we
get $\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(\Box
y)=\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(y)+1\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and $\Diamond_{\mathcal{D}}(\Box
y)-\Diamond_{\mathcal{D}}(b)=\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

$\Box$ and $\Diamond$ rules: we only give the proof for the $\Box$ case, as
the proof for the $\Diamond$ rule is analogous. Using induction on
$b:[R_{\Box}]C$ and $y::C$, by items 4 and 5, we have
$\Box_{\mathcal{D}}(b)+\Box_{\mathcal{D}}([R_{\Box}]C)=\Box_{\mathcal{D}}(b)+\Box_{\mathcal{D}}(C)+1\leq\Box_{\mathcal{D}}(\mathcal{A})+1$,
and $-\Box_{\mathcal{D}}(y)-\Box_{\mathcal{D}}(C)\leq 0$. By adding them, we
get
$\Box_{\mathcal{D}}(b)+1-\Box_{\mathcal{D}}(y)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$.
Similarly, by items 4 and 5 we have
$-\Diamond_{\mathcal{D}}(b)-\Diamond_{\mathcal{D}}([R_{\Box}]C)=-\Diamond_{\mathcal{D}}(b)-\Diamond_{\mathcal{D}}(C)\leq
0$, and
$\Diamond_{\mathcal{D}}(y)+\Diamond_{\mathcal{D}}(C)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.
Hence,
$\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

Adjunction rules $R_{\Box}$ and $R_{\Diamond}$: we only give the proof for
$R_{\Box}$. The proof for the $R_{\Diamond}$ case is analogous. We need to
prove item 1 for the terms $\blacklozenge bIy$ and $bI\Box y$. By the
induction hypothesis applied to $bR_{\Box}y$, by item 2 we have
$\Box_{\mathcal{D}}(b)+1-\Box_{\mathcal{D}}(y)=\Box_{\mathcal{D}}(\blacklozenge
b)-\Box_{\mathcal{D}}(y)=\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(\Box
y)\leq\Box_{\mathcal{D}}(\mathcal{A})+1$. Similarly, we also have
$\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(b)=\Diamond_{\mathcal{D}}(y)-\Diamond_{\mathcal{D}}(\blacklozenge
b)=\Diamond_{\mathcal{D}}(\Box
y)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

Appending rules $a_{C}$ and $x_{C}$: we only give the proof for $x_{C}$. The
proof for $a_{C}$ is analogous. We add a new term $b:C$ from the term
$bIx_{C}$. As $\Box_{\mathcal{D}}(x_{C})=-\Box_{\mathcal{D}}(C)$ and
$\Diamond_{\mathcal{D}}(x_{C})=-\Diamond_{\mathcal{D}}(C)$, by the induction
hypothesis and using Equation (4) for $x_{C}$, we immediately get the required
conditions on $\Box_{\mathcal{D}}(C)$ and $\Diamond_{\mathcal{D}}(C)$.
Moreover, by induction on term $bIx_{C}$ using item 1, we have
$-\Box_{\mathcal{D}}(\mathcal{A})-1\leq\Box_{\mathcal{D}}(b)-\Box_{\mathcal{D}}(x_{C})=\Box_{\mathcal{D}}(b)+\Box_{\mathcal{D}}(x_{C})\leq\Box_{\mathcal{D}}(\mathcal{A})+1$
and
$-\Diamond_{\mathcal{D}}(\mathcal{A})-1\leq\Diamond_{\mathcal{D}}(x_{C})-\Diamond_{\mathcal{D}}(b)=-\Diamond_{\mathcal{D}}(C)-\Diamond_{\mathcal{D}}(b)\leq\Diamond_{\mathcal{D}}(\mathcal{A})+1$.

###### Definition 4

For any concept ABox term of the form $t\equiv a:C$ or $t\equiv x::C$,
$size(t)=1+|sub(C)|$. For any relational term $\beta$, $size(\beta)=2$. For
any LE-$\mathcal{ALC}$ ABox $\mathcal{A}$,
$size(\mathcal{A})=\sum_{t\in\mathcal{A}}size(t)$.

######  Theorem 4.1 (Termination)

For any ABox $\mathcal{A}$, the tableaux algorithm 1 terminates in a finite
number of steps which is polynomial in $size(\mathcal{A})$.

###### Proof

New individuals are added to the tableau only in the following ways:

(1) individuals of the form $a_{C}$ or $x_{C}$ can be added by creation rules;

(2) individuals of the form $\Box y$, $\blacksquare y$, $\Diamond b$, and
$\blacklozenge b$ can be added through the expansion rules for $bR_{\Box}x$
and $yR_{\Diamond}a$.

New concepts can only be added by the appending rules through some constant
that was already added. Note that no new propositional connective is added by
any of the rules. Thus, the only concept that can appear are added by the
application of $\Box$ and $\Diamond$ operators to concepts already appearing
in $\mathcal{A}$. By Equation (2) of Lemma 1, the maximum number of $\Box$ or
$\Diamond$ connectives appearing in any concept added is bounded by
$\Box_{\mathcal{D}}(\mathcal{A})+1$ and
$\Diamond_{\mathcal{D}}(\mathcal{A})+1$, respectively. Also, by Equations (3)
and (4) of Lemma 1 the number of $\blacklozenge$ (resp. $\Diamond$, $\Box$,
$\blacksquare$), occurring in a constant $b$ (resp. $b$, $y$, $y$) is bounded
by $\Box_{\mathcal{D}}(\mathcal{A})+1$ (resp.
$\Diamond_{\mathcal{D}}(\mathcal{A})+1$, $\Box_{\mathcal{D}}(\mathcal{A})+1$,
$\Diamond_{\mathcal{D}}(\mathcal{A})+1$). Therefore, the total number of new
constant and concepts occurring in an expansion of $\mathcal{A}$ is bounded by
$size(\mathcal{A})*(\Box_{\mathcal{D}}(\mathcal{A})+\Diamond_{\mathcal{D}}(\mathcal{A}))$.
Thus, only finitely many individuals of type (2) are added. Overall, the size
of the tableau expansion (and hence the model) is
$O((size(\mathcal{A})*(\Box_{\mathcal{D}}(\mathcal{A})+\Diamond_{\mathcal{D}}(\mathcal{A}))^{2}*(|\mathcal{R}_{\Box}|+|\mathcal{R}_{\Diamond}|))$.
Since the tableaux algorithm for LE-$\mathcal{ALC}$ does not involve any
branching, the above theorem implies that the time complexity of checking the
consistency of an LE-$\mathcal{ALC}$ ABox $\mathcal{A}$ using the tableaux
algorithm is $Poly(size(\mathcal{A}))$.

###  4.2 Soundness of the tableaux algorithm

For any consistent ABox $\mathcal{A}$, we let its completion
$\overline{\mathcal{A}}$ be its maximal expansion (which exists due to
termination) after post-processing. If there is no clash in
$\overline{\mathcal{A}}$, we construct a model
$(\mathbb{F},\cdot^{\mathrm{I}})$ where $A$ and $X$ are the sets of names of
objects and features occurring in the expansion, and for any $a\in A$, $x\in
X$, and any role names $R_{\Box}\in\mathcal{R}_{\Box}$,
$R_{\Diamond}\in\mathcal{R}_{\Diamond}$ we have $aIx$, $aR_{\Box}x$,
$xR_{\Diamond}a$ iff such relational terms explicitly occur in
$\overline{\mathcal{A}}$. We also add a new element $x_{\bot}$ (resp.
$a_{\top}$) to $X$ (resp. $A$) such that it is not related to any element of
$A$ (resp. $X$) by any relation. Let
$\mathbb{F}=(A,X,I,\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$ be the
relational structure obtained in this manner. We define an interpretation
$\mathrm{I}$ on it as follows. For any object name $a$, and feature name $x$,
we let $a^{\mathrm{I}}\coloneqq a$ and $x^{\mathrm{I}}\coloneqq x$. For any
atomic concept $D$, we define
$D^{\mathrm{I}}=({x_{D}}^{\downarrow},{a_{D}}^{\uparrow})$. Next, we show that
$\mathrm{I}$ is a valid interpretation for LE-$\mathcal{ALC}$. To this end, we
need to show that $\mathbb{F}$ is an enriched formal context, i.e. that all
$R_{\Box}$ and $R_{\Diamond}$ are $I$-compatible, and that $D^{\mathrm{I}}$ is
a concept in the concept lattice $\mathbb{P}^{+}$ of $\mathbb{P}=(A,X,I)$. The
latter condition is shown in the next lemma, and the former in the subsequent
one.

###### Lemma 2

$x_{D}^{\downarrow\uparrow}=a_{D}^{\uparrow}$ and
$a_{D}^{\uparrow\downarrow}=x_{D}^{\downarrow}$ for any $D\in\mathcal{C}$.

###### Proof

For any atomic concept $D$, we have $a_{D}Ix_{D}$ by the creation and
appending rules. Therefore, $I^{(0)}[I^{(1)}[a_{D}]]\subseteq I^{(0)}[x_{D}]$.
Suppose $a_{D}Iy$ and $bIx_{D}$ are in $\overline{\mathcal{A}}$, then by the
appending and basic rule we get $bIy\in\overline{\mathcal{A}}$. Therefore,
$I^{(0)}[x_{D}]\subseteq I^{(0)}[I^{(1)}[a_{D}]]$. Hence the statement is
proved.

###### Lemma 3

All the relations $R_{\Box}\in\mathcal{R}_{\Box}$ and
$R_{\Diamond}\in\mathcal{R}_{\Diamond}$ in
$\mathbb{F}=(\mathbb{P},\mathcal{R}_{\Box},\mathcal{R}_{\Diamond})$ are
$I$-compatible.

###### Proof

We prove that $R_{\Box}^{(0)}[y]$ is Galois-stable for every $y$ appearing in
$\overline{\mathcal{A}}$. All the remaining proofs are similar. Consider the
case where $\Box y$ appears in the tableaux expansion: if $bI\Box y$ (resp.
$bR_{\Box}y)$ is in $\overline{\mathcal{A}}$, then $bR_{\Box}y$ (resp. $bI\Box
y$) is added by the rule $\Box y$ (resp. $R_{\Box}$).

In the case where $\Box y$ does not appear in $\overline{\mathcal{A}}$, then
there is no term of the form $bR_{\Box}y$ in $\overline{\mathcal{A}}$.
Therefore, we have that $R_{\Box}^{(0)}[y]=\emptyset=I^{(0)}[X]$ is Galois-
stable, because we have a feature $x_{\bot}$ which is not related to any of
the objects.

From the lemmas above, it immediately follows that the tuple
$M=(\mathbb{F},\cdot^{\mathrm{I}})$, with $\mathbb{F}$ and
$\cdot^{\mathrm{I}}$ defined at the beginning of the present section, is a
model for LE-$\mathcal{ALC}$. The following lemma states that the
interpretation of any concept $C$ in the model $M$ is completely determined by
the terms of the form $bIx_{C}$ and $a_{C}Iy$ occurring in the tableau
expansion.

###### Lemma 4

Let $M=(\mathbb{F},\cdot^{\mathrm{I}})$ be the model defined by the
construction above. Then for any concept $C$ and individuals $b$, $y$
occurring in ${\mathcal{A}}$,

(1) $b\in[\\![{C}]\\!]_{M}$ iff $bIx_{C}\in\overline{\mathcal{A}}$ (2)
$y\in(\\![{C}]\\!)_{M}$ iff $a_{C}Iy\in\overline{\mathcal{A}}$.

###### Proof

The proof is by simultaneous induction on the complexity of $C$. The base case
is obvious by the construction of $M$.

For the induction step, we distinguish four cases.

1\. Suppose $C=C_{1}\wedge C_{2}$.

For the first claim, notice that $b\in[\\![{C_{1}\wedge C_{2}}]\\!]$ iff
$b\in[\\![{C_{1}}]\\!]$, and $b\in[\\![{C_{2}}]\\!]$. By the induction
hypothesis, this is equivalent to
$bIx_{C_{1}},bIx_{C_{2}}\in\overline{\mathcal{A}}$. Suppose
$b\in[\\![{C_{1}\wedge C_{2}}]\\!]$. Then
$bIx_{C_{1}},bIx_{C_{2}}\in\overline{\mathcal{A}}$. By the appending rules,
$b:C_{1},b:C_{2}\in\overline{\mathcal{A}}$. As $C_{1}\wedge C_{2}$ appears in
$\overline{\mathcal{A}}$, by rule $\wedge_{A}^{-1}$, $b:C_{1}\wedge C_{2}$ is
added which by the creation and appending rule implies $bIx_{C_{1}\wedge
C_{2}}\in\overline{\mathcal{A}}$. Conversely, suppose $bIx_{C_{1}\wedge
C_{2}}\in\overline{\mathcal{A}}$. By the appending rule we have $b:C_{1}\wedge
C_{2}\in\overline{\mathcal{A}}$. By rule $\wedge_{A}$, we have
$b:C_{1},b:C_{2}\in\overline{\mathcal{A}}$. By the creation and basic rule we
have $bIx_{C_{1}},bIx_{C_{2}}\in\overline{\mathcal{A}}$. By induction
hypothesis, this implies $b\in[\\![{C_{1}}]\\!]$, and $b\in[\\![{C_{2}}]\\!]$.
By definition, this implies $b\in[\\![{C_{1}\wedge C_{2}}]\\!]$.

To prove item 2, $y\in(\\![{C_{1}\wedge C_{2}}]\\!)$ iff $\forall
b(b\in[\\![{C_{1}\wedge C_{2}}]\\!]\implies bIy\in\overline{\mathcal{A}})$. By
the proof above, this is equivalent to $\forall b(bIx_{C_{1}\wedge
C_{2}}\in\overline{\mathcal{A}}\implies bIy\in\overline{\mathcal{A}})$.
Suppose $y\in(\\![{C_{1}\wedge C_{2}}]\\!)$. By creation and basic rule,
$a_{C_{1}\wedge C_{2}}Ix_{C_{1}\wedge C_{2}}\in\overline{\mathcal{A}}$. By
$\forall b(bIx_{C_{1}\wedge C_{2}}\in\overline{\mathcal{A}}\implies
bIy\in\overline{\mathcal{A}})$, we get $a_{C_{1}\wedge C_{2}}Iy$. Conversely,
suppose $a_{C_{1}\wedge C_{2}}Iy\in\overline{\mathcal{A}}$. From
$bIx_{C_{1}\wedge C_{2}}\in\overline{\mathcal{A}}$ and by the appending and
basic rule, we get $bIy\in\overline{\mathcal{A}}$. Hence the statement is
proved.

2\. The proof for $C=C_{1}\vee C_{2}$ is similar to the previous case.

3\. Suppose $C=[R_{\Box}]C_{1}$.

For the first claim, notice that $b\in[\\![{[R_{\Box}]C_{1}}]\\!]$ iff
$\forall y(y\in(\\![{C}]\\!)\implies bR_{\Box}y)$. By the induction
hypothesis, this is equivalent to $\forall
y(a_{C}Iy\in\overline{\mathcal{A}}\implies
bR_{\Box}y\in\overline{\mathcal{A}})$. Suppose
$b\in[\\![{[R_{\Box}]C_{1}}]\\!]$. By the creation and basic rule,
$a_{C_{1}}Ix_{C_{1}}\in\overline{\mathcal{A}}$. Then by $\forall
y(a_{C}Iy\in\overline{\mathcal{A}}\implies
bR_{\Box}y\in\overline{\mathcal{A}})$, we have
$bR_{\Box}x_{C_{1}}\in\overline{\mathcal{A}}$, meaning that via rule
$R_{\Box}$ we get $bIx_{\Box C_{1}}\in\overline{\mathcal{A}}$. Conversely,
suppose $bIx_{\Box C_{1}}$ and $a_{C_{1}}Iy$ occur in
$\overline{\mathcal{A}}$. By rule $\Box y$, we have $\blacklozenge
bIx_{C_{1}}\in\overline{\mathcal{A}}$. By the appending and basic rule,
$\blacklozenge bIy\in\overline{\mathcal{A}}$. By rule $\blacklozenge b$, we
get $bR_{\Box}y\in\overline{\mathcal{A}}$.

To prove item 2, $y\in(\\![{[R_{\Box}]C_{1}}]\\!)$ iff $\forall
b(b\in[\\![{[R_{\Box}]C_{1}}]\\!]\implies bIy)$. By the proof above, this is
equivalent to $\forall
b(bIx_{[R_{\Box}]C_{1}}\in\overline{\mathcal{A}}\implies
bIy\in\overline{\mathcal{A}})$. Suppose $y\in(\\![{[R_{\Box}]C_{1}}]\\!)$. By
the creation and basic rule we have
$a_{[R_{\Box}]C_{1}}Ix_{[R_{\Box}]C_{1}}\in\overline{\mathcal{A}}$. Therefore,
by $\forall b(bIx_{[R_{\Box}]C_{1}}\in\overline{\mathcal{A}}\implies
bIy\in\overline{\mathcal{A}})$, we have
$a_{[R_{\Box}]C_{1}}Iy\in\overline{\mathcal{A}}$. Conversely, suppose
$a_{[R_{\Box}]C_{1}}Iy\in\overline{\mathcal{A}}$ and
$bIx_{[R_{\Box}]C_{1}}\in\overline{\mathcal{A}}$. By the appending and basic
rule, we get $bIy\in\overline{\mathcal{A}}$. Hence the statement is proved.

4\. The proof for $C=\langle R_{\Diamond}\rangle C_{1}$ is similar to the
previous one.

######  Theorem 4.2 (Soundness)

The model $M=(\mathbb{F},\cdot^{\mathrm{I}})$ defined above satisfies the ABox
$\mathcal{A}$.

###### Proof

We proceed by cases.

1\. By construction, $M$ satisfies all terms of the form $bR_{\Box}y$, $bIy$,
or $yR_{\Diamond}b$ in $\mathcal{A}$.

2\. By construction, any relational term is satisfied by $M$ iff it explicitly
occurs in $\overline{\mathcal{A}}$. Thus, either $M$ satisfies all terms of
the form $\neg(bR_{\Box}y)$, $\neg(bIy)$, and $\neg(yR_{\Diamond}b)$ occurring
in $\mathcal{A}$, or some expansion of ${\mathcal{A}}$ contains a clash.

3\. For the terms of the form $b:C$, $y::C$, $\neg(b:C)$, or $\neg(y::C)$, we
have $b\in[\\![{C}]\\!]$ iff $bIx_{C}\in\overline{\mathcal{A}}$, and
$y\in(\\![{C}]\\!)$ iff $a_{C}Iy\in\overline{\mathcal{A}}$ (Lemma 4). For any
$b:C$, $y::C$, $\neg(b:C)$, or $\neg(y::C)$ occurring in $\mathcal{A}$, we
respectively add $bIx_{C}$, $a_{C}Iy$, $\neg(bIx_{C})$, or $\neg(a_{C}Iy)$ to
$\overline{\mathcal{A}}$ via the expansion rules, and thus $M$ satisfies the
constraints.

The following corollary is an immediate consequence of the termination and
soundness of the tableau procedure.

######  Corollary 1 (Finite Model Property)

For any consistent LE-$\mathcal{ALC}$ ABox $\mathcal{A}$, some model of
$\mathcal{A}$ exists the size of which is polynomial in $size(\mathcal{A})$.

###### Proof

The model $M$ of Theorem 4.2 is the required witness. The polynomial bound on
the size of $M$ follows from the proof of Theorem 4.1.

###  4.3 Completeness of the tableaux algorithm

In this section, we prove the completeness of the tableau algorithm. The
following lemma is key to this end, since it shows that every model for an
LE-$\mathcal{ALC}$ ABox can be extended to a model with classifying object and
features.

###### Lemma 5

For any ABox $\mathcal{A}$, any model $M=(\mathbb{F},\cdot^{\mathrm{I}})$ of
$\mathcal{A}$ can be extended to a model
$M^{\prime}=(\mathbb{F}^{\prime},\cdot^{\mathrm{I}^{\prime}})$ such that
$\mathbb{F}^{\prime}=(A^{\prime},X^{\prime},I^{\prime},\\{R_{\Box}^{\prime}\\}_{\Box\in\mathcal{G}},\\{R_{\Diamond}^{\prime}\\}_{\Diamond\in\mathcal{F}})$,
$A\subseteq A^{\prime}$ and $X\subseteq X^{\prime}$, and moreover for every
$\Box\in\mathcal{G}$ and $\Diamond\in\mathcal{F}$:

1\. There exists $a_{C}\in A^{\prime}$ and $x_{C}\in X^{\prime}$ such that:

$C^{\mathrm{I}^{\prime}}=(I^{\prime(0)}[x_{C}^{\mathrm{I}^{\prime}}],I^{\prime(1)}[a_{C}^{\mathrm{I}^{\prime}}]),\quad
a_{C}^{\mathrm{I}^{\prime}}\in[\\![{C^{\mathrm{I}^{\prime}}}]\\!],\quad
x_{C}^{\mathrm{I}^{\prime}}\in(\\![{C^{\mathrm{I}^{\prime}}}]\\!),$ (5)

2\. For every individual $b$ in $A$ there exist $\Diamond b$ and
$\blacklozenge b$ in $A^{\prime}$ such that:

$I^{\prime(1)}[\blacklozenge
b]=R_{\Box}^{\prime(1)}[b^{\mathrm{I}^{\prime}}]\quad\mbox{and}\quad
I^{\prime(1)}[\Diamond b]=R_{\Diamond}^{\prime(0)}[b^{\mathrm{I}^{\prime}}],$
(6)

3\. For every individual $y$ in $X$ there exist $\Box y$ and $\blacksquare y$
in $X^{\prime}$ such that:

$I^{\prime(0)}[\blacksquare
y]=R_{\Diamond}^{\prime(1)}[y^{\mathrm{I}^{\prime}}]\quad\mbox{and}\quad
I^{\prime(0)}[\Box y]=R_{\Box}^{\prime(0)}[y^{\mathrm{I}^{\prime}}].$ (7)

4\. For any $C$,
$[\\![{C^{\mathrm{I}}}]\\!]=[\\![{C^{\mathrm{I^{\prime}}}}]\\!]\cap A$ and
$(\\![{C^{\mathrm{I}}}]\\!)=(\\![{C^{\mathrm{I^{\prime}}}}]\\!)\cap X$.

###### Proof

Fix $\Box\in\mathcal{G}$ and $\Diamond\in\mathcal{F}$. Let $M^{\prime}$ be
defined as follows. For every concept $C$, we add new elements $a_{C}$ and
$x_{C}$ to $A$ and $X$ (respectively) to obtain the sets $A^{\prime}$ and
$X^{\prime}$. For any $J\in\\{I,R_{\Box}\\}$, any $a\in A^{\prime}$ and $x\in
X^{\prime}$, we set $aJ^{\prime}x$ iff one of the following holds:

1\. $a\in A$, $x\in X$, and $aJx$;

2\. $x\in X$, and $a=a_{C}$ for some concept $C$, and $bJx$ for all
$b\in[\\![{C^{\mathrm{I}}}]\\!]$;

3\. $a\in A$, and $x=x_{C}$ for some concept $C$, and $aJy$ for all
$y\in(\\![{C^{\mathrm{I}}}]\\!)$;

4\. $a=a_{C_{1}}$ and $x=x_{C_{2}}$ for some $C_{1}$, $C_{2}$, and $bJy$ for
all $b\in[\\![{C_{1}^{\mathrm{I}}}]\\!]$, and
$y\in(\\![{C_{2}^{\mathrm{I}}}]\\!)$.

We set $xR_{\Diamond}^{\prime}a$ iff one of the following holds:

1\. $a\in A$, $x\in X$, and $xR_{\Diamond}a$;

2\. $x\in X$, and $a=a_{C}$ for some concept $C$, and $xR_{\Diamond}b$ for all
$b\in[\\![{C^{\mathrm{I}}}]\\!]$;

3\. $a\in A$, and $x=x_{C}$ for some concept $C$, and $yR_{\Diamond}a$ for all
$y\in(\\![{C^{\mathrm{I}}}]\\!)$;

4\. $a=a_{C_{1}}$ and $x=x_{C_{2}}$ for some $C_{1}$, $C_{2}$, and
$yR_{\Diamond}b$ for all $b\in[\\![{C_{1}^{\mathrm{I}}}]\\!]$,
$y\in(\\![{C_{2}^{\mathrm{I}}}]\\!)$.

For any $b\in A$, $y\in X$, let $\blacklozenge b=a_{\blacklozenge(cl(b))}$,
$\Diamond b=a_{\Diamond(cl(b))}$, $\blacksquare y=x_{\blacksquare(cl(y))}$,
and $\Box y=x_{\Box(cl(y))}$, where $cl(b)$ (resp. $cl(y)$) is the smallest
concept generated by $b$ (resp. $y$), and the operations $\blacklozenge$ and
$\blacksquare$ are the adjoints of operations $\Box$ and $\Diamond$,
respectively. For any $C$, let
$C^{\mathrm{I^{\prime}}}=(I^{\prime(0)}[x_{C}],I^{\prime(1)}[a_{C}])$. Then
$M^{\prime}$ is as required.

######  Theorem 4.3 (Completeness)

Let $\mathcal{A}$ be a consistent ABox and $\mathcal{A}^{\prime}$ be obtained
via the application of any expansion rule or post-processing applied to
$\mathcal{A}$. Then $\mathcal{A}^{\prime}$ is also consistent.

###### Proof

If $\mathcal{A}$ is consistent, by Lemma 5, a model $M^{\prime}$ of
$\mathcal{A}$ exists which satisfies (5), (6) and (7). The statement follows
from the fact that any term added by any expansion rule or in post-processing
is satisfied by $M^{\prime}$ where we interpret $a_{C}$, $x_{C}$,
$\blacklozenge b$, $\Diamond b$, $\Box y$, $\blacksquare y$ as in Lemma 5.

###### Remark 1

The algorithm can easily be extended to acyclic TBoxes, via the unravelling
technique (cf. [3] for details). Notice that in the presence of TBoxes that
are not completely unravelled (cf. Subsection 2.1), polynomial-time complexity
for the consistency check procedure is not necessarily preserved.

##  5 Conclusion and future work

In this paper, we define a two-sorted non-distributive description logic
LE-$\mathcal{ALC}$ to describe and reason about formal concepts arising from
(enriched) formal contexts from FCA. We describe ABox and TBox terms for the
logic and define a tableaux algorithm for it. This tableaux algorithm decides
the consistency of ABoxes and acyclic TBoxes, and provides a procedure to
construct a model when the input is consistent. We show that this algorithm is
computationally more efficient than the tableaux algorithm for
$\mathcal{ALC}$.

This work can be extended in several interesting directions.

Dealing with cyclic TBoxes and RBox axioms. In this paper, we introduced a
tableaux algorithm only for knowledge bases with acyclic TBoxes. We conjecture
that the following statement holds of general (i.e. possibly cyclic) TBoxes.

Developing such an algorithm is a research direction we are currently
pursuing. Another aspect we intend to develop in future work concerns giving a
complete axiomatization for LE-$\mathcal{ALC}$. RBox axioms are used in
description logics to describe the relationship between different relations in
knowledge bases and the properties of these relations such as reflexivity,
symmetry, and transitivity. It would be interesting to see if it is possible
to obtain necessary and/or sufficient conditions on the shape of RBox axioms
for which a tableaux algorithm can be obtained. This has an interesting
relationship with the problem in LE-logic of providing computationally
efficient proof systems for various extensions of LE-logic in a modular manner
[16, 5].

Generalizing to other semantic frameworks. The non-distributive DL introduced
in this paper is semantically motivated by a relational semantics for LE-
logics which establishes a link with FCA. A different semantics for the same
logic, referred to as graph-based semantics [12], provides another
interpretation of the same logic as a logic suitable for evidential and hyper-
constructivist reasoning. In the future, we intend to develop description
logics for reasoning in the framework of graph-based semantics, to
appropriately model evidential and hyper-constructivist settings.

Generalizing to more expressive description logics. The DL LE-$\mathcal{ALC}$
is the non-distributive counterpart of $\mathcal{ALC}$. A natural direction
for further research is to explore the non-distributive counterparts of
extensions of $\mathcal{ALC}$ such as $\mathcal{ALCI}$ and $\mathcal{ALCIN}$.

Description logic and Formal Concept Analysis. The relationship between FCA
and DL has been studied and used in several applications [1, 4, 17]. The
framework of LE-$\mathcal{ALC}$ formally brings FCA and DL together, both
because its concepts are naturally interpreted as formal concepts in FCA, and
because its language is designed to represent knowledge and reasoning in
enriched formal contexts. Thus, these results pave the way to the possibility
of establishing a closer and more formally explicit connection between FCA and
DL, and of using this connection in theory and applications.

## References

  * [1] Atif, J., Hudelot, C., Bloch, I.: Explanatory reasoning for image understanding using formal concept analysis and description logics. IEEE Transactions on Systems, Man, and Cybernetics: Systems 44(5), 552–570 (2014)
  * [2] Baader, F., Calvanese, D., McGuinness, D., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook: Theory, Implementation and Applications. Cambridge University Press (2003)
  * [3] Baader, F., Horrocks, I., Lutz, C., Sattler, U.: An Introduction to Description Logic. Cambridge University Press (2017)
  * [4] Baader, F., Sertkaya, B.: Applying formal concept analysis to description logics. Concept Lattices pp. 261–286 (2004)
  * [5] van der Berg, I., De Domenico, A., Greco, G., Manoorkar, K.B., Palmigiano, A., Panettiere, M.: Labelled calculi for the logics of rough concepts. Logic and Its Applications pp. 172–188 (2023)
  * [6] Borgwardt, S., Peñaloza, R.: Fuzzy description logics – a survey. Scalable Uncertainty Management pp. 31–45 (2017)
  * [7] Conradie, W., De Domenico, A., Manoorkar, K., Palmigiano, A., Panettiere, M., Prieto, D.P., Tzimoulis, A.: Modal reduction principles across relational semantics. arXiv preprint arXiv:2202.00899 (2022)
  * [8] Conradie, W., Frittella, S., Manoorkar, K., Nazari, S., Palmigiano, A., Tzimoulis, A., Wijnberg, N.M.: Rough concepts. Information Sciences 561, 371–413 (2021)
  * [9] Conradie, W., Frittella, S., Palmigiano, A., Piazzai, M., Tzimoulis, A., Wijnberg, N.M.: Toward an epistemic-logical theory of categorization. Electronic Proceedings in Theoretical Computer Science, EPTCS 251 (2017)
  * [10] Conradie, W., Frittella, S., Palmigiano, A., Piazzai, M., Tzimoulis, A., Wijnberg, N.M.: Categories: how I learned to stop worrying and love two sorts. In: International Workshop on Logic, Language, Information, and Computation. pp. 145–164. Springer (2016)
  * [11] Conradie, W., Palmigiano, A.: Algorithmic correspondence and canonicity for non-distributive logics. Annals of Pure and Applied Logic 170(9), 923–974 (2019)
  * [12] Conradie, W., Palmigiano, A., Robinson, C., Wijnberg, N.: Non-distributive logics: from semantics to meaning. In: Rezus, A. (ed.) Contemporary Logic and Computing, Landscapes in Logic, vol. 1, pp. 38–86. College Publications (2020)
  * [13] Ganter, B., Wille, R.: Formal concept analysis: mathematical foundations. Springer Science & Business Media (2012)
  * [14] Giordano, L., Gliozzi, V., Olivetti, N., Pozzato, G.L.: Semantic characterization of rational closure: From propositional logic to description logics. Artificial Intelligence 226, 1–33 (2015)
  * [15] Giordano, L., Gliozzi, V., Theseider Dupré, D.: A conditional, a fuzzy and a probabilistic interpretation of self-organizing maps. Journal of Logic and Computation 32(2), 178–205 (2022)
  * [16] Greco, G., Ma, M., Palmigiano, A., Tzimoulis, A., Zhao, Z.: Unified correspondence as a proof-theoretic tool. Journal of Logic and Computation 28(7), 1367–1442 (2016)
  * [17] Jiang, Y.: Semantifying formal concept analysis using description logics. Knowledge-Based Systems 186 (2019)
  * [18] Lieto, A., Pozzato, G.L.: A description logic framework for commonsense conceptual combination integrating typicality, probabilities and cognitive heuristics. Journal of Experimental & Theoretical Artificial Intelligence 32(5), 769–804 (2020)
  * [19] Ma, Z.M., Zhang, F., Wang, H., Yan, L.: An overview of fuzzy description logics for the semantic web. The Knowledge Engineering Review 28(1), 1–34 (2013)
  * [20] de Paiva, V., Haeusler, E.H., Rademaker, A.: Constructive description logics hybrid-style. Electronic Notes in Theoretical Computer Science 273, 21–31 (2011)
  * [21] Shilov, N.V., Han, S.Y.: A proposal of description logic on concept lattices. In: Proceedings of the Fifth International Conference on Concept Lattices and their Applications. pp. 165–176 (2007)
  * [22] Wurm, C.: Language-theoretic and finite relation models for the (full) lambek calculus. Journal of Logic, Language and Information 26(2), 179–214 (2017)


# RFSoC-based front-end electronics for pulse detection

S. N. Axani  S. Futagi11footnotetext: Present address: National Institute of
Advanced Industrial Science and Technology, Tsukuba, Ibaraki 305-8560, Japan
M. Garcia  C. Grant  K. Hosokawa22footnotetext: Present address: Kamioka
Observatory, Institute for Cosmic-Ray Research, The University of Tokyo, Hida,
Gifu 506-1205, Japan S. Ieki  K. Inoue  K. Ishidoshiro  N. Kawada  Y.
Matsumoto  T. Nakahata  K. Nakamura  R. Shouji  H. Song  L. A. Winslow

###### Abstract

Radiation measurement relies on pulse detection, which can be performed using
various configurations of high-speed analog-to-digital converters (ADCs) and
field-programmable gate arrays (FPGAs). For optimal power consumption, design
simplicity, system flexibility, and the availability of DSP slices, we
consider the Radio Frequency System-on-Chip (RFSoC) to be a more suitable
option than traditional setups. To this end, we have developed custom RFSoC-
based electronics and verified its feasibility. The ADCs on RFSoC exhibit a
flat frequency response of 1-125 MHz. The root-mean-square (RMS) noise level
is 2.1 ADC without any digital signal processing. The digital signal
processing improves the RMS noise level to 0.8 ADC (input equivalent 40
$\mu$V${}_{\textrm{rms}}$). Baseline correction via digital signal processing
can effectively prevent photomultiplier overshoot after a large pulse.
Crosstalk between all channels is less than -55 dB. The measured data transfer
speed can support up to 32 kHz trigger rates (corresponding to 750 Mbps).
Overall, our RFSoC-based electronics are highly suitable for pulse detection,
and after some modifications, they will be employed in the Kamioka Liquid
Scintillator Anti-Neutrino Detector (KamLAND).

##  1 Introduction

Pulse detection serves as a fundamental role in particle and nuclear physics
[1], and radiation measurements [2]. In the pursuit of extracting maximal
information from pulses, the acquisition of pulse waveforms stands as a
crucial objective. To address this goal, systems equipped with high-speed
analog-to-digital converters (ADCs) and field-programmable gate arrays (FPGAs)
are commonly employed. In most cases, ADCs digitize the analog waveforms with
a sampling speed of 50 MS/s to 1 GS/s and a resolution of 8 to 12-bits. The
FPGA is used mainly to control and read out the ADCs and transmit the
digitized waveforms to back-end computers. To improve sampling speed,
application-specific integrated circuits (ASICs) such as Domino Ring Sampling
(DRS4) chips [3] are often used. Nevertheless, the DRS4 is not ideal for dead-
time free measurements. In astroparticle physics, dead-time free measurements
assume significance, particularly in experiments targeting rare events like
neutrinos, dark matter, and neutrinoless double beta decay. This is due to
certain background discrimination strategies necessitating the capture of
pulses very close in time.

Consequently, many rare event search experiments devise custom electronics [4,
5, 6, 7]. Similarly, we have developed and implemented dead-time free front-
end electronics within the Kamioka Liquid Scintillator Anti-Neutrino Detector
(KamLAND). KamLAND is an 1 kiloton liquid scintillator (LS) detector located
in the Kamioka mine. It was originally designed to detect $\bar{\nu}_{e}$ from
Japan’s nuclear reactors [8] and geoneutrinos [9]. Currently, KamLAND is
searching for neutrinoless double beta decay (0$\nu\beta\beta$) of 136Xe in
the KamLAND-Zen experiment. The dead-time free front-end electronics played a
pivotal role in enabling world-leading search for $0\nu\beta\beta$ [10, 11].
Nonetheless, the front-end electronics exhibits limitations concerning buffer
capacity, readout speed, and digital processing resources. These limitations
hinder the detection efficiency of neutrons originating from cosmic-ray
spallation, one of the most significant backgrounds in KamLAND-Zen. Triple
coincidences among cosmic-ray muons, neutron events, and spallation product
decay can identify the spallation backgrounds. However, the difficulty of the
triple coincidence identification is the low neutron detection efficiency.
Cosmic-ray muons induce large pulses that saturate the Photomultiplier Tubes
(PMTs), subsequently burying the neutron-related signals within PMT overshoot
and afterpulses. To enhance neutron detection efficiency, it is desirable to
correct the waveform overshoot and capture all pulses generated, including
afterpulses, with substantial buffer capacity and rapid readout. Accompanied
by state-of-the-art software processing on back-end computers, this approach
can provide better neutron detection efficiency. Additionally, the power
consumption posses additional constraints in environments with restricted
power and cooling resources.

To solve these problems, we propose the integration of Radio Frequency System-
on-Chip (RFSoC) technology. The RFSoC, a cutting-edge FPGA family developed by
AMD Xilinx, amalgamates programmable logic (PL) with a large number of digital
signal processors, a quad-core processing system (PS) based on Arm Cortex-A53
and a dual-core Arm Cortex-R5F processors, and radio-frequency ADCs (RF-ADCs),
and radio-frequency digital-to-analog converters (RF-DACs). The application of
RFSoC technology holds promise for achieving dead-time free pulse detection,
particularly within the KamLAND-Zen experiment. It offers notable advantages
over conventional systems, including easy implementation of high speed data
transfer with 1 GbE or 10 GbE, easy handling to external and/or internal
memory, low power consumption due to the tight integration between the ADCs
and PL, and the large number of logic cells and digital signal processors.
RFSoCs have begun to make inroads into physics experiments, aiding in
controlling and extracting data from superconducting qubits [12, 13].
Moreover, the application of RFSoC technology in radio astronomy receivers has
been recently explored [14]. Despite these advances, the application of RFSoC
for pulse detection remains uncharted territory.

In this paper, we conduct feasibility studies on a custom built RFSoC-based
front-end system aimed at achieving dead-time free pulse detection.

##  2 Prototype design

The custom electronics (shown in Fig. 1) consists of a Main Board and 16
analog daughter cards. The firmware and software for this board was developed
with Vivado 2019.2, Vitis 2019.2, and PetaLinux2019.2. This section describes
the RFSoC-based front-end electronics.

###  2.1 Main Board

The main board is designed in accordance with the VME9U standard. The main
board accommodates a single RFSoC (XCZU29DR-1FFVF1760E), hosting 16 RF-ADCs
with 12-bit resolution and a maximum sampling rate of 2.058 GS/s, and 16 RF-
DACs with 14-bit resolution and a maximum sampling rate of 6.554 GS/s. This
RFSoC also integrates 930,300 logic cells, 4,272 digital signal processing
elements (DSP slices), a quad-core Arm Cortex-A53, and a dual-core Arm
Cortex-R5. The PS and PL are each integrated with 4 GB Double-Data-Rate (DDR)
Synchronous Dynamic Random Access Memory (SDRAM).

The front panel accommodates 16 Bayonet-Neel-Concelman (BNC) connectors, which
operate as 50 $\Omega$ inputs for the RG58 coaxial cables capacitively coupled
to the anode of the KamLAND PMTs. The analog signal from each PMT is feed into
a daughter card, where the signal is terminated and split into a high-gain
($h$-gain) and low-gain ($l$-gain) channel. The $h$-gain output from the
daughter cards utilize the RF-ADCs, while the $l$-gain output employs
additional 250 MS/s, 16-bit ADCs (ADS42LB69). The use of the slow DACs enables
the RF-ADCs to digitize -150 mV to +50 mV in the input level with a $\sim 50$
$\mu$V resolution. To further minimize reflections off of the inputs to the
amplifier, we also back terminate the input at the PMT base as well. The front
panel also includes two LEMO connectors, designated for Transistor-Transistor
Logic (TTL) input and output. These TTL interfaces are used for external-
triggered waveform recording and debugging.

The rear face of the board houses two VME connectors, two RJ45 connectors, and
two enhanced small form-factor pluggable (SFP+) ports. The VME connectors are
used for providing power ($\pm 12$ V, 5 V, 3.3 V). One RJ45 port manages slow
control and data transmission via 1 GbE, while the other functions as an input
for an external clock (50 MHz) and system reset for synchronization with
external modules. The SFP+ ports are provisioned for prospective expansions
and can potentially facilitate 10 GbE data transmission.

Figure 1: The front-end electronics for our feasibility studies.

###  2.2 Analog daughter card

The analog circuit on the daughter card amplifies the uni-polar PMT signal to
detect single-to-a-few-tens of photoelectrons (p.e.) through the $h$-gain
channel and attenuates the signal to record large pulse waveforms induced by
the cosmic-muon events through the $l$-gain channel. Both channels are
designed to have a flat gain response as possible. Noise levels are minimized
through the choice of low-noise amplifiers, anti-aliasing via the natural
frequency response of the amplifiers, electromagnetic induction shielding, and
careful attention to circuit board layout. Additionally, the digitized signal
on the RFSoC PL further reduce noise through oversampling.

The $h$-gain signal path passes through an isolation resistor to a cascade of
non-inverting LMH6703 (SOT23-6 package) ultra-low distortion wide-bandwidth
current feedback amplifiers. The output of the amplifiers is capacitively
coupled to a single ended input fully differential amplifier (FDA). A current
feedback LMH6552 (WSON package) FDA is used to drive the inputs of the RF-ADC.
The FDA 1.2 V common mode voltage is supplied by the RF-ADC. Given the uni-
polar nature of the PMT signal, we unbalance the feedback path of the FDA such
that we can maximize our dynamic range. When the input to the front end is
grounded, the common mode voltage of the FDA is 1.2 V and the unbalancing sets
the default output levels to approximately 1.4 V and 1.0 V. This maximizes the
dynamic range and provides 50 mV input equivalent of overhead for digitizing
the overshoot introduced through capacitive coupling. A clamping diode on each
output of the FDA limits the voltage between 1.2 V +/- 0.4 V. This is well
within the fully reliable region (-0.3 V to 2.1 V) of the RF-ADC and within
the RF-ADC over-voltage range (1.2 V +/-0.45V). The conceptual analog design
is in Fig. 2.

The $l$-gain channel is designed to digitize the $\sim$8 V pulse with a
$\sim$0.1 mV resolution. The analog circuit attenuates the signal to
effectively match the dynamic range of the $l$-gain ADCs. To check the
consistency between the $h$-gain and the $l$-gain, 20-70 p.e. pulses should be
effectively recorded with both gain channels. The $l$-gain channel is standard
analog design with conventional ADCs. In this paper, we do not report the
details of the $l$-gain channel.

Prior to commissioning the daughter cards for experimental use, the cards are
tested by injecting approximately 100 years of equivalent large amplitude
pulses into the system and the performance of the cards is re-checked.

Figure 2: A simplified schematic of the analog daughter card design described
in the text.

###  2.3 Programmable logic

The data flow through the PL is shown in Figure 3. We configure the RF-ADCs to
operate at 2 GS/s with a $\times 2$ decimation, effectively yielding an
overall sampling rate of 1 GS/s. Each RF-ADC output adheres to the Advanced
eXtensible Interface 4 stream (AXI4-stream)) standard. Its data size (TDATA)
amounts to 128 bits (8 samples $\times$ 16 bits) at a 125 MHz frequency. Its
valid signal (TVALID) is concurrently generated by the RF-ADCs. Notably,
Xilinx guarantees the upper 12 bits of the RF-ADCs’ output. The lower 4 bits
are truncated, and the remaining bits are routed through the digital signal
processing (DSP) module. This module applies filtering to enhance the signal-
to-noise ratio for single photoelectron measurements and correct overshoot
phenomena following large pulse events.

The DSP module’s output is split into two AXI4-Streams. One stream is directed
to a digital discriminator, which issues an event-hit flag based on a simple
amplitude threshold. Alternative types of hit flags include an external-hit
flag derived from the TTL input and a forced flag controlled by the PS and/or
an external module via the RJ45 connector. These flags converge as a single
trigger flag at a trigger selector, which amalgamates them according to the
designated trigger mode.

The other stream is delayed to accommodate the processing time of the digital
discriminator and trigger selector. On the data trigger, the TVALID signal
within this AXI4-Stream is then temporarily set to ’Low’ (’L’). Determined by
the trigger flag outcome from the trigger selector, TVALID is subsequently set
to ’High’ (’H’), inclusive of pre-defined post/pre times. A frame generator
identifies individual events based on the state of TVALID and produces a
corresponding frame of data inclusive of headers, footers, timestamps, and
$l$-gain ADC values using the 56 kB buffer located on block random access
memories (BRAM). The output from the frame generator is converted to an
AXI4-Stream.

The 16 AXI4-Streams from the 16 frame generators are managed via an
AXI4-Stream Interconnect, a feature provided by Xilinx employing the Round-
Robin arbitration scheme. The merged AXI4-Stream is subsequently directed
towards the AXI Direct Memory Access (AXI DMA) Intellectual Property (IP)
module via a First in First out (FIFO) buffer. All pertinent parameters
governing PL functions are set through AXI4-lite or AXI4 on the PS.

Figure 3: PL firmware design

###  2.4 DSP module

A DSP module performs baseline restoration (BLR) and digital filtering. The
BLR aims to remove the waveform overshoot after a large pulse. This overshoot
is effectively mitigated by computing a 64 ns moving average within the
negative region of the waveform. Subtracting this moving average from the
original digitized waveform results in the generation of the BLR waveform. A
conceptual image of BLR is shown in Fig. 4.

The BLR waveform is now digitally filtered by applying a simple 8 ns moving
average (MA). The selection of an 8 ns length is optimized to minimize high-
frequency noise while preserving the PMT signal. This design is developed
using System Generator for DSP and MATLAB/Simulink.

Figure 4: Concept of digital BLR

###  2.5 Processing system

The PS, encompassing a quad-core Arm Cortex-A53 architecture, operates on a
Linux environment that has been compiled using Petalinux 2019.2. The PS reads
the data from PL and sends them to back-end computer(s) through a 1 GbE
connection, which is implemented via the Gigabit Ethernet MAC (GEM3) module
employing Multiplexed Input/Output (MIO). To facilitate seamless communication
via traditional TCP sockets, the system has been equipped with ZeroMQ [15].
Consequently, the main board can function as a ZMQ module, simplifying
communication tasks. It’s worth noting that a potential future enhancement
includes the possibility of utilizing the 10 GbE connection with high-speed
transceivers in the PL.

##  3 Prototype test

We conducted an evaluation of our customized electronics using a Wiener VME9U
crate. The electronics demonstrated successful operation with the following
power specifications: +12 V at 0.7 A, -12 V at 0.3 A, +5 V at 6 A, and +3.3 V
at 0.4 A. This translates to a total power consumption of 43 W with the test
firmware in place. We note that the power consumption of the +3.3 V line is
expected to increase when utilizing the 10 GbE connection, since it is
primarily utilized to power SFP+ modules.

In comparison, our previous dead-time free electronics, which utilized the
conventional ADCs and FPGA configuration, operated with 12 analog inputs and
consumed 74 W. This represents an enhanced power efficiency per channel of
56%. In this section, we delve into board testing, with a primary focus on the
$h$-gain channels.

###  3.1 Frequency response

We conducted measurements to evaluate the response using 10 mV (500 mV) sine
waves across various frequencies within the $h$-gain ($l$-gain) channels.
Figure 5 provides a comparison between the measured frequency responses and
the expected responses, with MA on the DSP module enabled (disabled). With MA,
the designed cut-off frequency is set at 68 MHz. The measured and designed
frequency responses exhibit no significant disparities. This result shows that
the RF-ADC’s frequency response maintains flatness within the range of 1 to
125 MHz, with a cut-off frequency controllable through the DSP module.

Figure 5: Frequency response of $h$-gain with and without the 8 ns moving
average (MA) on DSP and $l$-gain. There is no significant difference between
data and simulation.

###  3.2 Noise level

We performed measurements to assess the noise level in the absence of input
configuration. Figure 6 shows both the histogram and spectrum of the input
equivalent noise from the $h$-gain data. Without MA, the root mean square
(RMS) noise level amounts to 2.1 ADC${}_{\textrm{rms}}$, which corresponds to
an input equivalent 100 $\mu$V${}_{\textrm{rms}}$. A noise spectral density
measurement indicated the line noise at 250 MHz, which corresponded to double
the frequency of the system clock. Employing MA on DSP suppress the noise
level to 0.9 ADC${}_{\textrm{rms}}$ (an input equivalent 40
$\mu$V${}_{\textrm{rms}}$). The right panel of Fig. 6 depicts how MA
effectively mitigates the line noise. With this low noise level, 2 mV pulses,
which corresponds to a single photoelectron pulse, are clearly visible, as
shown in Fig. 7.

Figure 6: Noise histogram (left) and spectrum (right) with and without MV.
Applying MV, the noise level is 0.9 ADC${}_{\textrm{rms}}$ and there is no
structure in the frequency space. Figure 7: Example of 2 mV pulse detection
with and without 8 ns moving average (MV). An amplitude of 2 mV corresponds to
the single photoelectron peak.

###  3.3 Discriminator threshold

A threshold scan was conducted in order to evaluate the discriminator
thresholds available. Figure 8 illustrates the hit rate as a function of
discriminator thresholds. For this evaluation, 2 mV pulses with a duration of
20 ns were injected into the system using an arbitrary waveform generator at a
frequency of 1 kHz. Given that we expect the single photoelectron peak to
occur around 40 ADC counts, a threshold of 1/5 p.e. is achievable.
Regrettably, the noise originating from the waveform generator amounts to 126
$\mu$V${}_{\textrm{rms}}$, nearly three times larger than the electronics
noise.

Figure 8: Results of threshold scan using 2 mV pulses with a duration of 20
ns. From its derivative (blue dotted curves), a clear peak structure can be
seen around threshold of 39 ADC counts. Given the scan, a threshold can be
safely set at the 1/5 p.e. level.

###  3.4 Linearity

Ensuring linearity in the response is crucial when quantifying the number of
photoelectrons detected by PMTs. To assess this aspect, we employed a waveform
generator to generate pulses characterized with a 40 ns time window. Our
evaluation involved comparing the input equivalent amplitudes against the
corresponding input amplitudes across various levels (Fig. 9). Barring pulses
less than 1 mV and exceeding 100 mV, the input equivalent amplitude is
observed to be withing $\pm 2\%$ of the desired level. Our target is the
single photoelectron events, typical amplitude $\sim 2$ mV. Thus, deviations
at 1 mV is not a problem and can be compensated for during calibration if
needed. By tuning the DAC output, it is feasible to tune the saturation
amplitude to approximately 150 mV. Importantly, the $h$-gain and $l$-gain are
naturally interconnected.

Figure 9: (Left) Output (recorded) amplitudes as a function of input
amplitudes. (Right) Residual as a function of input amplitude. There is
sufficient overlap range between $h$-gain and $l$-gain. Input and output
amplitudes match within 2% most of the range.

###  3.5 Crosstalk

To prevent the creation of spurious single photoelectron-like signals, a
crosstalk level of at least -55 dB is necessary. To evaluate the crosstalk, we
introduced sine waves with a frequency of $f=10$ MHz and an amplitude of 25
mV. We define the "rock-in amplitude" ($A$) as:

$\displaystyle A=2\sqrt{\langle s(t)\times\cos(2\pi ft)\rangle^{2}+\langle
s(t)\times\sin(2\pi ft)\rangle^{2})}$ (3.1)

$\langle\cdot\cdot\cdot\rangle$ is mean of $\cdot\cdot\cdot$, $s(t)$ is
measured time-series data as a func of time $t$. When the sine waves is
introduced to to $j$ channel, evaluating the crosstalk from channel $j$ to
channel $i$ involves the calculation:

$\displaystyle
20\log_{10}\Biggl{(}\frac{A^{i}}{A^{j}}\Biggr{)}~{}\textrm{[dB]},$ (3.2)

where $i=0,1,\cdot\cdot\cdot 15$ but not $j$. Fig. 10 shows the measured
crosstalk levels, showcasing that they remain below the required level. The
average crosstalk was measured at -62.3 dB, while the highest value recorded
was -55.2 dB, stemming from interactions between different tiles. These
measurements indicates that the observed crosstalk is within acceptable
limits, effectively preventing the generation of fake single photoelectron
signals.

Figure 10: Results of crosstalk measurements. The vertical axis shows the
input channel of the sine wave, the horizontal axis shows the channel of the
crosstalk measurement at that time, and the $z$ axis shows the magnitude of
the crosstalk.

###  3.6 Test with a real 20-inch PMT

We validated the baseline correction function implemented within BLR on the
DSP module using a 20-inch PMT (HAMAMATSU R12860). This validation process
involved employing a light-emitting diode (LED) to illuminate the PMT, as
depicted in Fig. 11. The timing of LED’s light was controlled through a pulse
generator. The trigger output from the generator signal was supplied to the
front-end electronics for the external-hit flag.

Fig. 12 shows the acquired waveform data both with and without BLR. The
baseline was subsequently adjusted to zero during the offline analysis. The
primary LED-induced pulses appears around the 400-600 ns. Without BLR, the
baseline deviates from zero due to the presence of overshoot. With BLR, the
baseline effectively returns to zero within approximately 200 ns. We also
confirmed that the baseline correction did not cause any distortion for the
PMT signal waveform.

Figure 11: Test setup with a read 20-inch PMT.  Figure 12: LED pulse and
overshoot waveforms w/ and w/o the BLR on the DSP module. With BLR, the
baseline restored 200 ns after the end of the LED pulse.

###  3.7 Date transfer

The KamLAND experiment which use 20-inch PMTs with a typical dark rate of 25
kHz. We assume that the duration of a single event amounts to 80 ns,
translating to 184 Bytes, inclusive of headers and footers. As a result, the
minimum required data rate to record all dark hits is 588.8 Mbps. In KamLAND,
the cosmic-muon rate is approximately 0.3 Hz. Following a muon event, we
anticipate a subsequent afterpulse rate of 1 MHz, lasting 1 ms. The event rate
within the KamLAND is approximately 100 Hz. These are low-occupancy events
resembling single photon hits. Thus, the main contribution is from the dark
pulse and a data transfer speed of 600 Mbps is sufficient for our objectives.

We evaluated the data transfer speed with respect to the external-hit flag
rate. Our approach involved setting up a ZMQ client on a back-end computer
running Ubuntu 18.04.6 LTS. This client was designed to receive data from the
ZMQ server located on the RFSoC PS. Throughout this evaluation, the focus was
solely on measuring the data transfer speed within the ZMQ client. To maintain
the clarity of the assessment, we refrained from implementing additional
processes like data saving. The results of this evaluation are presented in
Fig. 13, showcasing the measured data transfer speed versus varying external
trigger rates. The figure indicates consistency, with expected values and
stable data transfer performance for external triggers below 32 kHz (750
Mbps). However, a noticeable deviation becomes apparent when comparing the
measured and expected speeds beyond an external trigger rate of 40 kHz. These
findings allow us to validate that a dark rate of 25 kHz and a data transfer
speed of 600 Mbps are attainable for the intended purposes in KamLAND. It
should be noted that throughout the entirety of this evaluation, our
utilization was restricted to the capabilities of 1 GbE. The incorporation of
10 GbE through the SFP+ connector will open the potential for conducting data-
taking operations at significantly higher event rates.

Figure 13: Measured and expected data transfer speed by varying the forced
trigger rate. This evaluation was conducted using a ZMQ client on a back-end
computer. The measured and expected data transfer speeds aligned well up to 32
kHz.

##  4 Summary

RFSoC technology represents a cutting-edge advancement in signal processing
and data acquisition. This paper has been dedicated to the development of
RFSoC-based front-end electronics for pulse detection, accompanied by an
extensive feasibility study. The prototype has demonstrated well-understood
frequency response, low noise ($\sim 40$ $\mu$V${}_{\textrm{rms}}$), linearity
within $\pm$2%, low crosstalk (<55 dB), and stable data transfer up to the 36
kHz trigger rate (750 Mbps). The DSP module has proven effective in correcting
the PMT overshoot. Moreover, the system’s power consumption has demonstrated a
notable advantage over the traditional FPGA + ADC system. The results of this
study provide robust evidence in favor of the feasibility and potential of
adopting the RFSoC-based approach for pulse detection. With some necessary
modifications, the front-end electronics described here hold promise for
practical implementation in the KamLAND system.

## Acknowledgments

This work was supported by JSPS KAKENHI Grant Number 19H058028, the National
Science Foundation (NSF) No. NSF-1806440, NSF-2012964, the Heising-Simons
Foundation, as well as other DOE and NSF grants to individual institutions,
U.S.-Japan Science and Technology Cooperation Program in High Energy Physics.
We would like to say thank J. Suzuki for useful discussion about RFSoC. The
authors are also grateful to all KamLAND collaborators for supporting this
effort.

## References

  * [1] L. William R, _Techniques for Nuclear and Particle Physics Experiments_.  Springer-Verlag, 1993.
  * [2] G. Knoll, _Radiation Detection and Measurement_.  John Wiley, Hoboken, NJ, 2010.
  * [3] M. Bitossi, R. Paoletti and D. Tescaro, _Ultra-Fast Sampling and Data Acquisition Using the DRS4 Waveform Digitizer_ , _IEEE Trans. Nucl. Sci._ 63 (2016) 2309–2316.
  * [4] H. Nishino et al., _The new front-end electronics for the Super-Kamiokande experiment_ , in _2007 IEEE Nuclear Science Symposium and Medical Imaging Conference_ , vol. 1, pp. 127–132, 2007.  DOI.
  * [5] M. Bellato et al., _Embedded Readout Electronics R \ & D for the Large PMTs in the JUNO Experiment_, _Nucl. Instrum. Meth. A_ 985 (2021) 164600, [2003.08339].
  * [6] Y. Abe et al., _The Waveform Digitiser of the Double Chooz Experiment: Performance and Quantisation Effects on PhotoMultiplier Tube Signals_ , _JINST_ 8 (2013) P08015, [1307.4917].
  * [7] AXEL collaboration, K. Z. Nakamura, S. Ban, A. K. Ichikawa, M. Ikeno, K. D. Nakamura, T. Nakaya et al., _Front-end-Electronics for the SiPM-readout gaseous TPC for neutrinoless double beta decay search_ , _IEEE Trans. Nucl. Sci._ 67 (2020) 1772–1776, [2001.02104].
  * [8] KamLAND collaboration, A. Gando et al., _Reactor On-Off Antineutrino Measurement with KamLAND_ , _Phys. Rev. D_ 88 (2013) 033001, [1303.4667].
  * [9] KamLAND collaboration, S. Abe et al., _Abundances of uranium and thorium elements in Earth estimated by geoneutrino spectroscopy_ , 2205.14934.
  * [10] KamLAND-Zen collaboration, A. Gando et al., _Search for Majorana Neutrinos near the Inverted Mass Hierarchy Region with KamLAND-Zen_ , _Phys. Rev. Lett._ 117 (2016) 082503, [1605.02889].
  * [11] KamLAND-Zen collaboration, S. Abe et al., _Search for the Majorana Nature of Neutrinos in the Inverted Mass Ordering Region with KamLAND-Zen_ , _Phys. Rev. Lett._ 130 (2023) 051801, [2203.02139].
  * [12] L. Stefanazzi et al., _The QICK (Quantum Instrumentation Control Kit): Readout and control for qubits and detectors_ , 2110.00557.
  * [13] K. H. Park, Y. S. Yap, Y. P. Tan, C. Hufnagel, L. H. Nguyen, K. H. Lau et al., _ICARUS-Q: A scalable RFSoC-based control system for superconducting quantum computers_ , 2112.02933.
  * [14] C. Liu, M. E. Jones and A. C. Taylor, _Characterizing the performance of high-speed data converters for RFSoC-based radio astronomy receivers_ , _Monthly Notices of the Royal Astronomical Society_ 501 (12, 2020) 5096–5104.
  * [15] “ZeroMQ.” http://zeromq.org/.