11institutetext: Universität Koblenz-Landau, Germany
11email<EMAIL_ADDRESS>22institutetext: University of Bergen, Norway
22email<EMAIL_ADDRESS>
# Revising Ontologies via Models:
The ${\cal ALC}$-formula Case

Jandson S. Ribeiro 11 Ricardo Guimarães 22 Ana Ozaki 22

###### Abstract

Most approaches for repairing description logic (DL) ontologies aim at
changing the axioms as little as possible while solving inconsistencies,
incoherences and other types of undesired behaviours. As in Belief Change,
these issues are often specified using logical formulae. Instead, in the new
setting for updating DL ontologies that we propose here, the input for the
change is given by a _model_ which we want to add or remove. The main goal is
to minimise the loss of information, without concerning with the syntactic
structure. This new setting is motivated by scenarios where an ontology is
built automatically and needs to be refined or updated. In such situations,
the syntactical form is often irrelevant and the incoming information is not
necessarily given as a formula. We define general operations and conditions on
which they are applicable, and instantiate our approach to the case of ${\cal
ALC}$-formulae.

††Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).

##  1 Introduction

Formal specifications often have to be updated either due to modelling errors
or because they have become obsolete. When these specifications are
description logic (DL) ontologies, it is possible to use one of the many
approaches to fix missing or unwanted behaviours. Usually these methods
involve the removal or replacement of formulae responsible by the undesired
aspect [28, 16, 29, 2, 20].

The problem of changing logical representations of knowledge upon the arrival
of new information is the subject matter of _Belief Change_ [13]. The theory
developed in this field provides constructions suitable for various formalisms
and applications [13, 24, 27, 23]. In most approaches for Belief Change and
for repairing ontologies, it is assumed that a set of formulae represents the
entailments to be added or removed. However, in some situations, it might be
easier to obtain this information as a _model_ instead. This idea relates with
Model Checking [3] whose main problem is to determine whether a model
satisfies a set of constraints; and with the paradigm of Learning from
Interpretations [4], where a formula needs to be created or changed so as to
have certain interpretations as part of its models and remove others from its
set of models. Example 1 illustrates the intuition behind using models as
input.

###### Example 1

Suppose that a system, which serves a university, uses an internal logical
representation of the domain with a open world behaviour and unique names. Let
${\mathcal{B}}$ be its current represention:

$\displaystyle{\mathcal{B}}=$
$\displaystyle\left\\{Professors:\\{Mary\\},Courses:\\{DL,AI\\},\right.$
$\displaystyle\qquad\left.\\{teaches:\\{(Mary,AI),(Mary,DL)\\}\right\\}.$

Assume that a user finds mistakes in the course schedule and this is caused by
the wrong information that Mary teaches the DL course. The user may lack
knowledge to define the issue formally. An alternative would be to provide the
user with an interface where one can specify, for instance, that the following
model should be accepted
$M=\\{Professors=\\{Mary\\},Courses=\\{DL,AI\\},teaches=\\{(Mary,AI)\\}\\},$
(in this model Mary does not teach the DL course). Given this input, the
system should repair itself (semi-)automatically.

We propose a new setting for Belief Change, in particular, contraction and
expansion functions which take models as input. We analyse the case of ${\cal
ALC}$-formula using quasimodels as a mean to define belief change operations.
This logic satisfies properties which facilitate the design of these
operations and it is close to ${\cal ALC}$, which is a well-studied DL.
Additionally, we identify the postulates which determine these functions and
prove that they characterise the mathematical constructions via representation
theorems. The remaining of this work is organised as follows: in Section 2 we
introduce the concepts from Belief Change which our approach builds upon and
detail the paradigm we propose here. Section 3 presents ${\cal ALC}$-formula,
the belief operations that take models as input and their respective
representation theorems. In Section 4, we highlight studies which share
similarities with our proposal and we conclude in Section 5.

##  2 Belief Change

###  2.1 The Classical Setting

Belief Change [1, 13] studies the problem of how an agent should modify its
knowledge in light of new information. In the original paradigm of Belief
Change, the AGM theory, an agent’s body of knowledge is represented as a set
of formulae closed under logical consequence, called a _belief set_ , and the
new information is represented as a single _formula_. Belief sets, however,
are not the only way for representing an agent’s body of knowledge, and
another way of representing an agent’s knowledge is via _belief bases_ :
arbitrary sets of formulae, not necessarily closed under logical consequence
[11]. In the AGM paradigm, an agent may modify its current belief base
$\mathcal{B}$ in response to a new piece of information $\varphi$ through
three kinds of operations:

Expansion:

$\operatorname{ex}(\mathcal{B},\varphi)$, simply add $\varphi$ to
${\mathcal{B}}$;

Contraction:

$\operatorname{con}(\mathcal{B},\varphi)$, reduce ${\mathcal{B}}$ so that it
does not imply $\varphi$;

Revision:

$\operatorname{rev}(\mathcal{B},\varphi)$, incorporate $\varphi$ and keep
consistency of the resulting belief base, as long as $\varphi$ is consistent.

When modifying its body of knowledge an agent should rationally modify its
beliefs conserving most of its original beliefs. This principle of minimal
change is captured in Belief Change via sets of rationality postulates. Each
of the three operations (expansion, contraction and revision) presents its own
set of rationality postulates which characterize precisely different classes
of belief change constructions. The AGM paradigm was initially proposed for
classical logics that satisfy specific requirements, dubbed AGM assumptions,
among them Tarskianicity, compactness and _deduction_. See [6, 24] for a
complete list of the AGM assumptions and a discussion on the topic. Recently,
efforts have been applied to extend Belief Change to logics that do not
satisfy such assumptions. For instance, logics that are not closed under
classical negation of formulae (such as is the case for most DLs) [24, 26],
and temporal logics and logics without compactness [21, 22, 23].

In what follows, we define _kernel contraction_ [13], one of the most studied
constructions in Belief Change and which is closely related to the most common
ways to repair ontologies. Kernel operations rely on calculating the minimal
implying sets (MinImps), also known as justifications [15] or kernels [13]. A
MinImp is a minimal subset that does entail a formula $\varphi$. The set of
all MinImps of a belief base ${\mathcal{B}}$ w.r.t. a formula $\varphi$ is
denoted by $\operatorname{MinImps}({\mathcal{B}},\varphi)$. A kernel
contraction removes from each MinImp at least one formula using an _incision
function_.

###### Definition 1

Given a set of formulae ${\mathcal{B}}$ of language $\mathcal{L}$, a function
$f$ is an incision function for ${\mathcal{B}}$ iff for all
$\varphi\in\mathcal{L}$: (i)
$f(\operatorname{MinImps}({\mathcal{B}},\varphi))\subseteq\bigcup\operatorname{MinImps}({\mathcal{B}},\varphi)$
and (ii) $f(\operatorname{MinImps}({\mathcal{B}},\varphi))\cap
X\neq\emptyset$, for all $X\in\operatorname{MinImps}({\mathcal{B}},\varphi)$.

Kernel contraction operators are built upon incision functions. The
application of an incision function to a set of MinImps is a hitting set [16,
2].

###### Definition 2

Let $\mathcal{L}$ be a language and $f$ an incision function. The _kernel
contraction_ on ${\mathcal{B}}\subseteq\mathcal{L}$ determined by $f$ is the
operation $\operatorname{con}_{f}:2^{\mathcal{L}}\times\mathcal{L}\mapsto
2^{\mathcal{L}}$ defined as:
$\operatorname{con}_{f}({\mathcal{B}},\varphi)={\mathcal{B}}\setminus
f(\operatorname{MinImps}({\mathcal{B}},\varphi))$.

Kernel contraction operations are characterised precisely by a set of
rationality postulates, as shown in the following representation theorem:

######  Theorem 2.1 ([14])

Let ${\operatorname{Cn}}$ be a consequence operator satisfying monotonicity
and compactness defined for a language $\mathcal{L}$. Then
$\operatorname{con}:2^{\mathcal{L}}\times\mathcal{L}\mapsto 2^{\mathcal{L}}$
is an operation of kernel contraction on ${\mathcal{B}}\subseteq\mathcal{L}$
iff for all sentences $\varphi\in\mathcal{L}$:

(success)

if $\varphi\not\in{\operatorname{Cn}}(\emptyset)$, then
$\varphi\not\in{\operatorname{Cn}}(\operatorname{con}({\mathcal{B}},\varphi))$,

(inclusion)

$\operatorname{con}({\mathcal{B}},\varphi)\subseteq{\mathcal{B}}$,

(core-retainment)

if $\psi\in{\mathcal{B}}\setminus\operatorname{con}({\mathcal{B}},\varphi)$,
then there is some ${\mathcal{B}}^{\prime}\subseteq{\mathcal{B}}$ such that
$\varphi\not\in{\operatorname{Cn}}({\mathcal{B}}^{\prime})$ and
$\varphi\in{\operatorname{Cn}}({\mathcal{B}}^{\prime}\cup\psi)$,

(uniformity)

if for all subsets ${\mathcal{B}}^{\prime}$ of ${\mathcal{B}}$,
$\varphi\in{\operatorname{Cn}}({\mathcal{B}}^{\prime})$ iff
$\psi\in{\operatorname{Cn}}({\mathcal{B}}^{\prime})$, then
$\operatorname{con}({\mathcal{B}},\varphi)=\operatorname{con}({\mathcal{B}},\psi)$.

###  2.2 Changing Finite Bases by Models

The Belief Change setting discussed in this section represents an epistemic
state by means of a finite base. While this essentially differ from the
traditional approach [1, 11], it aligns with the KM paradigm established by
Katsuno and Mendelzon [17]. In Section 4 we discuss other studies in Belief
Change which also take finite representability into account.

In this work, unlike the standard representation methods in Belief Change, we
consider that an incoming piece of information is represented as a finite
model. Belief Change operations defined in this format will be called model
change operations. Recall that a model $M$ is simply a structure used to give
semantics to an underlying logic language. The set of all possible models is
given by $\mathfrak{M}$. Moreover, we assume a semantic system that, for each
set of formulae ${\mathcal{B}}$ of the language $\mathcal{L}$ gives a set of
models
$\operatorname{Mod}({{\mathcal{B}}})\coloneqq\\{M\in\mathfrak{M}\mid\forall\varphi\in{\mathcal{B}}:M\models\varphi\\}$.
Let $\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$ denote the
set of all finite bases in $\mathcal{L}$.  We also say that a set of models
$\mathbb{M}$ is _finitely representable in $\mathcal{L}$_ if there is a finite
base
${\mathcal{B}}\in\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$
such that $\operatorname{Mod}({{\mathcal{B}}})=\mathbb{M}$. Additionally, if
for all $\varphi\in\mathcal{L}$ it holds that $M\models\varphi$ iff
$M^{\prime}\models\varphi$ then we write $M\equiv^{\mathcal{L}}M^{\prime}$. We
also define ${[{M}]^{\mathcal{L}}}\coloneqq\\{M^{\prime}\in\mathfrak{M}\mid
M^{\prime}\equiv^{\mathcal{L}}M\\}$.

When compared to traditional methods in Belief Change and Ontology Repair [13,
16, 2], where the incoming information comes as a single formula, our approach
receives instead a single model as input. Although, the initial body of
knowledge is represented as a finite base, the operations we define do not aim
to preserve its syntactic structure.

The first model change operation we introduce is model contraction, which
eliminates one of the models of the current base (which in Section 3 is
instantiated as an ontology). Model contraction is akin to a belief expansion,
where a formula is added to the belief set or base, reducing the set of
accepted models. The counterpart operation, model expansion, changes the base
to include a new model. This relates to belief contraction, in which a formula
is removed, and thus more models are seen as plausible.

We rewrite the rationality postulates that characterize kernel contraction
[14], considering an incoming piece of information represented as a model
instead of a single formula.

######  Definition 3 (Model Contraction)

Let $\mathcal{L}$ be a language. A function
$\operatorname{con}:\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})\times\mathfrak{M}\mapsto\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$
is a _finitely representable model contraction function_ iff for every
$\mathcal{B}\in\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$
and $M\in\mathfrak{M}$ it satisfies the following postulates:

(success)

$M\not\in\operatorname{Mod}({\operatorname{con}(\mathcal{B},M)})=\emptyset$,

(inclusion)

$\operatorname{Mod}({\operatorname{con}(\mathcal{B},M)})\subseteq\operatorname{Mod}({\mathcal{B}})$,

(retainment)

if
$M^{\prime}\in\operatorname{Mod}({\mathcal{B}})\setminus\operatorname{Mod}({\operatorname{con}(\mathcal{B},M)})$
then $M^{\prime}\equiv^{\mathcal{L}}M$,

(extensionality)

$\operatorname{con}({\mathcal{B}},M)=\operatorname{con}({\mathcal{B}},M^{\prime})$,
if $M\equiv^{\mathcal{L}}M^{\prime}$.

We might also need to add a model to the set of models of the current base.
This addition relates to classical contractions in Belief Change, which
_reduces_ the belief base.

######  Definition 4 (Model Expansion)

Let $\mathcal{L}$ be a language. A function
$\operatorname{ex}:\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})\times\mathfrak{M}\mapsto\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$
is a _finitely representable model expansion_ iff for every
${\mathcal{B}}\in\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$
and $M\in\mathfrak{M}$ it satisfies the postulates:

(success)

$M\in\operatorname{Mod}({\operatorname{ex}({\mathcal{B}},M)}),$

(persistence)

$\operatorname{Mod}({{\mathcal{B}}})\subseteq\operatorname{Mod}({\operatorname{ex}({\mathcal{B}},M)}),$

(vacuity)

$\operatorname{Mod}({\operatorname{ex}({\mathcal{B}},M)})=\operatorname{Mod}({{\mathcal{B}}}),$
if $M\in\operatorname{Mod}({{\mathcal{B}}})$,

(extensionality)

$\operatorname{ex}({\mathcal{B}},M)=\operatorname{ex}({\mathcal{B}},M^{\prime})$,
if $M\equiv^{\mathcal{L}}M^{\prime}$.

###### Definition 5

Let $\mathcal{L}$ be a language and ${\operatorname{Cn}}$ a Tarskian
consequence operator defined over $\mathcal{L}$. Also let $\mathfrak{M}$ be a
fixed set of models. We say that a triple
${\Lambda}=(\mathcal{L},{\operatorname{Cn}},\mathfrak{M})$ is an _ideal
logical system_ if the following holds.

  * •

For every ${\mathcal{B}}\subseteq\mathcal{L}$ and $\varphi\in\mathcal{L}$,
${\mathcal{B}}\models\varphi$ (i.e.
$\varphi\in{\operatorname{Cn}}({\mathcal{B}})$) iff
$\operatorname{Mod}({{\mathcal{B}}})\subseteq\operatorname{Mod}({\varphi})$.

  * •

For each $\mathbb{M}\subseteq\mathfrak{M}$ there is a finite set of formulae
${\mathcal{B}}$ such that $\operatorname{Mod}({{\mathcal{B}}})=\mathbb{M}$.

If ${\Lambda}=(\mathcal{L},{\operatorname{Cn}},\mathfrak{M})$ is an ideal
logical system, we can define a function
${\operatorname{FR}}_{\Lambda}:2^{\mathfrak{M}}\mapsto\operatorname{\operatorname{\mathcal{P}}_{fin}}(\mathcal{L})$
and such that
$\operatorname{Mod}({{\operatorname{FR}}(\mathbb{M})})=\mathbb{M}$. Then, we
can define model contraction as
$\operatorname{con}({\mathcal{B}},M)={\operatorname{FR}}(\operatorname{Mod}({{\mathcal{B}}})\setminus{[{M}]^{\mathcal{L}}})$
and expansion as
$\operatorname{ex}({\mathcal{B}},M)={\operatorname{FR}}(\operatorname{Mod}({{\mathcal{B}}})\cup{[{M}]^{\mathcal{L}}})$.
The first condition in Definition 5 implies that there is a connection between
the models satisfied and the logical consequences of the base obtained and the
second ensures that the result always exists. An example that fits these
requirements is to consider classical propositional logic with a finite
signature $\Sigma$, together with its usual consequence operator and models.
In this situation, we can define ${\operatorname{FR}}_{prop}$ as follows:

${\operatorname{FR}}_{prop}(\mathbb{M})=\bigvee_{M\in\mathbb{M}}\left(\bigwedge_{a\in\Sigma\mid
M\models a}a\land\bigwedge_{a\in\Sigma\mid M\models\neg{a}}\neg{a}\right).$

Next, we show that the construction proposed with ${\operatorname{FR}}$ has
the properties stated in Definitions 3 and 4.

###### Theorem 2.2

Let $(\mathcal{L},{\operatorname{Cn}},\mathfrak{M})$ be an ideal logical
system as in Definition 5. Then
$\operatorname{iCon}({\mathcal{B}},M)\coloneqq{\operatorname{FR}}\left(\operatorname{Mod}({{\mathcal{B}}})\setminus{[{M}]^{\mathcal{L}}}\right)$
satisfies the postulates in Definition 3.

###### Proof

Definition 5 ensures that the result exists and that $M\models\varphi$, for
all $\varphi\in\Lambda$, giving us success. By construction we do gain models,
thus we have inclusion. If $M\equiv^{\mathcal{L}}M^{\prime}$, then
${[{M}]^{\mathcal{L}}}={[{M^{\prime}}]^{\mathcal{L}}}$, thus extensionality is
satisfied. Also, if
$M^{\prime}\in\operatorname{Mod}({\varphi})\setminus\operatorname{Mod}({\operatorname{iCon}(\varphi,M)})$
then $M^{\prime}\in{[{M}]^{\mathcal{L}}}$, hence the operation satisfies
retainment.

###### Theorem 2.3

Let $(\mathcal{L},{\operatorname{Cn}},\mathfrak{M})$ be an ideal logical
system as in Definition 5. Then
$\operatorname{iExp}({\mathcal{B}},M)\coloneqq{\operatorname{FR}}\left(\operatorname{Mod}({{\mathcal{B}}})\cup{[{M}]^{\mathcal{L}}}\right)$
satisfies the postulates in Definition 4.

###### Proof

Definition 5 ensures that the result exists and that $M\models\varphi$, for
all $\varphi\in\Lambda$, giving us success. Due to the first condition in
Definition 5 we gain vacuity: if $M\in\operatorname{Mod}({{\mathcal{B}}})$,
then there will be no changes in the accepted models. By construction we do
not lose models, thus we have persistance. Extensionality also holds because
whenever $M\equiv^{\mathcal{L}}M^{\prime}$ we have then
${[{M}]^{\mathcal{L}}}={[{M^{\prime}}]^{\mathcal{L}}}$.

A revision operation incorporates new formulae, and removes potential
conflicts in behalf of consistency. In our setting, incorporating information
coincides with model contraction which could lead to an inconsistent belief
state. In this case, model revision could be interpreted as a conditional
model contraction: in some cases the removal might be rejected to preserve
consistency. We leave the study on revision as a future work.

##  3 The case of $\mathcal{ALC}$-formula

The logic $\mathcal{ALC}$-formula corresponds to the DL $\mathcal{ALC}$
enriched with boolean operators over ${\cal ALC}$ axioms. As discussed in
Section 2.2, in finite representable logics, such as the classical
propositional logics, we can easily add and remove models while keeping the
representation finite. For ${\cal ALC}$-formula, however, it is not possible
to uniquely add or remove a new model $M$ since, for instance, the language
does not distinguish quantities (e.g., a model $M$ and another model that has
two duplicates of $M$).

Even if quantities are disregarded and our input is a class of models
indistinguishable by ${\cal ALC}$-formulae, there are sets of formulae in this
language that are not finitely representable. As for instance in the following
infinite set: $\\{C\sqsubseteq\exists r^{n}.\top\mid n\in\mathbb{N}^{>0}\\}$,
where $\exists r^{n+1}.\top$ is a shorthand for $\exists r.(\exists
r^{n}.\top)$ and $\exists r^{1}.\top\coloneqq\exists r.C$. As a workaround for
the ${\cal ALC}$-formula case, we propose a new strategy based on the
translation of $\mathcal{ALC}$-formulae into DNF.

###  3.1 ${\cal ALC}$-formulae and Quasimodels

Let ${\sf N_{C}}$, ${\sf N_{R}}$ and ${\sf N_{I}}$ be countably infinite and
pairwise disjoint sets of concept names, role names, and individual names,
respectively. ${\cal ALC}$ _concepts_ are built according to the rule:
$C::=A\mid\neg C\mid(C\sqcap C)\mid\exists r.C$, where $A\in{\sf N_{C}}$ and
$r\in{\sf N_{R}}$. ${\cal ALC}$-_formulae_ are defined as expressions $\phi$
of the form

$\phi::=\alpha\mid\neg(\phi)\mid(\phi\wedge\phi)\quad\quad\alpha::=C(a)\mid
r(a,b)\mid(C=\top),$

where $C$ is an ${\cal ALC}$ concept, $a,b\in{\sf N_{I}}$, and $r\in{\sf
N_{R}}$111 We may omit parentheses if there is no risk of confusion. The usual
concept inclusions $C\sqsubseteq D$ can be expressed with $\top\sqsubseteq\neg
C\sqcup D$ and $\neg C\sqcup D\sqsubseteq\top$, which is $(\neg C\sqcup
D=\top)$.. Denote by ${\sf ind}(\varphi)$ the set of all individual names
occurring in an ${\cal ALC}$-formula $\varphi$.

The semantics of ${\cal ALC}$-formulae and the definitions related to
quasimodels are standard [8, page 70]. In what follows, we reproduce the
essential definitions and results for this work. Let $\varphi$ be an ${\cal
ALC}$-formula. Let ${\sf f}(\varphi)$ and ${\sf c}(\varphi)$ be the set of all
subformulae and subconcepts of $\varphi$ closed under single negation,
respectively.

###### Definition 6

A _concept type_ for $\varphi$ is a subset ${\mathbf{c}}\subseteq{\sf
c}(\varphi)$ such that:

  1. 1.

$D\in{\mathbf{c}}$ iff $\neg D\not\in{\mathbf{c}}$, for all $D\in{\sf
c}(\varphi)$;

  2. 2.

$D\sqcap E\in{\mathbf{c}}$ iff $\\{D,E\\}\subseteq{\mathbf{c}}$, for all
$D\sqcap E\in{\sf c}(\varphi)$.

###### Definition 7

A _formula type_ for $\varphi$ is a subset ${\mathbf{f}}\subseteq{\sf
f}(\varphi)$ such that:

  1. 1.

$\phi\in{\mathbf{f}}$ iff $\neg\phi\not\in{\mathbf{f}}$, for all $\phi\in{\sf
f}(\varphi)$;

  2. 2.

$\phi\wedge\psi\in{\mathbf{f}}$ iff $\\{\phi,\psi\\}\subseteq{\mathbf{f}}$,
for all $\phi\wedge\psi\in{\sf f}(\varphi)$.

We may omit ‘for $\varphi$’ if this is clear from the context. A _model
candidate_ for $\varphi$ is a triple $(T,o,{\mathbf{f}})$ such that $T$ is a
set of concept types, $o$ is a function from ${\sf ind}(\varphi)$ to $T$,
${\mathbf{f}}$ a formula type, and $(T,o,{\mathbf{f}})$ satisfies the
conditions: $\varphi\in{\mathbf{f}}$; $C(a)\in{\mathbf{f}}$ implies $C\in
o(a)$; $r(a,b)\in{\mathbf{f}}$ implies $\\{\neg C\mid\neg\exists r.C\in
o(a)\\}\subseteq o(b)$.

######  Definition 8 (Quasimodel)

A model candidate $(T,o,{\mathbf{f}})$ for $\varphi$ is a _quasimodel_ for
$\varphi$ if the following holds

  * •

for every concept type ${\mathbf{c}}\in T$ and every $\exists
r.D\in{\mathbf{c}}$, there is ${\mathbf{c}}^{\prime}\in T$ such that
$\\{D\\}\cup\\{\neg E\mid\neg\exists
r.E\in{\mathbf{c}}\\}\subseteq{\mathbf{c}}^{\prime}$;

  * •

for every concept type ${\mathbf{c}}\in T$ and every concept $C$, if $\neg
C\in{\mathbf{c}}$ then this implies $(C=\top)\not\in{\mathbf{f}}$;

  * •

for every concept $C$, if $\neg(C=\top)\in{\mathbf{f}}$ then there is
${\mathbf{c}}\in T$ such that $C\not\in{\mathbf{c}}$;

  * •

$T$ is not empty.

Theorem 3.1 motivates the decision of using quasimodels to implement our
operations for finite bases described in ${\cal ALC}$-formulae.

######  Theorem 3.1 (Theorem 2.27 [8])

An $\mathcal{ALC}$-formula $\varphi$ is satisfiable iff there is a quasimodel
for $\varphi$.

###  3.2 ${\cal ALC}$-formulae in Disjunctive Normal Form

Next, we propose a translation method which converts an ${\cal ALC}$-formula
into a disjunction of conjunctions of (possibly negated) atomic formulae.  Let
${\sf S}(\varphi)$ be the set of all quasimodels for $\varphi$. We We define
$\varphi^{\dagger}$ as

$\bigvee_{(T,o,{\mathbf{f}})\in{\sf
S}(\varphi)}(\bigwedge_{\alpha\in{\mathbf{f}}}\alpha\wedge\bigwedge_{\neg\alpha\in{\mathbf{f}}}\neg\alpha).$

where $\alpha$ is of the form $(C=\top),C(a),r(a,b)$.

Theorem 3.2 confirms the equivalence between a formula and its translation
into DNF. As downside, the translation can be potentially exponentially larger
than the original formula.

######  Theorem 3.2 ()

For every ${\cal ALC}$-formula $\varphi$, we have that
$\varphi\equiv\varphi^{\dagger}$.

In the next subsections, we present finite base model change operations for
${\cal ALC}$-formulae, i.e., functions from
$\mathcal{L}\times\mathfrak{M}\mapsto\mathcal{L}$. We can represent the body
of knowledge as a single formula because every finite belief base of ${\cal
ALC}$-formulae can be represented by the conjunction of its elements. We use
our translation to add models in a “minimal” way by _adding disjuncts_ , while
removing a model amounts to _removing disjuncts_. We also need to obtain a
model candidate relative to our translated formula, as show in Definition 9.

######  Definition 9 ([8])

Let $\mathcal{I}$ be an interpretation and $\varphi$ an ${\cal ALC}$-formula
formula. The quasimodel of $\mathcal{I}$ w.r.t. $\varphi$, symbols
$\operatorname{qm}({\varphi},{\mathcal{I}})=(T,o,{\mathbf{f}})$, is

  * •

$T\coloneqq\\{c(x)\mid x\in\Delta^{\mathcal{I}}\\}$, where $c(x)=\\{C\in{\sf
c}(\varphi)\mid x\in C^{\mathcal{I}}\\}$,

  * •

$o(a)\coloneqq c(a^{\mathcal{I}})$, for all $a\in{\sf ind}(\varphi)$,

  * •

${\mathbf{f}}\coloneqq\\{\psi\in{\sf
f}(\varphi)\mid\mathcal{I}\models\psi\\}.$

###  3.3 Model Contraction for $\mathcal{ALC}$-formulae

We define model contraction for $\mathcal{ALC}$-formulae using the notion of
quasimodels discussed previously and a correspondence between models and
quasimodels.

We use the following operator, denoted $\operatorname{\mu}$, to define model
contraction in Definition 10. Let $\varphi$ be an ${\cal ALC}$-formula and let
$M$ be a model. Then,

$\operatorname{\mu}(\varphi,M)=\operatorname{ftypes}({\varphi})\setminus\\{{\mathbf{f}}\\},\mbox{
where }qm(\varphi,M)=(T,o,{\mathbf{f}})$

and $\operatorname{ftypes}({\varphi})$ is the set of all formula types in all
quasimodels for $\varphi$, that is:

$\operatorname{ftypes}({\varphi})=\\{{\mathbf{f}}\mid(T,o,{\mathbf{f}})\in{\sf
S}(\varphi)\\}.$

Let $lit({\mathbf{f}})\coloneqq\\{\ell\in{\mathbf{f}}\mid\ell\mbox{ is a
literal }\\}$ be the set of all literals in a formula type ${\mathbf{f}}$.

###### Definition 10

A _finite base model contraction function_ is a function
$\operatorname{con}:\mathcal{L}\times\mathfrak{M}\mapsto\mathcal{L}$ such that

$\displaystyle\operatorname{con}(\varphi,M)$
$\displaystyle{=}\left\\{\begin{array}[]{cl}\bigvee\limits_{{\mathbf{f}}\in\operatorname{\mu}(\varphi,M)}\bigwedge
lit({\mathbf{f}}),&\mbox{if }M\models\varphi\mbox{ and
}\operatorname{\mu}(\varphi,M)\neq\emptyset\\\ \bot&\mbox{if
}M\models\varphi\mbox{ and }\operatorname{\mu}(\varphi,M)=\emptyset\\\
\varphi&\mbox{otherwise}.\end{array}\right.$

As we see later in this Section, there are models $M,M^{\prime}$ such that
$M{\not\equiv}^{\mathcal{L}}M^{\prime}$ but our operations based on
quasimodels cannot distinguish them. Given ${\cal ALC}$-formulae
$\varphi,\psi$, we say that $\psi$ is _in the language of the literals of
$\varphi$_, written $\psi\in{\mathcal{L}_{lit}({\varphi})}$, if $\psi$ is a
boolean combination of the atoms in $\varphi$. Our operations partition the
models according to this restricted language. We write
$M\equiv^{\varphi}M^{\prime}$ instead of
$M\equiv^{\mathcal{L}_{lit}({\varphi})}M^{\prime}$, and ${{[{M}]^{\varphi}}}$
instead of $[M]^{\mathcal{L}_{lit}({\varphi})}$ for conciseness.

######  Theorem 3.3 ()

Let $M$ be a model and $\varphi$ an ${\cal ALC}$-formula. A finite base model
function $\operatorname{con}^{*}(\varphi,M)$ is equivalent to
$\operatorname{con}(\varphi,M)$ iff $\operatorname{con}^{*}$ satisfies:

(success)

$M\not\models\operatorname{con}^{*}(\varphi,M)$,

(inclusion)

$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})\subseteq\operatorname{Mod}({\varphi})$,

(atomic retainment):

For all $\mathbb{M}^{\prime}\subseteq\mathfrak{M}$, if
$\operatorname{Mod}({\operatorname{con}^{*}({\mathcal{B}},{M})})\subset\mathbb{M}^{\prime}\subseteq\operatorname{Mod}({{\mathcal{B}}})\setminus{{[{{M}}]^{\varphi}}}$
then $\mathbb{M}^{\prime}$ is not finitely representable in ${\cal
ALC}$-formula.

(atomic extensionality)

if $M^{\prime}\equiv^{\varphi}M$ then

$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})=\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M^{\prime})}).$

The postulate of success guarantees that $M$ will be indeed relinquished,
while inclusion imposes that no model will be gained during a contraction
operation. Recall that in order to guarantee finite representability, it might
be necessary to remove $M$ jointly with other models. The postulate atomic
retainmentcaptures a notion of minimal change, dictating which models are
allowed to be removed together with $M$.

On the other hand, atomic extensionality imposes that if two models $M$ and
$M^{\prime}$ satisfy the same formulae within the literals of the current
knowledge base $\varphi$, then they should present the same result.

A simpler way of implementing model contraction, also using the notion of a
quasimodel,

###### Definition 11

Let $\varphi$ be an ${\cal ALC}$-formula and $M$ a model. Also, let
$(T,o,{\mathbf{f}})=\operatorname{qm}({\varphi},{M})$. The function
$\operatorname{con}_{s}(\varphi,M)$ is defined follows:

$\displaystyle\operatorname{con}_{s}(\varphi,M)=\left\\{\begin{array}[]{cl}\varphi\land\neg(\bigwedge
lit({\mathbf{f}}))&\text{if }M\models\varphi\\\
\varphi&\text{otherwise.}\end{array}\right.$

Example 2 illustrates how $\operatorname{con}_{s}$ works.

###### Example 2

Consider the following ${\cal ALC}$-formula and interpretation $M$:

$\displaystyle\varphi\coloneqq$ $\displaystyle P(Mary)\land C(DL)\land
C(AI)\land\left((teaches(Mary,DL)\right.\land$
$\displaystyle\left.\neg{teaches(Mary,AI)})\lor(\neg{teaches(Mary,DL)}\land
teaches(Mary,AI))\right)$

and $M=(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$, where
$\Delta^{\mathcal{I}}=\\{m,d,a\\}$, $C^{\mathcal{I}}=\\{d,a\\}$,
$P^{\mathcal{I}}=\\{m\\}$, $teaches^{\mathcal{I}}=\\{(m,d)\\}$,
$Mary^{\mathcal{I}}=m$, $AI^{\mathcal{I}}=a$, and $DL^{\mathcal{I}}=d$. Assume
we want to remove $M$ from $\operatorname{Mod}({\varphi})$. Let
$\operatorname{qm}({\varphi},{M})=(T,o,{\mathbf{f}})$. Thus,

$\displaystyle lit({\mathbf{f}})$ $\displaystyle=\\{\neg
teaches(m,a),teaches(m,d),C(d),C(a),P(m)\\}$
$\displaystyle\operatorname{con}_{s}(\varphi,M)$
$\displaystyle=\varphi\land\neg\bigwedge lit({\mathbf{f}})$
$\displaystyle=\varphi\land\neg\left(\neg teaches(m,a)\land teaches(m,d)\land
C(d)\land C(a)\land P(m)\right).$

Both model contraction operations $\operatorname{con}$ and
$\operatorname{con}_{s}$ are equivalent.

######  Theorem 3.4 ()

For every ${\cal ALC}$-formula $\varphi$ and model $M$,
$\operatorname{con}(\varphi,M){\equiv}\operatorname{con}_{s}(\varphi,M)$.

###  3.4 Model Expansion in $\mathcal{ALC}$-formulae

In this section, we investigate model expansion for ${\cal ALC}$-formulae.
Recall that we assume that a knowledge base is represented as a single ${\cal
ALC}$-formula $\varphi$. Expansion consists in adding an input model $M$ to
the current knowledge base $\varphi$ with the requirement that the new
epistemic state can be represented also as a finite formula.

###### Definition 12

Given a quasimodel $(T,o,{\mathbf{f}})$, we write
$\bigwedge(T,o,{\mathbf{f}})$ as a short-cut for $\bigwedge
lit({\mathbf{f}})$. A _finite base model expansion_ is a function
$\operatorname{ex}:\mathcal{L}\times\mathfrak{M}\to\mathcal{L}$ s.t.:

$\displaystyle\operatorname{ex}(\varphi,M)$
$\displaystyle=\left\\{\begin{array}[]{cl}\varphi&\mbox{if }M\models\varphi\\\
\varphi\lor\bigwedge qm(\neg\varphi,M)&\mbox{otherwise}.\end{array}\right.$

Example 3 illustrates how $\operatorname{ex}$ works.

###### Example 3

Consider the interpretation $M$ from Example 2 and

$\varphi\coloneqq P(Mary)\land C(DL)\land C(AI)\land
teaches(Mary,AI)\land\neg{teaches(Mary,DL)}.$

Assume we want to add $M$ to $\operatorname{Mod}({\varphi})$ and
$qm(\neg\varphi,M)=(T,o,{\mathbf{f}})$. Thus,

$\displaystyle lit({\mathbf{f}})$ $\displaystyle=\\{\neg
teaches(m,a),teaches(m,d),C(d),C(a),P(m)\\}$
$\displaystyle\operatorname{ex}(\varphi,M)$
$\displaystyle=\varphi\lor\bigwedge lit({\mathbf{f}})$
$\displaystyle=\varphi\lor\left(\neg teaches(m,a)\land teaches(m,d)\land
C(d)\land C(a)\land P(m)\right).$

The operation ‘$\operatorname{ex}$’ maps a current knowledge base represented
as a single formula $\varphi$ and maps it to a new knowledge base that is
satisfied by the input model $M$. The intuition is that ‘$\operatorname{ex}$’
modifies the current knowledge base only if $M$ does not satisfy $\varphi$.
This modification is carried out by making a disjunct of $\varphi$ with a
formula $\psi$ that is satisfied by $M$. This guarantees that $M$ is present
in the new epistemic state and that models of $\varphi$ are not discarded. The
trick is to find such an appropriate formula $\psi$ which is obtained by
taking the conjunction of all the literals within the quasimodel
$qm(\neg\varphi,M)$. Here, the quasimodel needs to be centred on $\neg\varphi$
because $M\not\models\varphi$, and therefore it is not possible to construct a
quasimodel based on $M$ centred on $\varphi$. As discussed in the prelude of
this section, this strategy not only adds $M$ to the new knowledge base but
also the whole equivalence class modulo the literals of $\varphi$.

######  Lemma 1 ()

For every ${\cal ALC}$-formula $\varphi$ and model $M$:

$\displaystyle\operatorname{Mod}({\operatorname{ex}(\varphi,M)})=\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}.$

Actually, any operation that adds precisely the equivalence class of $M$
modulo the literals is equivalent to ‘$\operatorname{ex}$’. In the following,
we write $\operatorname{ex}^{*}(\varphi,M)$ to refer to an arbitrary finite
base expansion function of the form
$\operatorname{ex}^{*}:\mathcal{L}\times\mathfrak{M}\mapsto\mathcal{L}$.

######  Theorem 3.5 ()

For every $\operatorname{ex}^{*}$, if
$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,M)})=\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}$
then

  * (i) $\operatorname{ex}^{*}(\varphi,M)\equiv\varphi$, if $M\models\varphi$; and

  * (ii) $\operatorname{ex}^{*}(\varphi,M)\equiv\varphi\lor\bigwedge qm(\neg\varphi,M)$, if $M\not\models\varphi$.

Our next step is to investigate the rationality of ‘$\operatorname{ex}^{*}$’.
As expected adding the whole equivalence class of $M$ with respect to
${\mathcal{L}_{lit}({\varphi})}$ does not come freely, and some rationality
postulates are captured, while others are lost:

######  Theorem 3.6 ()

Let $M$ be a model and $\varphi$ an ${\cal ALC}$-formula. A finite base model
function $\operatorname{ex}^{*}(\varphi,M)$ is equivalent to
$\operatorname{ex}(\varphi,M)$ iff $\operatorname{ex}^{*}$ satisfies:

(success)

${M}\in\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$.

(persistence):

$\operatorname{Mod}({\varphi})\subseteq\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$.

(atomic temperance):

For all $\mathbb{M}^{\prime}\subseteq\mathfrak{M}$, if
$\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}\subseteq\mathbb{M}^{\prime}\subset\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})\cup\\{{M}\\}$
then $\mathbb{M}^{\prime}$ is not finitely representable in ${\cal
ALC}$-formula.

(atomic extensionality)

if $M^{\prime}\equiv^{\varphi}M$ then

$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,M)})=\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,M^{\prime})}).$

The postulates success and persistence come from requiring that $M$ will be
absorbed, and that models will not be lost during an expansion. The atomic
extensionality postulate states that if two models satisfy exactly the same
literals within $\varphi$, then they should present the same results. Atomic
temperance captures a principle of minimality and guarantees that when adding
$M$, the loss of information should be minimised. Precisely, the only formulae
allowed to be given up are those that are incompatible with $M$ modulo the
literals of $\varphi$. Lemma 1 and Theorem 3.6 prove that the
‘$\operatorname{ex}$’ operation is characterized by the postulates: success,
persistence, atomic temperance and atomic extensionality.

##  4 Related Work

In the foundational paradigm of Belief Change, the AGM theory, bases have been
used in the literature with two main purposes: as a finite representation of
the knowledge of an agent [19, 5], and as a way of distinguishing agents
knowledge explicitly [11]. Even though the AGM theory cannot be directly
applied to DLs because most of these logics do not satisfy the prerequisites
known as the AGM-assumptions [7], it has been studied and adapted to DLs [6,
25].

The syntactic connectivity in a knowledge base has a strong consequence of how
an agent should modify its knowledge [13]. This sensitivity to syntax is also
present in Ontology Repair and Evolution. Classical approaches preserve the
syntactic form of the ontology as much as possible [16, 28]. However, these
approaches may lead to drastic loss of information, as noticed by Hansson
[10]. This problem has been studied in Belief Change for pseudo-contraction
[27]. In the same direction, Troquard et al. [29] proposed the repair of DL
ontologies by weakening axioms using refinement operators. Building on this
study, Baader et al. [2] devised the theory of _gentle repairs_ , which also
aims at keeping most of the information within the ontology upon repair. In
fact, gentle repairs are closely related to pseudo-contractions [18].

Other remarkable works in Belief Change in which the body of knowledge is
represented in a finite way include the formalisation of revision due to
Katsuno and Mendelzon [17] and the base-generated operations by Hansson [12].
In the former, Katsuno and Mendelzon [17] formalise traditional belief
revision operations using a single formula to represent the whole belief set.
This is possible because they only consider finitary propositional languages.
Hansson provides a characterisation of belief change operations over finite
bases but restricted for logics which satisfy all the AGM-assumptions (such as
propositional classical logic). Guerra and Wassermann [9] develop operations
for rational change where an agent’s knowledge or behaviour is given by a
Kripke model. They also provide two characterisations with AGM-style
postulates.

##  5 Conclusion and Future Work

In this work, we have introduced a new kind of belief change operation: belief
change via models. In our approach, an agent is confronted with a new piece of
information in the format of a finite model, and it is compelled to modify its
current epistemic state, represented as a single finite formula, either
incorporating the new model, called model expansion; or removing it, called
model contraction. The price for such finite representation is that the single
input model cannot be removed or added alone, and some other models must be
added or removed as well. As future work, we will investigate model change
operations in other DLs, still taking into account finite representability. We
will also explore the effects of relaxing some constraints on Belief Base
operations, allowing us to rewrite axioms with different levels of
preservation in the spirit of Pseudo-Contractions, Gentle Repairs, and Axiom
Weakening.

## Acknowledgements

Part of this work has been done in the context of CEDAS (Center for Data
Science, University of Bergen, Norway). The first author is supported by the
German Research Association (DFG), project number 424710479. Ozaki is
supported by the Norwegian Research Council, grant number 316022.

## References

  * Alchourrón et al. [1985] Carlos E. Alchourrón, Peter Gärdenfors, and David Makinson.  On the Logic of Theory Change: Partial Meet Contraction and Revision Functions.  _Journal of Symbolic Logic_ , 50(2):510–530, 1985\.
  * Baader et al. [2018] Franz Baader, Francesco Kriegel, Adrian Nuradiansyah, and Rafael Peñaloza.  Making Repairs in Description Logics More Gentle.  In _Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning, KR 2018_. AAAI Press, 2018.
  * Clarke et al. [1986] Edmund M. Clarke, E. Allen Emerson, and Aravinda P. Sistla.  Automatic verification of finite-state concurrent systems using temporal logic specifications.  _ACM Transactions on Programming Languages and Systems_ , 8(2):244–263, apr 1986.  doi: 10.1145/5397.5399.
  * De Raedt [1997] Luc De Raedt.  Logical settings for concept-learning.  _Artificial Intelligence_ , 95(1):187–201, aug 1997.  doi: 10.1016/s0004-3702(97)00041-6.
  * Dixon and Wobcke [1993] Simon Dixon and Wayne Wobcke.  The Implementation of a First-Order Logic AGM Belief Revision System.  In _Proceedings of the 5th International Conference on Tools with Artificial Intelligence, ICTAI 1993_ , pages 40–47. IEEE Computer Society, 1993.  doi: 10.1109/TAI.1993.633934.
  * Flouris [2006] Giorgos Flouris.  _On Belief Change and Ontology Evolution_.  PhD thesis, University of Crete, 2006.
  * Flouris et al. [2005] Giorgos Flouris, Dimitris Plexousakis, and Grigoris Antoniou.  On Applying the AGM Theory to DLs and OWL.  In _The Semantic Web – ISWC 2005_ , pages 216–231. Springer Berlin Heidelberg, 2005.  doi: 10.1007/11574620_18.
  * Gabbay [2003] Dov Gabbay.  _Many-dimensional modal logics : theory and applications_.  Elsevier North Holland, Amsterdam Boston, 2003.  ISBN 0444508260.
  * Guerra and Wassermann [2019] Paulo T. Guerra and Renata Wassermann.  Two AGM-style characterizations of model repair.  _Ann. Math. Artif. Intell._ , 87(3):233–257, 2019\.  doi: 10.1007/s10472-019-09656-4.
  * Hansson [1993] Sven Ove Hansson.  Changes of disjunctively closed bases.  _Journal of Logic, Language and Information_ , 2(4):255–284, oct 1993.  doi: 10.1007/bf01181682.
  * Hansson [1994] Sven Ove Hansson.  Taking Belief Bases Seriously.  In _Logic and Philosophy of Science in Uppsala: Papers from the 9th International Congress of Logic, Methodology and Philosophy of Science_ , pages 13–28. Springer Netherlands, Dordrecht, 1994.  ISBN 978-94-015-8311-4.
  * Hansson [1996] Sven Ove Hansson.  Knowledge-Level Analysis of Belief Base Operations.  _Artificial Intelligence_ , 82(1-2):215–235, 1996\.  doi: 10.1016/0004-3702(95)00005-4.
  * Hansson [1999] Sven Ove Hansson.  _A Textbook of Belief Dynamics: Theory Change and Database Updating_.  Applied Logic Series. Kluwer Academic Publishers, 1999.
  * Hansson and Wassermann [2002] Sven Ove Hansson and Renata Wassermann.  Local Change.  _Studia Logica_ , 70(1):49–76, 2002.
  * Horridge [2011] Matthew Horridge.  _Justification based explanation in ontologies_.  PhD thesis, University of Manchester, 2011.
  * Kalyanpur [2006] Aditya Kalyanpur.  _Debugging and repair of OWL ontologies_.  PhD thesis, University of Maryland, 2006.
  * Katsuno and Mendelzon [1991] Hirofumi Katsuno and Alberto O. Mendelzon.  Propositional knowledge base revision and minimal change.  _Artificial Intelligence_ , 52(3):263–294, dec 1991.
  * Matos et al. [2019] Vinícius Bitencourt Matos, Ricardo Guimarães, Yuri David Santos, and Renata Wassermann.  Pseudo-contractions as Gentle Repairs.  In _Lecture Notes in Computer Science_ , pages 385–403. Springer International Publishing, 2019.  doi: 10.1007/978-3-030-22102-7_18.
  * Nebel [1991] Bernhard Nebel.  Belief Revision and Default Reasoning: Syntax-Based Approaches.  In _Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning, KR 1991_ , pages 417–428. Morgan Kaufmann, 1991.
  * Ozaki and Peñaloza [2018] Ana Ozaki and Rafael Peñaloza.  Consequence-Based Axiom Pinpointing.  In _Proceedings of the 12th International Conference on Scalable Uncertainty Management, SUM 2018_ , volume 11142 of _Lecture Notes in Computer Science_ , pages 181–195. Springer, 2018.
  * Ribeiro et al. [2018] Jandson S. Ribeiro, Abhaya Nayak, and Renata Wassermann.  Towards Belief Contraction without Compactness.  In _Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning, KR 2018_ , pages 287–296. AAAI Press, 2018.
  * Ribeiro et al. [2019a] Jandson S. Ribeiro, Abhaya Nayak, and Renata Wassermann.  Belief Update without Compactness in Non-finitary Languages.  In _Proceedings of the 28th International Joint Conference on Artificial Intelligence, IJCAI 2019_ , pages 1858–1864. ijcai.org, 2019a.
  * Ribeiro et al. [2019b] Jandson S. Ribeiro, Abhaya Nayak, and Renata Wassermann.  Belief Change and Non-Monotonic Reasoning Sans Compactness.  In _Proceedings of the 33rd AAAI Conference on Artificial Intelligence, AAAI 2019_ , pages 3019–3026. AAAI Press, 2019b.
  * Ribeiro [2013] Márcio Moretto Ribeiro.  _Belief Revision in Non-Classical Logics_.  Springer London, 2013.  doi: 10.1007/978-1-4471-4186-0.
  * Ribeiro and Wassermann [2008] Márcio Moretto Ribeiro and Renata Wassermann.  Base revision for ontology debugging.  _Journal of Logic and Computation_ , 19(5):721–743, sep 2008.  doi: 10.1093/logcom/exn048.
  * Ribeiro and Wassermann [2014] Márcio Moretto Ribeiro and Renata Wassermann.  Minimal Change in AGM Revision for Non-Classical Logics.  In _Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning, KR 2014_. AAAI Press, 2014.
  * Santos et al. [2018] Yuri David Santos, Vinícius Bitencourt Matos, Márcio Moretto Ribeiro, and Renata Wassermann.  Partial meet pseudo-contractions.  _International Journal of Approximate Reasoning_ , 103:11–27, dec 2018.  doi: 10.1016/j.ijar.2018.08.006.
  * Suntisrivaraporn [2009] Boontawee Suntisrivaraporn.  _Polynomial time reasoning support for design and maintenance of large-scale biomedical ontologies_.  PhD thesis, Dresden University of Technology, Germany, 2009.
  * Troquard et al. [2018] Nicolas Troquard, Roberto Confalonieri, Pietro Galliani, Rafael Peñaloza, Daniele Porello, and Oliver Kutz.  Repairing Ontologies via Axiom Weakening.  In _Proceedings of the 22nd AAAI Conference on Artificial Intelligence, AAAI 2018_ , pages 1981–1988. AAAI Press, 2018.

##  Appendix 0.A Proofs for Section 3

We have already given the syntax of ${\cal ALC}$-formulae in the main text and
we provide the semantics here for the convenience of the reader. The semantics
is given by interpretations. As usual, an interpretation $\mathcal{I}$ is a
pair $(\Delta^{\mathcal{I}},\cdot^{\mathcal{I}})$ where $\Delta^{\mathcal{I}}$
is a countable non-empty set, called the _domain of invidivuals_ , and
$\cdot^{\mathcal{I}}$ is a function mapping each concept name $A\in{\sf
N_{C}}$ to a subset $A^{\mathcal{I}}$ of $\Delta^{\mathcal{I}}$ and each role
name $r\in{\sf N_{R}}$ to a subset $r^{\mathcal{I}}$ of
$\Delta^{\mathcal{I}}\times\Delta^{\mathcal{I}}$. The interpretation of
concepts in $\mathcal{I}$ is

$\displaystyle\top^{\mathcal{I}}=\Delta^{\mathcal{I}}\quad(\neg
C)^{\mathcal{I}}=\Delta^{\mathcal{I}}\setminus C^{\mathcal{I}}\quad(C\sqcap
D)^{\mathcal{I}}=C^{\mathcal{I}}\cap D^{\mathcal{I}}$ $\displaystyle(\exists
R.C)^{\mathcal{I}}=\\{d\in\Delta^{\mathcal{I}}\mid\exists d^{\prime}\in
C^{\mathcal{I}}:(d,d^{\prime})\in R^{\mathcal{I}}\\}.$

The interpretation of formulae is as expected

$\displaystyle\mathcal{I}\models\neg(\varphi)\text{ iff not
}\mathcal{I}\models\neg(\varphi)\quad\quad\mathcal{I}\models(\varphi\wedge\psi)\text{
iff }\mathcal{I}\models\varphi\text{ and }\mathcal{I}\models\psi$
$\displaystyle\mathcal{I}\models(C=\top)\text{ iff
}C^{\mathcal{I}}=\top^{\mathcal{I}}\quad\mathcal{I}\models C(a)\text{ iff
}a^{\mathcal{I}}\in C^{\mathcal{I}}\quad\mathcal{I}\models r(a,b)\text{ iff
}(a^{\mathcal{I}},b^{\mathcal{I}})\in r^{\mathcal{I}}.$

Formally, we inductively define the sets ${\sf f}(\varphi)$ and ${\sf
c}(\varphi)$ as follows.

######  Definition 13 (Subformulae)

Given an ${\cal ALC}$-formula $\varphi$, we have that

  * •

if $\varphi$ is atomic then ${\sf
f}(\varphi)\coloneqq\\{\varphi,\neg\varphi\\}$;

  * •

${\sf
f}(\varphi\land\psi)\coloneqq\\{\varphi\land\psi,\neg(\varphi\land\psi)\\}\cup{\sf
f}(\varphi)\cup{\sf f}(\psi)$;

  * •

${\sf f}(\neg(\varphi\land\psi))\coloneqq{\sf f}(\varphi\land\psi)$.

######  Definition 14 (Subconcepts)

Given a an ${\cal ALC}$-formula $\varphi$, ${\sf c}(\varphi)$ is the minimal
set satisfying the following conditions:

  * •

if
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(C=\top)}\in{\sf
f}(\varphi)$ then $C\in{\sf c}(\varphi)$;

  * •

if $C(a)\in{\sf f}(\varphi)$ then $C\in{\sf c}(\varphi)$;

  * •

if $C\sqcap D\in{\sf c}(\varphi)$ then $C,D\in{\sf c}(\varphi)$;

  * •

if $\exists r.C\in{\sf c}(\varphi)$ then $C\in{\sf c}(\varphi)$;

  * •

$\neg C\in{\sf c}(\varphi)$ iff $C\in{\sf c}(\varphi)$.

###### Definition 15

Let $(T,o,{\mathbf{f}})$ be a model candidate for $\varphi$. Then, the
interpretation $\mathcal{I}_{(T,o,{\mathbf{f}})}$ is defined as:

  * •

$\Delta^{\mathcal{I}}\coloneqq T\cup{\sf ind}(\varphi)$;

  * •

$a^{\mathcal{I}}\coloneqq a$, for all $a\in{\sf ind}(\varphi)$;

  * •

$A^{\mathcal{I}}\coloneqq\\{{\mathbf{c}}\in T\mid
A\in{\mathbf{c}}\\}\cup\\{a\in{\sf ind}(\varphi)\mid A\in o(a)\\}$;

  * •

$({\mathbf{c}},{\mathbf{c}}^{\prime})\in r^{\mathcal{I}}$ iff $\\{\neg
C\mid\neg\exists r.C\in{\mathbf{c}}\\}\subseteq{\mathbf{c}}^{\prime}$, for
${\mathbf{c}},{\mathbf{c}}^{\prime}\in T$;

  * •

$(a,b)\in r^{\mathcal{I}}$ iff $r(a,b)\in{\mathbf{f}}$, for $a,b\in{\sf
ind}(\varphi)$;

  * •

$(a,{\mathbf{c}})\in r^{\mathcal{I}}$ iff $\\{\neg C\mid\neg\exists r.C\in
o(a)\\}\subseteq{\mathbf{c}}$, for $a\in{\sf ind}(\varphi)$ and
${\mathbf{c}}\in T$.

###### Example 4

Let
$\varphi=(C=\top)\land\neg(C(a)\land\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(r(a,b))})$.
Then, we have:

$\displaystyle{\sf f}(\varphi)=$
$\displaystyle\\{\varphi,\neg\varphi,C=\top,C\neq\top,\neg(C(a)\land(\neg
r(a,b))),$ $\displaystyle\qquad C(a)\land(\neg
r(a,b)),C(a),{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\neg(C(a))},\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(r(a,b))},r(a,b)\\}$

In any quasimodel $(T,o,{\mathbf{f}})$ for $\varphi$, we have that
$\varphi\in{\mathbf{f}}$. However this also implies that
$(C=\top),\neg(C(a)\land(\neg r(a,b)))\in{\mathbf{f}}$. Consequently
$(C(a)\land(\neg r(a,b)))\not\in{\mathbf{f}}$ and thus,
$C(a)\not\in{\mathbf{f}}$ or $\neg r(a,b)\not\in{\mathbf{f}}$. Hence, there
are only three possible formula types for ${\mathbf{f}}$:

${\mathbf{f}}=\begin{cases}\\{\varphi,C=\top,\neg(C(a)\land(\neg
r(a,b))),C(a),r(a,b)\\}&\text{ or }\\\ \\{\varphi,C=\top,\neg(C(a)\land(\neg
r(a,b))),\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(C(a))},r(a,b)\\}&\text{
or }\\\ \\{\varphi,C=\top,\neg(C(a)\land(\neg
r(a,b))),\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(C(a))},\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(r(a,b))}\\}\end{cases}$

Assuming that for each of these possible formula types there is at least one
quasimodel of ${\mathbf{f}}$, we get that:

$\displaystyle\varphi^{\dagger}\equiv$ $\displaystyle\left((C=\top)\land
C(a)\land
r(a,b)\right){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\lor}$
$\displaystyle\left((C=\top)\land\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(C(a))}\land
r(a,b)\right){\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\lor}$
$\displaystyle\left((C=\top)\land\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(C(a))}\land\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}(r(a,b))}\right)$

It is easy to check that the formula above is equivalent to $\varphi$.

###### Lemma 2

Let $\varphi,\phi$ be ${\cal ALC}$-formulae. If $\varphi\in{\sf f}(\phi)$ then
${\sf f}(\varphi)\subseteq{\sf f}(\phi)$.

###### Proof

The proof follows by induction in the structure of $\phi$. Base: $\phi$ is
atomic. Then, by construction ${\sf f}(\phi)=\\{\phi,\neg\phi\\}$. Thus, if
$\varphi\in{\sf f}(\phi)$ then $\varphi=\phi$ or $\varphi=\neg\phi$. In either
case, ${\sf f}(\varphi)=\\{\varphi,\neg\varphi\\}$ which implies that ${\sf
f}(\varphi)=\\{\phi,\neg\phi\\}$. Thus, ${\sf f}(\varphi)\subseteq{\sf
f}(\phi)$.

In the following, assume that $\phi$ is not atomic.

Induction Hypothesis: by construction $\phi$ is defined as the conjunction of
two formulae $\psi$ and $\psi^{\prime}$ or the negation of such conjunction,
that is, $\phi=\psi\land\psi^{\prime}$ or
$\varphi=\neg(\psi\land\psi^{\prime})$. Let us assume that for all
$\beta\in\\{\psi,\psi^{\prime}\\}$, if $\varphi\in{\sf f}(\beta)$ then ${\sf
f}(\varphi)\subseteq{\sf f}(\beta)$.

Induction step: consider the cases (i) $\phi=\psi\land\psi^{\prime}$ and (ii)
$\phi=\neg(\psi\land\psi^{\prime})$.

  * (i) $\phi=\psi\land\psi^{\prime}$. By construction

${\sf f}(\phi)={\sf
f}(\psi\land\psi^{\prime})=\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}\cup{\sf
f}(\psi)\cup{\sf f}(\psi^{\prime}).$ (1)

Thus, (a)
$\varphi\in\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}$ or (b)
$\varphi\in{\sf f}(\psi)$ or (c) $\varphi\in{\sf f}(\psi^{\prime})$.

    * (a) $\varphi\in\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}$. Thus, either $\varphi=\psi\land\psi^{\prime}$ or $\varphi=\neg(\psi\land\psi^{\prime})$. For $\varphi=\psi\land\psi^{\prime}$, we get that ${\sf f}(\varphi)={\sf f}(\psi\land\psi^{\prime})={\sf f}(\phi)$ which means that ${\sf f}(\varphi)\subseteq{\sf f}(\phi)$. For $\varphi=\neg(\psi\land\psi^{\prime})$, we get that ${\sf f}(\varphi)={\sf f}(\neg(\psi\land\psi^{\prime}))$. By construction, ${\sf f}(\neg(\psi\land\psi^{\prime}))={\sf f}(\psi\land\psi^{\prime})$. Therefore, ${\sf f}(\varphi)={\sf f}(\psi\land\psi^{\prime})={\sf f}(\phi)$ and so ${\sf f}(\varphi)\subseteq{\sf f}(\phi)$.

    * (b) $\varphi\in{\sf f}(\psi)$. By the inductive hypothesis, ${\sf f}(\varphi)\subseteq{\sf f}(\psi)$. From (1), ${\sf f}(\psi)\subseteq{\sf f}(\phi)$. So, ${\sf f}(\varphi)\subseteq{\sf f}(\phi)$.

    * (c) $\varphi\in{\sf f}(\psi^{\prime})$. Analogous to item (b).

  * (ii) $\phi=\neg(\psi\land\psi^{\prime})$. By construction, ${\sf f}(\neg(\psi\land\psi^{\prime}))={\sf f}(\psi\land\psi^{\prime})$. So, ${\sf f}(\phi)={\sf f}(\psi\land\psi^{\prime})=\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}\cup{\sf f}(\psi)\cup{\sf f}(\psi^{\prime})$. Proof proceeds as in item (i).

###### Lemma 3

For every ${\cal ALC}$-formula $\phi$ and formula type ${\mathbf{f}}$ for
$\phi$, if $\phi,\varphi\in{\mathbf{f}}$ then ${\mathbf{f}}\cap{\sf
f}(\varphi)$ is a formula type for $\varphi$.

###### Proof

Let ${\mathbf{f}}_{\phi}$ be a fixed but arbitrary formula type for $\phi$
with $\phi\in{\mathbf{f}}_{\phi}$. We will show that
${\mathbf{f}}\coloneqq{\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$ is a formula
type for $\varphi$. Suppose for contradiction that ${\mathbf{f}}$ is not a
formula type for $\varphi$. Thus, as ${\mathbf{f}}\subseteq{\sf f}(\varphi)$,
either condition (1) or (2) of the formula type definition is violated:

  1. 1.

There are formulae $\psi,\neg\psi\in{\sf f}(\varphi)$ such that either (a)
$\psi\not\in{\mathbf{f}}$ and $\neg\psi\not\in{\mathbf{f}}$, or (b)
$\psi,\neg\psi\in{\mathbf{f}}$.

    1. (a) $\psi\not\in{\mathbf{f}}$ and $\neg\psi\not\in{\mathbf{f}}$. By hypothesis, $\varphi\in{\mathbf{f}}_{\phi}$. Thus, as ${\mathbf{f}}={\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$, and by construction $\varphi\in{\sf f}(\varphi)$, we get that $\varphi\in{\mathbf{f}}$. Since ${\mathbf{f}}_{\phi}$ is a formula type, we have that for all $\psi^{\prime}\in{\sf f}(\phi)$, $\psi^{\prime}\in{\mathbf{f}}_{\phi}$ iff $\neg\psi^{\prime}\not\in{\mathbf{f}}_{\phi}$. As $\varphi\in{\mathbf{f}}_{\phi}\subseteq{\sf f}(\phi)$, it follows from Lemma 2 that ${\sf f}(\varphi)\subseteq{\sf f}(\phi)$. Therefore, for all $\psi^{\prime}\in{\sf f}(\varphi)$, $\psi^{\prime}\in{\mathbf{f}}_{\phi}$ iff $\neg\psi^{\prime}\not\in{\mathbf{f}}_{\phi}$. By hypothesis, $\neg\psi,\psi\in{\sf f}(\varphi)$ which implies from above that either:

$\displaystyle\psi\in{\mathbf{f}}_{\phi}\mbox{ and
}\neg\psi\not\in{\mathbf{f}}_{\phi},\mbox{ or
}\psi\not\in{\mathbf{f}}_{\phi}\mbox{ and }\neg\psi\in{\mathbf{f}}_{\phi}.$
(2)

By hypothesis, $\neg\psi,\psi\in{\sf f}(\varphi)$ but
$\neg\psi,\psi\not\in{\mathbf{f}}$. Thus, as
${\mathbf{f}}={\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$, we get
$\neg\psi,\psi\not\in{\mathbf{f}}_{\phi}$, contradicting (2).

    2. (b) $\psi,\neg\psi\in{\mathbf{f}}$. By hypothesis, ${\mathbf{f}}_{\phi}$ is a formula type which implies that for all $\psi^{\prime}\in{\mathbf{f}}_{\phi}$, $\psi^{\prime},\neg\psi^{\prime}\not\in{\mathbf{f}}_{\phi}$. Therefore, as ${\mathbf{f}}\subseteq{\mathbf{f}}_{\phi}$, we get that $\psi,\neg\psi\not\in{\mathbf{f}}$, a contradiction.

  2. 2.

Let $\psi\land\psi^{\prime}\in{\sf f}(\varphi)$. We will show that
$\psi\land\psi^{\prime}\in{\mathbf{f}}$ iff
$\\{\psi,\psi^{\prime}\\}\subseteq{\mathbf{f}}$ which contradicts the
hypothesis that condition (2) from the formula type definition is violated. We
split the proof in two cases: either (a)
$\psi\land\psi^{\prime}\in{\mathbf{f}}$ or (b)
$\psi\land\psi^{\prime}\not\in{\mathbf{f}}$. If
$\psi\land\psi^{\prime}\in{\mathbf{f}}$, as
${\mathbf{f}}={\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$, we get that
$\psi\land\psi^{\prime}\in{\mathbf{f}}_{\phi}$. Since ${\mathbf{f}}_{\phi}$ is
a formula type, we have that
$\\{\psi,\psi^{\prime}\\}\subseteq{\mathbf{f}}_{\phi}$. By definition of ${\sf
f}(\varphi)$, if $\psi\land\psi^{\prime}\in{\sf f}(\varphi)$ then
$\\{\psi,\psi^{\prime}\\}\subseteq{\sf f}(\varphi)$. Hence,
$\\{\psi,\psi^{\prime}\\}\in{\mathbf{f}}={\mathbf{f}}_{\phi}\cap{\sf
f}(\varphi)$.

Otherwise, $\psi\land\psi^{\prime}\not\in{\mathbf{f}}$. As
${\mathbf{f}}={\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$ and
$\psi\land\psi^{\prime}\in{\sf f}(\varphi)$, we get that
$\psi\land\psi^{\prime}\not\in{\mathbf{f}}_{\phi}$. Thus, as
${\mathbf{f}}_{\phi}$ is a formula type, we get that
$\\{\psi,\psi^{\prime}\\}\not\subseteq{\mathbf{f}}_{\phi}$. Therefore, as
${\mathbf{f}}\subseteq{\mathbf{f}}_{\phi}$, we get that
$\\{\psi,\psi^{\prime}\\}\not\subseteq{\mathbf{f}}$. From (a) and (b) we
conclude that $\psi\land\psi^{\prime}\in{\mathbf{f}}$ iff
$\\{\psi,\psi^{\prime}\\}\subseteq{\mathbf{f}}$. But this contradicts the
hypothesis that condition (2) from the formula type definition is violated.

Therefore, we conclude that ${\mathbf{f}}$ is a formula type.

###### Lemma 4

For every ${\cal ALC}$-formula $\varphi$, ${\sf f}(\varphi)={\sf
f}(\neg\varphi)$ 222 We silently remove double negation and treat
$\neg\neg\phi$ as equal to $\phi$..

###### Proof

By construction $\varphi$ is a subformula of $\neg\varphi$. We can see that
${\sf f}(\neg\varphi)={\sf f}(\varphi)\cup\\{\neg\varphi\\}$. Since ${\sf
f}(\varphi)$ is closed under single negation and, by construction,
$\varphi\in{\sf f}(\varphi)$, we have that $\neg\varphi\in{\sf f}(\varphi)$.
Thus, ${\sf f}(\varphi)={\sf f}(\neg\varphi)$.

###### Definition 16

Let $\varphi$ be an ${\cal ALC}$-formula. The set of of formula types for
$\varphi$ that has $\varphi$ is given by the set

$\tau(\varphi)=\\{{\mathbf{f}}\subseteq{\sf f}(\varphi)\mid{\mathbf{f}}\mbox{
is a formula type for }\varphi\mbox{ and }\varphi\in{\mathbf{f}}\\}.$

###### Lemma 5

For every ${\cal ALC}$-formula $\phi$ and formula type ${\mathbf{f}}$ for
$\phi$, if $\phi\in{\mathbf{f}}$ and $\varphi\in{\sf f}(\phi)$ then
${\mathbf{f}}\cap{\sf f}(\varphi)\in\tau(\varphi)\cup\tau(\neg\varphi)$.

###### Proof

Let ${\mathbf{f}}_{\phi}$ be a fixed but arbitrary formula type for $\phi$
with $\phi\in{\mathbf{f}}_{\phi}$. As ${\mathbf{f}}_{\phi}$ is a formula type
(for $\phi$) and $\varphi\in{\sf f}(\phi)$, either (i)
$\varphi\in{\mathbf{f}}_{\phi}$ or $\neg\varphi\in{\mathbf{f}}_{\phi}$:

  1. (i) $\varphi\in{\mathbf{f}}_{\phi}$. Thus, by Lemma 3, we have that ${\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$ is a formula type of $\varphi$. Also, $\varphi\in{\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$. Therefore, ${\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)\in\tau(\varphi)$ which means that ${\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)\in\tau(\varphi)\cup\tau(\neg\varphi)$.

  2. (ii) $\neg\varphi\in{\mathbf{f}}_{\phi}$. Thus, by Lemma 3, we have that ${\mathbf{f}}_{\phi}\cap{\sf f}(\neg\varphi)$ is a formula type for $\neg\varphi$. Also, $\neg\varphi\in{\mathbf{f}}_{\phi}\cap{\sf f}(\neg\varphi)$. Therefore, ${\mathbf{f}}_{\phi}\cap{\sf f}(\neg\varphi)\in\tau(\neg\varphi)$ which means that ${\mathbf{f}}_{\phi}\cap{\sf f}(\neg\varphi)\in\tau(\varphi)\cup\tau(\neg\varphi)$. By Lemma 4, we have that ${\sf f}(\varphi)={\sf f}(\neg\varphi)$ which implies that ${\mathbf{f}}_{\phi}\cap{\sf f}(\neg\varphi)={\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)$. Therefore, ${\mathbf{f}}_{\phi}\cap{\sf f}(\varphi)\in\tau(\varphi)\cup\tau(\neg\varphi)$.

###### Lemma 6

For every ${\cal ALC}$-formula $\varphi$, ${\mathbf{f}}\in\tau(\varphi)$ iff
${\mathbf{f}}$ is a formula type for $\varphi$ and

  1. 1.

if $\varphi$ is atomic then ${\mathbf{f}}=\\{\varphi\\}$;

  2. 2.

if $\varphi=\psi\land\psi^{\prime}$ then
${\mathbf{f}}=\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$,
for some ${\mathbf{f}}_{\psi}\in\tau(\psi)$ and
${\mathbf{f}}_{\psi^{\prime}}\in\tau(\psi^{\prime})$;

  3. 3.

if $\varphi=\neg(\psi\land\psi^{\prime})$ then
${\mathbf{f}}=\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$,
for some
${\mathbf{f}}_{\psi}\in\tau(\psi)\cup\tau(\neg\psi),{\mathbf{f}}_{\psi^{\prime}}\in\tau(\psi^{\prime})\cup\tau(\neg\psi^{\prime})$
such that either ${\mathbf{f}}_{\psi}\in\tau(\neg\psi)$ or
${\mathbf{f}}_{\psi^{\prime}}\in\tau(\neg\psi^{\prime})$.

###### Proof

The direction “$\Leftarrow$” is trivial, so we focus only on the
“$\Rightarrow$” direction. Let ${\mathbf{f}}\in\tau(\varphi)$. Thus,
$\varphi\in{\mathbf{f}}$ and ${\mathbf{f}}$ is a formula type for $\varphi$.
By construction, (I) either $\varphi$ is atomic or (II)
$\varphi=\psi\land\psi^{\prime}$ or (III)
$\varphi=\neg(\psi\land\psi^{\prime})$:

  1. (I) $\varphi$ is atomic. Thus, by construction ${\mathbf{f}}=\\{\varphi\\}$ or ${\mathbf{f}}=\\{\neg\varphi\\}$. Thus, as $\varphi\in{\mathbf{f}}$, we get ${\mathbf{f}}=\\{\varphi\\}$.

  2. (II) $\varphi=\psi\land\psi^{\prime}$. As $\varphi\in{\mathbf{f}}$, we get that $\psi\land\psi^{\prime}\in{\mathbf{f}}$. Moreover, as ${\mathbf{f}}$ is a formula type for $\varphi$ and $\psi\land\psi^{\prime}\in{\mathbf{f}}$, it follows that $\psi,\psi^{\prime}\in{\mathbf{f}}$.

Let

$\displaystyle{\mathbf{f}}_{\psi}\coloneqq{\mathbf{f}}\cap{\sf f}(\psi)$
$\displaystyle\mbox{ and
}{\mathbf{f}}_{\psi^{\prime}}\coloneqq{\mathbf{f}}\cap{\sf f}(\psi^{\prime}).$

As $\psi,\psi^{\prime}\in{\mathbf{f}}$ and ${\mathbf{f}}$ is a formula type
for $\varphi=\psi\land\psi^{\prime}$, by Lemma 3,
${\mathbf{f}}_{\psi}={\mathbf{f}}\cap{\sf f}(\psi)$ is a formula type for
$\psi$ and ${\mathbf{f}}_{\psi^{\prime}}={\mathbf{f}}\cap{\sf
f}(\psi^{\prime})$ is a formula type for $\psi^{\prime}$. We have that
$\psi\in{\sf f}(\psi)$ and $\psi^{\prime}\in{\sf f}(\psi^{\prime})$ which
means that $\psi\in{\mathbf{f}}_{\psi}$ and
$\psi^{\prime}\in{\mathbf{f}}_{\psi^{\prime}}$. Thus,
${\mathbf{f}}_{\psi}\in\tau(\psi)$ and
${\mathbf{f}}_{\psi^{\prime}}\in\tau(\psi^{\prime})$. We still need to show
that
${\mathbf{f}}=\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.
For this, we will show that (i)
${\mathbf{f}}\subseteq\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$
and (ii)
$\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}\subseteq{\mathbf{f}}$.
The case (ii) is trivial, so we focus only on case (i). Let
$\phi\in{\mathbf{f}}$. As ${\mathbf{f}}$ is a formula type for
$\varphi=\psi\land\psi^{\prime}$, we get that

$\phi\in{\mathbf{f}}\subseteq{\sf
f}(\psi\land\psi^{\prime})=\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}\cup{\sf
f}(\psi)\cup{\sf f}(\psi^{\prime}).$

Therefore, (a)
$\phi\in\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}$ or (b)
$\phi\in{\sf f}(\psi)$ or (c) $\phi\in{\sf f}(\psi^{\prime})$.

     * (a) $\phi\in\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}$. As ${\mathbf{f}}$ is a formula type and $\varphi=\psi\land\psi^{\prime}\in{\mathbf{f}}$, we get that $\neg(\psi\land\psi^{\prime})\not\in{\mathbf{f}}$. Therefore, as $\phi\in{\mathbf{f}}$, we have that $\phi\neq\neg(\psi\land\psi^{\prime})$. Hence, $\phi=\psi\land\psi^{\prime}$, which implies that $\phi\in\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

     * (b) $\phi\in{\sf f}(\psi)$. Thus, as $\phi\in{\mathbf{f}}$, we get that $\phi\in{\mathbf{f}}_{\psi}={\mathbf{f}}\cap{\sf f}(\psi)$ which implies that $\phi\in\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

     * (c) $\phi\in{\sf f}(\psi^{\prime})$. Thus, as $\phi\in{\mathbf{f}}$, we get that $\phi\in{\mathbf{f}}_{\psi^{\prime}}={\mathbf{f}}\cap{\sf f}(\psi^{\prime})$ which implies that $\phi\in\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

Thus,
$\phi\in\\{\psi\land\psi^{\prime}\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

  3. (III) $\varphi=\neg(\psi\land\psi^{\prime})$. As $\varphi\in{\mathbf{f}}$, we get that $\neg(\psi\land\psi^{\prime})\in{\mathbf{f}}$. Let

$\displaystyle{\mathbf{f}}_{\psi}\coloneqq{\mathbf{f}}\cap{\sf f}(\neg\psi)$
$\displaystyle\mbox{ and
}{\mathbf{f}}_{\psi^{\prime}}\coloneqq{\mathbf{f}}\cap{\sf
f}(\neg\psi^{\prime}).$

As $\neg\psi,\neg\psi^{\prime}\in{\sf
f}(\varphi=\neg(\psi\land\psi^{\prime}))$, by Lemma 5, we have that

${\mathbf{f}}_{\psi}\in\tau(\psi)\cup\tau(\neg\psi)\mbox{ and
}{\mathbf{f}}_{\psi^{\prime}}\in\tau(\psi^{\prime})\cup\tau(\neg\psi^{\prime}).$

Moreover, as ${\mathbf{f}}$ is a formula type for $\varphi$ and
$\varphi=\neg(\psi\land\psi^{\prime})\in{\mathbf{f}}$, it follows that
$\psi\land\psi^{\prime}\not\in{\mathbf{f}}$. Therefore,
$\\{\psi,\psi^{\prime}\\}\not\subseteq{\mathbf{f}}$. Thus, either
$\psi\not\in{\mathbf{f}}$ or $\psi^{\prime}\not\in{\mathbf{f}}$. Thus, as
${\mathbf{f}}$ is a formula type, either (i) $\neg\psi\in{\mathbf{f}}$ or (ii)
$\neg\psi^{\prime}\in{\mathbf{f}}$.

     * (i) $\neg\psi\in{\mathbf{f}}$. Thus, as ${\mathbf{f}}$ is a formula type for $\varphi=\neg(\psi\land\psi^{\prime})$, by Lemma 3, ${\mathbf{f}}_{\psi}={\mathbf{f}}\cap{\sf f}(\neg\psi)$ is a formula type for $\neg\psi$. We have that $\neg\psi\in{\sf f}(\neg\psi)$. So $\neg\psi\in{\mathbf{f}}_{\psi}$. Thus, ${\mathbf{f}}_{\psi}\in\tau(\neg\psi)$.

     * (ii) $\neg\psi^{\prime}\in{\mathbf{f}}$. Analogously to item (i), we get that ${\mathbf{f}}_{\psi^{\prime}}\in\tau(\neg\psi^{\prime})$.

Thus,

${\mathbf{f}}_{\psi}\in\tau(\neg\psi)\mbox{ or
}{\mathbf{f}}_{\psi^{\prime}}\in\tau(\neg\psi^{\prime}).$

We still need to show that
${\mathbf{f}}=\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.
For this we need to show that (i)
${\mathbf{f}}\subseteq\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$
and (ii)
$\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}\subseteq{\mathbf{f}}$.
The case (ii) is trivial. So we focus only on case (i).

Let $\phi\in{\mathbf{f}}$. As ${\mathbf{f}}$ is a formula type for
$\varphi=\neg(\psi\land\psi^{\prime})$, we get that

$\displaystyle\phi\in{\mathbf{f}}\subseteq{\sf
f}(\neg(\psi\land\psi^{\prime}))$ $\displaystyle={\sf
f}(\psi\land\psi^{\prime})$
$\displaystyle=\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}\cup{\sf
f}(\psi)\cup{\sf f}(\psi^{\prime}).$

Therefore, (a)
$\phi\in\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}$ or (b)
$\phi\in{\sf f}(\psi)$ or (c) $\phi\in{\sf f}(\psi^{\prime})$.

     * (a) $\phi\in\\{\psi\land\psi^{\prime},\neg(\psi\land\psi^{\prime})\\}$. As ${\mathbf{f}}$ is a formula type and $\varphi=\neg(\psi\land\psi^{\prime})\in{\mathbf{f}}$, we get that $(\psi\land\psi^{\prime})\not\in{\mathbf{f}}$. Therefore, as $\phi\in{\mathbf{f}}$, we have that $\phi\neq(\psi\land\psi^{\prime})$. Therefore, $\phi=\neg(\psi\land\psi^{\prime})$, which implies that $\phi\in\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

     * (b) $\phi\in{\sf f}(\psi)$. By Lemma 4, we get ${\sf f}(\psi)={\sf f}(\neg\psi)$. Therefore, $\phi\in{\sf f}(\neg\psi)$. Thus, as $\phi\in{\mathbf{f}}$, we get that $\phi\in{\mathbf{f}}_{\psi}={\mathbf{f}}\cap{\sf f}(\neg\psi)$ which implies that $\phi\in\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$

     * (c) $\phi\in{\sf f}(\psi^{\prime})$. Analogously to item (b), we get $\phi\in\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

Thus,
$\phi\in\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}}$.

######  Definition 17 (Formula degree)

The degree of an ${\cal ALC}$-formula $\phi$, denoted $degree(\phi)$, is

  * •

$1$ if $\phi$ is an atomic ${\cal ALC}$-formula;

  * •

$degree(\varphi)+1$ if $\phi=\neg\varphi$; and

  * •

$degree(\varphi)+degree(\psi)$ if $\phi=\varphi\land\psi$.

######  Lemma 7 ([8])

If $\mathcal{I}\models\varphi$ then
$\operatorname{qm}({\varphi},{\mathcal{I}})$ is a quasimodel for $\varphi$.

To show Theorem 3.2, we use Lemma 8.

######  Lemma 8 ()

Let $\varphi$ be an ${\cal ALC}$-formula. If ${\mathbf{f}}\in\tau(\varphi)$
then

$\bigg{(}\bigwedge lit({\mathbf{f}})\bigg{)}\models\varphi.$

###### Proof

The proof follows by induction in the degree of $\phi$.

Base: $degree(\phi)=1$. Then $\phi$ is atomic. This implies from Lemma 6 that
${\mathbf{f}}=\\{\phi\\}$. Thus, $\bigwedge lit({\mathbf{f}})=\phi$. For
${\cal ALC}$, this means that $\bigwedge lit({\mathbf{f}})\models\phi$.

Induction Hypothesis: For every formula $\varphi$, and formula type
${\mathbf{f}}_{\varphi}$ for $\varphi$, if $\varphi\in{\mathbf{f}}_{\varphi}$
and $degree(\varphi)<degree(\phi)$ then $\bigwedge
lit({\mathbf{f}}_{\varphi})\models\varphi$.

Induction Step: Let $degree(\phi)>1$. By construction, $\phi$ is of the form
$\varphi\land\psi$ or $\neg\varphi$, for some ${\cal ALC}$-formulae $\varphi$
and $\psi$:

  1. 1.

$\phi=\varphi\land\psi$. Thus, from Lemma 6,

${\mathbf{f}}=\\{\varphi\land\psi\\}\cup{\mathbf{f}}_{\varphi}\cup{\mathbf{f}}_{\psi},\mbox{
such that
}{\mathbf{f}}_{\varphi}\in\tau(\varphi),{\mathbf{f}}_{\psi}\in\tau(\psi).$

Note that $lit({\mathbf{f}})=lit({\mathbf{f}}_{\varphi})\cup
lit({\mathbf{f}}_{\psi})$. Therefore,

$\bigwedge lit({\mathbf{f}})=\bigg{(}\bigwedge
lit({\mathbf{f}}_{\varphi})\bigg{)}\land\bigg{(}\bigwedge
lit({\mathbf{f}}_{\psi})\bigg{)}$

By the definition of degree, we get that
$degree(\phi)=degree(\varphi\land\psi)=degree(\varphi)+degree(\psi)$ and
$1\leq degree(\varphi)$ and $1\leq degree(\psi)$. Therefore,
$degree(\varphi)<degree(\phi)$ and $degree(\psi)<degree(\phi)$. By the
inductive hypothesis,

$\bigwedge lit({\mathbf{f}}_{\varphi})\models\varphi\mbox{ and }\bigwedge
lit({\mathbf{f}}_{\psi})\models\psi.$

Therefore,

$\bigwedge lit({\mathbf{f}})=\bigwedge
lit({\mathbf{f}}_{\varphi})\land\bigwedge
lit({\mathbf{f}}_{\psi})\models\varphi\land\psi.$

Thus, as $\phi=\varphi\land\psi$ , we get

$\bigwedge lit({\mathbf{f}})\models\phi.$

  2. 2.

$\phi=\neg\varphi$. By construction, either: (a) $\varphi$ is atomic, or
(b)$\varphi=\psi\land\psi^{\prime}$.

    1. (a)

$\varphi$ is atomic. We get from Lemma 6 that
${\mathbf{f}}=\\{\neg\varphi\\}$, which implies that
$lit({\mathbf{f}})=\\{\neg\varphi\\}$, and analogous to the base case, we get
that $\bigwedge lit({\mathbf{f}})\models\neg\varphi$ that is, $\bigwedge
lit({\mathbf{f}})\models\phi$.

    2. (b)

$\varphi=\psi\land\psi^{\prime}$. By Lemma 6, we get that

$\displaystyle{\mathbf{f}}=\\{\neg(\psi\land\psi^{\prime})\\}\cup{\mathbf{f}}_{\psi}\cup{\mathbf{f}}_{\psi^{\prime}},$
(3)

where
${\mathbf{f}}_{\psi}\in\tau(\psi)\cup\tau(\neg\psi),{\mathbf{f}}_{\psi^{\prime}}\in\tau(\psi^{\prime})\cup\tau(\neg\psi^{\prime})$
such that either

${\mathbf{f}}_{\psi}\in\tau(\neg\psi)\mbox{ or
}{\mathbf{f}}_{\psi^{\prime}}\in\tau(\neg\psi^{\prime}).$

      1. i.

${\mathbf{f}}_{\psi}\in\tau(\neg\psi)$. From definition of degree, we get that

$degree(\phi)=degree(\neg(\psi\land\psi^{\prime}))=degree(\psi)+degree(\psi^{\prime})+1,$

and $degree(\psi)\geq 1$ and $degree(\psi^{\prime})\geq 1$ and
$degree(\neg\psi)=degree(\psi)+1$. Thus,
$degree(\phi)=degree(\neg(\psi\land\psi^{\prime}))=degree(\neg\psi)+degree(\psi^{\prime})$.
Thus, as $degree(\psi^{\prime})\geq 1$ we get

$degree(\neg\psi)<degree(\phi).$

Thus, by the inductive hypothesis, $\bigwedge
lit({\mathbf{f}}_{\psi})\models\neg\psi$. Note that for every formula $\beta$,
$\neg\psi\models\neg(\psi\land\beta)$. Therefore, for $\beta=\psi^{\prime}$

$\bigwedge lit({\mathbf{f}}_{\psi})\models\neg(\psi\land\psi^{\prime})$

From (3), we get that

$\bigwedge lit({\mathbf{f}})=\bigwedge lit({\mathbf{f}}_{\psi})\land\bigwedge
lit({\mathbf{f}}_{\psi^{\prime}}).$

Thus, as $\bigwedge
lit({\mathbf{f}}_{\psi})\models\neg(\psi\land\psi^{\prime})$, we get that
$\bigwedge lit({\mathbf{f}}_{\psi})\land\bigwedge
lit({\mathbf{f}}_{\psi^{\prime}})\models\neg(\psi\land\psi^{\prime})$ which
implies from above that $\bigwedge
lit({\mathbf{f}})\models\neg(\psi\land\psi^{\prime})$ that is,

$\bigwedge lit({\mathbf{f}})\models\phi.$

      2. ii.

${\mathbf{f}}_{\psi}\in\tau(\neg\psi^{\prime})$. Analogous to item (i).

See 3.4

###### Proof

If $M\not\models\varphi$, then
$\operatorname{con}(\varphi,M)=\operatorname{con}^{\prime}(\varphi,M)=\varphi$.
Now, suppose that $M\models\varphi$. In this case, we know from Lemma 7 that
$(T^{\prime},o^{\prime},{\mathbf{f}}^{\prime})=\operatorname{qm}({\varphi},{M})$
is a quasimodel for $\varphi$. From Theorem 3.2, we know that:

$\displaystyle\operatorname{con}^{\prime}(\varphi,M)$
$\displaystyle\equiv\varphi^{\dagger}\land\neg(\bigwedge lit({\mathbf{f}}))$
$\displaystyle=\left(\bigvee_{(T,o,{\mathbf{f}})\in{\sf S}(\varphi)}(\bigwedge
lit({\mathbf{f}}))\right)\land\neg(\bigwedge lit({\mathbf{f}}))$

For each $(T,o,{\mathbf{f}})$ in ${\sf S}(\varphi)$ either
$lit({\mathbf{f}})=lit({\mathbf{f}}^{\prime})$ or $lit({\mathbf{f}})\neq
lit({\mathbf{f}}^{\prime})$. If
$lit({\mathbf{f}})=lit({\mathbf{f}}^{\prime})$, then:

$\bigwedge lit({\mathbf{f}})\land\neg(\bigwedge
lit({\mathbf{f}}^{\prime}))\equiv\bot.$

Otherwise, we know that

$\bigwedge lit({\mathbf{f}})\land\neg(\bigwedge
lit({\mathbf{f}}^{\prime}))\not\equiv\bot.$

Due to the definition of $\operatorname{\mu}$ and Corollary 1 we can conclude
that for every ${\mathbf{f}}\in\operatorname{ftypes}({\varphi})$,
${\mathbf{f}}\in\operatorname{\mu}(\varphi,M)$ iff $lit({\mathbf{f}})\neq
lit({\mathbf{f}}^{\prime})$. As we can ignore inconsistent formulae in
disjunctions, we get that
$\operatorname{con}(\varphi,M)\equiv\operatorname{con}^{\prime}(\varphi,M)$.

See 3.2

###### Proof

Let $\varphi$ be an ${\cal ALC}$-formula and $\mathcal{I}$ an interpretation.

####
$\mathcal{I}\models\varphi\Rightarrow\mathcal{I}\models\varphi^{\dagger}$:

First, suppose that $\mathcal{I}\models\varphi$. From Lemma 7 we know that
$\operatorname{qm}({\varphi},{\mathcal{I}})=(T,o,{\mathbf{f}})$ is a
quasimodel of $\varphi$. Therefore, there is a disjunct $\psi$ of
$\varphi^{\dagger}$ which is the conjunction of all atomic formulae in
${\mathbf{f}}$. By Definition 9 $\mathcal{I}\models{\mathbf{f}}$, thus we can
conclude that $\mathcal{I}\models\varphi^{\dagger}$.

####
$\mathcal{I}\models\varphi^{\dagger}\Rightarrow\mathcal{I}\models\varphi$:

Now, assume that $\mathcal{I}\models\varphi^{\dagger}$. This means that there
is one disjunct $\psi$ of $\varphi^{\dagger}$ such that
$\mathcal{I}\models\psi$. By construction, this disjunct is a conjunction of
atomic formulae in the formula type of a quasimodel $(T,o,{\mathbf{f}})$ for
$\varphi$. Using Lemma 8 we can conclude that
$\mathcal{I}\models{\mathbf{f}}$. As $\varphi\in{\mathbf{f}}$ we get that
$\mathcal{I}\models\varphi$. Hence, $\mathcal{I}\models\varphi$ iff
$\mathcal{I}\models\varphi^{\dagger}$, i.e., $\varphi\equiv\varphi^{\dagger}$.

Corollary 1 is a direct consequence of the definition of a formula type.

###### Corollary 1

Let $(T,o,{\mathbf{f}})$ and $(T^{\prime},o^{\prime},{\mathbf{f}}^{\prime})$
be quasimodels for an ${\cal ALC}$-formula $\varphi$. Then,
$lit({\mathbf{f}})=lit({\mathbf{f}}^{\prime})$ iff
${\mathbf{f}}={\mathbf{f}}^{\prime}$.

Given ${\cal ALC}$-formulae $\varphi,\psi$, we say that $\psi$ is in the
language of the literals of $\varphi$, written
$\psi\in{\mathcal{L}_{lit}({\varphi})}$, if $\psi$ is a boolean combination of
the atoms in $\varphi$.

###### Lemma 9

Let $M,M^{\prime}$ be models and $\varphi$ an ${\cal ALC}$-formula. Also let
$(T,o,{\mathbf{f}})\coloneqq\operatorname{qm}({\varphi},{M})$ and
$(T^{\prime},o^{\prime},{\mathbf{f}}^{\prime})\coloneqq\operatorname{qm}({\varphi},{M^{\prime}})$.
Then, ${{[{M}]^{\varphi}}}\ =\ {{[{M^{\prime}}]^{\varphi}}}$ iff
${\mathbf{f}}={\mathbf{f}}^{\prime}$.

###### Proof

First, assume that ${{[{M}]^{\varphi}}}={{[{M^{\prime}}]^{\varphi}}}$. Then we
know that for every $\alpha\in{\mathcal{L}_{lit}({\varphi})}$,
$M\models\alpha$ iff $M^{\prime}\models\alpha$. With Corollary 1 we can
conclude that ${\mathbf{f}}={\mathbf{f}}^{\prime}$.

Now, assume that ${\mathbf{f}}={\mathbf{f}}^{\prime}$. Corollary 1 implies
that $lit({\mathbf{f}})=lit({\mathbf{f}}^{\prime})$. In other words, for every
atomic subformula $\alpha\in{\mathcal{L}_{lit}({\varphi})}$ we have that
$\varphi$, $M\models\alpha$ iff $M^{\prime}\models\alpha$, that is,
${{[{M}]^{\varphi}}}={{[{M^{\prime}}]^{\varphi}}}$.

###### Lemma 10

Let $M$ be a model and $\varphi$ an ${\cal ALC}$-formula. Then, the following
holds:
$\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}=\operatorname{Mod}({\operatorname{con}(\varphi,M)})$.

###### Proof

Let $(T,o,{\mathbf{f}})\coloneqq\operatorname{qm}({\varphi},{M})$ and
$(T^{\prime},o^{\prime},{\mathbf{f}}^{\prime})\coloneqq\operatorname{qm}({\varphi},{M^{\prime}})$.
First, suppose that
$M^{\prime}\in{\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}}$. We
know that $M^{\prime}\models\varphi$ and by Lemma 7 we get that
$\operatorname{qm}({\varphi},{M^{\prime}})$ is a quasimodel for $\varphi$. We
also know that $M^{\prime}\not\in\ {{[{M}]^{\varphi}}}$. Thus, from Lemma 9,
we obtain ${\mathbf{f}}\neq{\mathbf{f}}^{\prime}$. Therefore,
${\mathbf{f}}^{\prime}\in\operatorname{\mu}(\varphi,M)$. Hence,
$M^{\prime}\in{\operatorname{Mod}({\operatorname{con}(\varphi,M)})}$ and so
${\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}}\subseteq{\operatorname{Mod}({\operatorname{con}(\varphi,M)})}$.

Now, let $M^{\prime}\in{\operatorname{Mod}({\operatorname{con}(\varphi,M)})}$.
This means that there is at least one
${\mathbf{f}}{{}^{\prime\prime}}\in\operatorname{\mu}(\varphi,M)$ such that
$M^{\prime}\models\bigwedge lit({\mathbf{f}}^{\prime\prime})$. But as
consequence of the definition of formula type, this implies that
$M^{\prime}\in\operatorname{Mod}({\varphi})$ and thus
$(T^{\prime},o^{\prime},{\mathbf{f}}^{\prime})\in{\sf S}(\varphi)$. We also
know that $M\not\in\ {{[{M}]^{\varphi}}}$, otherwise
${\mathbf{f}}^{\prime}={\mathbf{f}}$ due to Lemma 9. Therefore,
$M^{\prime}\in{\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}}$ and
we can conclude that
${\operatorname{Mod}({\operatorname{con}(\varphi,M)})}\subseteq{\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}}$.

Finally, we obtain:
${\operatorname{Mod}({\operatorname{con}(\varphi,M)})}={\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}}$.

See 3.3

###### Proof

Assume that
$\operatorname{con}^{*}(\varphi,{M})\equiv\operatorname{con}(\varphi,{M})$.
From Lemma 10 we have that
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})=\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}$,
hence success and inclusion are immediately satisfied. To prove atomic
retainment, assume that
${M}^{\prime}\not\in\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})$
and that there is a set of models $\mathbb{M}^{\prime}$ with
${M}^{\prime}\in\mathbb{M}^{\prime}$,
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})\subset\mathbb{M}^{\prime}\subseteq\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}$
and that is finitely representable in ${\cal ALC}$-formula. Lemma 10 implies
that
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})=\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}$.
Hence, ${M}^{\prime}\in{{[{{M}}]^{\varphi}}}$, a contradiction as we assumed
that
$\mathbb{M}^{\prime}\subseteq\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}$.
Therefore, no such $\mathbb{M}^{\prime}$ could exist, and thus,
$\operatorname{con}^{*}$ satisfies atomic retainment.

Let ${M}^{\prime}\equiv^{\varphi}{M}$. Since
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})=\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}$
and ${{[{M^{\prime}}]^{\varphi}}}={{[{M}]^{\varphi}}}$, we have that:
$\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}=\operatorname{Mod}({\varphi})\setminus{{[{{M}^{\prime}}]^{\varphi}}}=\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M}^{\prime})})$.
Hence, atomic extensionality is also satisfied.

On the other hand, suppose that $\operatorname{con}^{*}(\varphi,M)$ satisfies
the postulates stated. Let
$M^{\prime}\in\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}$ and
assume that
$M^{\prime}\not\in\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})$.
Due to atomic retainment, this means that there is no set
$\mathbb{M}^{\prime}$ finitely representable in ${\cal ALC}$-formula such that
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})\subset\mathbb{M}^{\prime}\subseteq\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}$
and ${M}^{\prime}\in\mathbb{M}^{\prime}$. But we know from Lemma 10 that
$\operatorname{Mod}({\varphi})\setminus{{[{{M}}]^{\varphi}}}$ is finitely
representable in ${\cal ALC}$-formula and includes ${M}^{\prime}$ by
assumption, a contradiction. Thus, no such ${M}^{\prime}$ could exist and
$\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}\subseteq\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})$.

Now, let
${M}^{\prime}\in\operatorname{Mod}({\operatorname{con}^{*}(\varphi,{M})})$. By
inclusion ${M}^{\prime}\in\operatorname{Mod}({\varphi})$ and by success
${M}^{\prime}\neq{M}$. We will show that
${M}^{\prime}\not\in{{[{M}]^{\varphi}}}$. By contradiction, suppose that
${M}^{\prime}\in\ {{[{M}]^{\varphi}}}$. Due to atomic extensionality
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})=\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M^{\prime})})$,
but success implies that
$M^{\prime}\not\in\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M^{\prime})})$.
This contradicts our initial assumption that
$M^{\prime}\in\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})$.
Therefore
$M^{\prime}\in\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}$ and
we can conclude that
$\operatorname{Mod}({\operatorname{con}^{*}(\varphi,M)})\subseteq\operatorname{Mod}({\varphi})\setminus{{[{M}]^{\varphi}}}$.

Hence, Lemma 10 yields
$\operatorname{con}(\varphi,M)\equiv\operatorname{con}^{*}(\varphi,M)$.

###### Proposition 1

Let ${\mathbf{f}}$ be a formula type. If $M\models\bigwedge
lit({\mathbf{f}})$, $\psi\in{\mathcal{L}_{lit}({{\mathbf{f}}})}$ and
$M\models\psi$ then $\bigwedge lit({\mathbf{f}})\models\psi$.

###### Proof

Let ${\mathbf{f}}$ be a formula type, $M$ a model such that $M\models\bigwedge
lit({\mathbf{f}})$, and $\psi$ and ${\cal ALC}$-formula such that
$M\models\psi$. The proof is by induction on the degree of $\psi$.

  * Base: $degree(\psi)=1$. Thus, from its definition, $\psi$ has to be an atomic formula. As ${\mathbf{f}}$ is a formula type, we have that $\varphi\in{\mathbf{f}}$ iff $\neg\varphi\not\in{\mathbf{f}}$. Let us suppose for contradiction that $\psi\not\in{\mathbf{f}}$. Thus, $\neg\psi\in{\mathbf{f}}$. This implies that $\bigwedge{\mathbf{f}}\models\neg\psi$. Thus, as $M\models\bigwedge lit({\mathbf{f}})$, we have that $M\models\neg\psi$. This contradicts the hypothesis that $M\models\psi$. Thus, we conclude that $\psi\in{\mathbf{f}}$. Therefore, $\bigwedge lit({\mathbf{f}})\models\psi$.

Induction Hypothesis: For every formula $\varphi$, if
$degree(\varphi)<degree(\psi)$ and $M\models\varphi$ then $\bigwedge
lif({\mathbf{f}})\models\varphi$.

Induction Step: Let $degree(\psi)>1$. By construction, $\psi$ is of the form
(1) $\varphi\land\varphi^{\prime}$ or (2) $\neg\varphi$, for some ${\cal
ALC}$-formulae $\varphi$ and $\varphi^{\prime}$:

    1. (1) $\psi=\varphi\land\varphi^{\prime}$. From definition, $degree(\varphi\land\varphi^{\prime})=degree(varphi)+degree(\varphi^{\prime})$. Recall from definition of $degree$ that $degree(\beta)>1$, for every formula $\beta$. Therefore, $degree(\varphi)<degree(\varphi\land\psi^{\prime})$ and $degree(\varphi^{\prime})<degree(\varphi\land\varphi^{\prime})$. This means that $degree(\varphi)<degree(\psi)$ and $degree(\varphi^{\prime})<degree(\psi)$. From hypothesis, $M\models\psi=\varphi\land\varphi^{\prime}$. Thus, $M\models\varphi$ and $M\models\psi$. This implies from IH that

$\bigwedge lit({\mathbf{f}})\models\varphi\mbox{ and }\bigwedge
lit({\mathbf{f}})\models\varphi^{\prime}$

Therefore, $\bigwedge
lit({\mathbf{f}})\models\varphi\land\varphi^{\prime}=\psi$.

    2. (2) $\psi=\neg\varphi$. We have two cases, either (i) $\varphi$ is an atomic formula or (ii) $\varphi=(\beta\land\beta^{\prime})$. For the first case, analogous to the base case, we get that $\bigwedge lit({\mathbf{f}})\models\psi$. So we focus only on the second case. From the definition of $degree$, we get that $degree(\neg\beta)<degree(\psi)$ and $degree(\neg beta^{\prime})<degree(\psi)$. As $M\models\psi=\neg(\beta\land\beta^{\prime})$, we get that either (a) $M\models\neg\beta$ or (b) $M\models\neg\beta^{\prime}$.

       * (a) $M\models\neg\beta$. From above, $degree(\neg\beta)<degree(\psi)$. Thus, from IH, we get that $\bigwedge lit({\mathbf{f}})\models\neg\beta$. Thus, $\bigwedge lit({\mathbf{f}})\models\neg(\beta\land\beta^{\prime})=\psi$.

       * (b): $M\models\neg\beta^{\prime}$. Analogous to case (a).

###### Lemma 11

If $M\models\varphi$, ${\mathbf{f}}\in\operatorname{ftypes}({\varphi})$ and
$M\models\bigwedge lit({\mathbf{f}})$ then $\operatorname{Mod}({\bigwedge
lit({\mathbf{f}})})={{[{M}]^{\varphi}}}$.

###### Proof

We need to show that $M^{\prime}\in\operatorname{Mod}({\bigwedge
lit({\mathbf{f}})})$ iff $M^{\prime}\in{{[{M}]^{\varphi}}}$.

  * “$\Rightarrow$”. $M^{\prime}\in\operatorname{Mod}({\bigwedge lit({\mathbf{f}})})$. To show that $M^{\prime}\in{{[{M}]^{\varphi}}}$, it suffices to show that $M^{\prime}\equiv^{\varphi}M$. Let $\psi\in{\mathcal{L}_{lit}({\varphi})}$, we need to show that $M\models\psi$ iff $M\models\psi$.

    * (a) “$\Rightarrow$” $M\models\psi$. From Proposition 1, we have that $\bigwedge lit({\mathbf{f}})\models\psi$. This jointly with $M^{\prime}\models\bigwedge lit({\mathbf{f}})$ implies that $M^{\prime}\models\psi$.

    * (b) “$\Leftarrow$” $M^{\prime}\models\psi$. Analogous to item (a).

  * “$\Leftarrow$” $M^{\prime}\in{{[{M}]^{\varphi}}}$. Note that $\bigwedge lit({\mathbf{f}})\in{\mathcal{L}_{lit}({\varphi})}$. Thus as $M^{\prime}\equiv^{\varphi}M$, and $M\models\bigwedge lit({\mathbf{f}})$, we get that $M^{\prime}\models\bigwedge lit({\mathbf{f}})$.

See 1

###### Proof

We have two cases: either (i) $M\models\varphi$ or (ii)$M\not\models\varphi$.

  1. (i) $M\models\varphi$. Then, from definition of $\operatorname{ex}$, we have that $\operatorname{ex}(\varphi,M)=\varphi$ which implies that $\operatorname{Mod}({\operatorname{ex}(\varphi,M)})=\operatorname{Mod}({\varphi})$. As $M\models\varphi$, we get that ${{[{M}]^{\varphi}}}\subseteq\operatorname{Mod}({\varphi})$. Therefore, $\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}=\operatorname{Mod}({\varphi})$. This implies that

$\operatorname{Mod}({\operatorname{ex}(\varphi,M)})=\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}.$

  2. (ii)$M\not\models\varphi$. Thus, from definition of $\operatorname{ex}$, we get that

$\operatorname{ex}(\varphi,M)=\varphi\lor\bigwedge lit({\mathbf{f}}),\mbox{
where }qm(\neg\varphi,M)=(T,o,{\mathbf{f}}).$

This implies that
$\operatorname{Mod}({\operatorname{ex}(\varphi,M)})=\operatorname{Mod}({\varphi\lor\bigwedge
lit({\mathbf{f}})})$. Note that

$\operatorname{Mod}({\varphi\lor\bigwedge
lit({\mathbf{f}})})=\operatorname{Mod}({\varphi})\cup\operatorname{Mod}({\bigwedge
lit({\mathbf{f}})}).$

As $qm(\neg\varphi,M)=(T,o,{\mathbf{f}})$, it follows from the definition of
$qm$ that ${\mathbf{f}}\in\operatorname{ftypes}({\neg\varphi})$ and
$M\models\bigwedge lit({\mathbf{f}})$. In summary, $M\models\neg\varphi$,
${\mathbf{f}}\in\operatorname{ftypes}({\neg\varphi})$ and $M\models\bigwedge
lit({\mathbf{f}})$. Thus, from Lemma 11, we have that

$\operatorname{Mod}({\bigwedge lit({\mathbf{f}})})={{[{M}]^{\varphi}}}.$

Therefore,

$\operatorname{Mod}({\operatorname{ex}(\varphi,M)})=\operatorname{Mod}({\varphi}){\cup}{{[{M}]^{\varphi}}}.$

See 3.5

###### Proof

We consider each case separately.

  1. (i) $M\models\varphi$. Thus, ${{[{M}]^{\varphi}}}{\subseteq}\ \operatorname{Mod}({\varphi})$ which implies that

$\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}=\operatorname{Mod}({\varphi}).$

Therefore, $\operatorname{ex}^{*}(\varphi,M)\equiv\varphi$.

  2. (ii) $M\not\models\varphi$. Let $qm(\neg\varphi,M)=(T,o,{\mathbf{f}})$. Note that ${\mathbf{f}}\in\operatorname{ftypes}({\varphi})$, and from definition of $qm$ that $M\models\bigwedge lit({\mathbf{f}})$. Thus, it follows from Lemma 11 that $\operatorname{Mod}({\bigwedge lit({\mathbf{f}})})={{[{M}]^{\varphi}}}$. Thus, $\operatorname{Mod}({\varphi\lor\bigwedge qm(\neg\varphi,M)})=\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}$. This means that $\operatorname{ex}^{*}(\varphi,M)\equiv\varphi\lor\bigwedge qm(\neg\varphi,M)$.

See 3.6

###### Proof

First, assume that
$\operatorname{ex}^{*}(\varphi,{M})\equiv\operatorname{ex}(\varphi,{M})$. From
Lemma 1 we have that
$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})=\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$,
hence success and persistence are immediately satisfied. To prove atomic
temperance, assume that
${M}^{\prime}\in\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$ and
that there is a set of models $\mathbb{M}^{\prime}$ with ${M}^{\prime}$ that
is finitely representable in ${\cal ALC}$-formula and such that
$\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}\subseteq\mathbb{M}^{\prime}\subset\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$.
Lemma 1 implies that
$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})=\operatorname{Mod}({\varphi})\cup{{[{M}]^{\varphi}}}$.
Hence, ${M}^{\prime}\not\in{{[{{M}}]^{\varphi}}}$, a contradiction as we
assumed that
$\mathbb{M}^{\prime}\supseteq\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$.
Therefore, no such $\mathbb{M}^{\prime}$ could exist, and thus,
$\operatorname{ex}^{*}$ satisfies atomic temperance.

Let ${M}^{\prime}\equiv^{\varphi}{M}$. Since
$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})=\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$
and ${{[{M^{\prime}}]^{\varphi}}}={{[{M}]^{\varphi}}}$, we have that:
$\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}=\operatorname{Mod}({\varphi})\cup{{[{{M}^{\prime}}]^{\varphi}}}=\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M}^{\prime})})$.
Hence, atomic extensionality is also satisfied.

On the other hand, suppose that $\operatorname{ex}^{*}(\varphi,M)$ satisfies
the postulates stated. Let
${M}^{\prime}\in\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$. If
${M}^{\prime}\in\operatorname{Mod}({\varphi})$ then success ensures that
${M}^{\prime}\in\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$.
Otherwise, we have ${M}^{\prime}\equiv^{\varphi}{M}$, and as consequence of
success and atomic extensionality we also obtain
${M}^{\prime}\in\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$.
Therefore,
$\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}\subseteq\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$.

Now, let
${M}^{\prime}\in\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$ and
assume that
${M}^{\prime}\not\in\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$.
Success, persistence and atomic extensionality imply that
$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})$. Atomic temperance
states that there is no set of models $\mathbb{M}^{\prime}$ that is finitely
representable in ${\cal ALC}$-formula with
$\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}\subseteq\mathbb{M}^{\prime}\subset\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})\cup\\{{M}\\}$.
But we know from Lemma 1 that
$\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$ is finitely
representable in ${\cal ALC}$-formula and does not include ${M}^{\prime}$ by
assumption, a contradiction. Thus, no such ${M}^{\prime}$ could exist and
$\operatorname{Mod}({\operatorname{ex}^{*}(\varphi,{M})})\subseteq\operatorname{Mod}({\varphi})\cup{{[{{M}}]^{\varphi}}}$.

Hence, Lemma 1 yields
$\operatorname{ex}^{*}(\varphi,{M})\equiv\operatorname{ex}(\varphi,{M})$.