=Paper=
{{Paper
|id=None
|storemode=property
|title=Craig interpolation on the logic of knowledge
|pdfUrl=https://ceur-ws.org/Vol-2264/paper2.pdf
|volume=Vol-2264
|authors=Everardo Bárcenas,José-de-Jesús Lavalle-Martínez,Guillermo Molero-Castillo,Alejandro Velázquez-Mena
|dblpUrl=https://dblp.org/rec/conf/lanmr/BarcenasLMV18
}}
==Craig interpolation on the logic of knowledge==
https://ceur-ws.org/Vol-2264/paper2.pdf
Craig Interpolation on the Logic of Knowledge
Everardo Bárcenas1 , José-de-Jesús Lavalle-Martínez2 , Guillermo Molero-Castillo3,4 ,
and Alejandro Velázquez-Mena1
1
Universidad Nacional Autónoma de México
[barcenas,mena]@fi-b.unam.mx
2
Benemérita Universidad Autónoma de Puebla
jlavalle@cs.buap.mx
3
Consejo Nacional de Ciencia y Tecnología
4
Universidad Veracruzana
ggmoleroca@conacyt.mx
Abstract. The Craig interpolation property is described as follows: if a formula
φ implies another formula ψ, then there is a formula β in the common language
of φ and ψ, such that φ also implies β, as well as β implies ψ. In this paper,
we provide a constructive proof of the Craig interpolation property on the modal
logic of knowledge Km . The proof is based on the application of the Maehara
technique on a tree-hypersequent calculus. We also show, as a consequence of
the interpolation property, Beth definability and Robinson joint consistency .
1 Introduction
Philosophy and Artificial Intelligence have been the traditional study framework to rea-
son about knowledge [12]. More recently, reasoning about knowledge has become of
much importance in many areas of computer science, such as distributed systems, cryp-
tography, natural language processing and databases [8]. In this paper, we consider
as a formal framework to study knowledge, the basic modal logic of knowledge, also
known as the multi-modal logic Km . This logic has been shown to be mathematically
well-founded [11]. As consequence of being a bisimulation invariant fragment of first
order logic, Km posses a nice balance of expressiveness and reasoning efficiency [3].
The interpolation property was first proved for classical first order logic by Craig [6].
Considering a formula φ implies another formula ψ, the interpolation property consists
in the existence of a formula β, called the interpolant, in the common language of
φ and β, which is assumed to be non-empty, such that φ implies β, and β implies ψ.
Some logical consequences of interpolation are Beth definability [1] and Robinson joint
consistency [22]. Applications of interpolation in computer science have been recently
studied for formal verification [18], computational complexity [5], and knowledge rep-
resentation [13, 4], among others.
In this paper, we give a constructive proof the Craig interpolation theorem for the
modal logic of knowledge Km . The proof implies a straightforward algorithm to com-
pute interpolants.
15
1.1 Related work
Early studies about the interpolation property in modal logics are reported in [10, 16].
In [10], Gabbay proved interpolation for several mono-modal logics including K and
S4. Maksimova in [16] indentifies a close conection of amalgamability of modal logics
containing S4, and proved that only a finite number modal logics conaining S4 enjoys
interpolation. Maksimova later proved in [15] interpolation of all normal modal log-
ics via amalgamation. This result was extended for multi-modal logics in [14]. Marx
proved interpolation in [17] for several modal logics with bisimulation. This work in-
cludes interpolation proofs for K, fibered modal logics and the multi-modal logics of
knowledge and belief. In all the above works, interpolation is proved by semantics meth-
ods. Although these methods are quite general and can be applied to several logics, they
not provide an explicit construction of interpolants. In the current paper, we provide a
syntactic proof of interpolation for the multi-modal logic Km . This proof includes an
explicit construction of interpolants.
Syntactic interpolation proofs for modal logics KB, KDB, K5 and KD5 are de-
scribed in [20]. In this work, interpolation is proved by means of a cut-free complete
sequent-like tableau deduction system. Constructive interpolation for modal logics K
and T is given in [2]. More precisely, a stronger form of interpolation, called uniform
interpolation, is proved in this work. In uniform interpolation, interpolants are com-
posed by the common language language of formulas in the implication, but restricted
by a choice of propositional variables. The closest work to our paper is [9]. In this work,
constructive interpolation is proved for the entire modal cube, composed by the logics
resulting from any combination of K, D, T , B, 5 and 4. The proof technique used in
this work is based on nested sequents. In our paper, we obtain a constructive interpo-
lation proof for the multi-modal logic Km , using the Maehara technique on a cut-free
complete tree-hypersequent calculus.
In [7], D’Agostino reports an extensive survey on interpolation for non-classical
logics, including modal logics.
1.2 Outline
We first introduce the multi-modal logic of knowledge Km in Section 2. In Section 3,
we describe a complete cut-free tree-hypersequent calculus for Km . Then, in Section 4,
by means of Maehara technique, we extract interpolants from tree-hypersequent proofs
of Km implications. In Section 5, as a consequence of interpolation, we also prove Beth
definability and Robinson joint consistency. Finally, in Section 6, we give a summary
of the article and briefly argue further research perspectives.
2 Logic of Knowledge
We assume a basic modal language: a non-empty set of propositions PROP; and a non-
empty finite set of modalities MOD.
The set of formulas is inductively defined by the following grammar.
φ := p | ¬φ | φ ∧ φ | 2m φ
16
where p is a proposition and m is a modality.
Notation:
> := p ∨ ¬p ⊥ := ¬>
φ ∨ ψ := ¬(¬φ ∧ ¬ψ) φ → ψ := ¬φ ∨ ψ
3m φ := ¬2m ¬φ
A Kripke structure is a tuple M = (W, R, V ) where:
– W is a non-empty set called domain;
– R is a finite set of binary relations Rm : W × W , for every modality m; and
– V : PROP 7→ 2W is valuation function mapping propositions to domain subsets.
Given a Kripke structure M = (W, R, V ), formulas are interpreted as follows:
M
[[p]] = {w ∈ V (p)}
M M
[[¬φ]] =W \ [[φ]]
M M M
[[φ ∧ ψ]] = [[φ]] ∩ [[ψ]]
M
[[2m φ]] = {w | ∀w0 ∈ W : if (w, w0 ) ∈ Rm ,
o
M
then w0 ∈ [[φ]]
M
We may also write M, w |= φ instead of w ∈ [[φ]] , M |= φ when for every w in
M , we have that M, w |= φ, in which case we say M is a model of φ. If any Kripke
structure is a model of φ, we write |= φ.
Definition 1 (Hilbert derivation system). We define the derivation system H by the
following schemas and rules, for each m ∈ MOD:
A1 φ → (ψ → φ)
A2 (φ → (ψ → β)) → ((φ → ψ) → (φ → β))
A3 (¬φ → ¬ψ) → (ψ → φ)
A4 2m (φ → ψ) → (2m φ → 2m ψ)
φ→ψ φ
R1
ψ
φ
R2
2m φ
We say a formula φn is derivable from H, written `H φn , if there is a sequence
φ1 , φ2 , . . . , φn , such that for each i ∈ {1, . . . , n}:
– φi is either an instance, up to substitution, of a schema in H, or
– there is (are) j < i (and k < i) such that φi and φj (and φk ) are instances of the
conclusion and premises, resp, of a rule in H.
Consider for instance the following derivation of 2m (φ ∧ ψ) → 2m φ:
1. (φ ∧ ψ) → φ, which by notation is an instance of A1 , ¬φ ∨ ψ ∨ φ;
2. 2m ((φ ∧ ψ) → φ), from 1 by R2 ;
3. 2m ((φ ∧ ψ) → φ) → (2m (φ ∧ ψ) → 2m φ), from A4 ; and
4. 2m (φ ∧ ψ) → 2m φ, from 2 and 3 by R1 .
Theorem 1 (Correctness [11]). For any formula φ, `H φ, if and only if, |= φ.
17
3 Tree-hypersequents
A sequent is an expression Γ ` ∆, where Γ and ∆ are formula multisets, non-empty
and finite. Intuitively, a sequent Γ ` ∆ is interpreted, in terms of logical symbols, as an
implication, where the antecedent is composed by the disjunction of formulas in Γ , and
the consequent is the conjunction of formulas in ∆. We then the define the following
interpretation function:
n
^ k
_
(φ1 , . . . , φn ` ψ1 , . . . , ψk )I := φi → ψj
i=1 j=1
where n and k are some positive integers.
In sequents, we often write φ, Γ or Γ, φ instead of {φ} ∪ Γ , also ` ∆ instead of
> ` ∆, and Γ ` in place of Γ ` ⊥.
Tree hypersequents expressions are inductively defined by the following grammar:
T :=S [ST ]
ST :=∅ | m : T, ST
where S is a sequent and m is a modality. We extend the interpretation function of
sequents for tree hypersequents as follows:
(S [ST ])I :=S I ∨ (ST )I
(∅)I :=⊥
(m : T, ST )I :=2m T I ∨ (ST )I
When clear from context, we often write tree instead of tree hypersequent. It is
usually written S instead of S [∅], also if S is Γ ` ∆, we write φ, S and S, φ instead of
φ, Γ ` ∆ and Γ ` φ, ∆, respectively.
We write T hSi when a sequent S occurs in a tree T , more precisely:
– S [ST ] hSi;
– S 0 [ST ] hSi, provided that S 0 is different than S and ST hSi; and
– (m : T 0 , ST ) hSi, when either T 0 hSi or ST hSi.
We extend the occurring relation T hT 0 i between trees as expected:
– T and T 0 are the same;
– (S [ST ]) hT 0 i, when ST hT 0 i;
– (m : T 0 , ST 0 ) hT 0 i; and
– (m : T 00 , ST 0 ) hT 0 i, provided that T 00 is different than T 0 and ST 0 hT 0 i.
We also distinguish when m : T 0 occurs in a tree T , written T hm : T 0 i:
– (S [ST ]) hm : T 0 i, when ST hm : T 0 i;
– (m : T 0 , ST 0 ) hm : T 0 i; and
– (m0 : T 00 , ST 0 ) hT 0 i, provided that either m is different than m0 or T 00 is different
than T 0 , and ST 0 hm : T 0 i.
18
We say a sequent S occurs, under a modality m, in a finite sequence of tree hyperse-
quents m1 : T1 , m2 : T2 , . . . , mk : Tk , when there is an i such that mi is m and Ti has
the form S [ST ]. Moreover, we often write S [m : S 0 ] instead of S [ST ], provided S 0
occurs under m in ST .
Definition 2 (Tree-hypersequents derivation system). The inference system for tree
hypersequents G is defined as follows.
– Initial tree hypersequents:
T hp, S, pi
– Propositional rules:
T hS, φi T hφ, Si
¬L ¬R
T h¬φ, Si T hS, ¬φi
T hφ, ψ, Si T hS, φi T hS, ψi
∧L ∧R
T hφ ∧ ψ, Si T hS, φ ∧ ψi
– Modal rules:
T h2m φ, S [m : φ, S 0 ]i
2m L
T h2m φ, S [m : S 0 ]i
T hS [m : ` φ, ST ]i
2m R
T hS, 2m φ [ST ]i
We now define the concept of derivation tree:
– any
0
rule (up
0
to00subtitution) of G is a derivation tree;
– TT and T T T are derivation trees, provided that T 0 and T 00 are derivation trees,
and
T0 T0 T 00
– T0 and 0 T 0 are rules in G and T00 and T000 are the lowest tree hypersequents
occurring in T 0 and T 00 .
If all the branches of a derivation tree, where T is the lowest tree hypersequent, are
finite and ends with an initial tree hypersequent, then we say the derivation tree is a
proof tree, or simply a proof, of T , or that T is derivable in G, and we write `G T .
Consider now for instance the following proof of A4 :
T hφ, ψ ` ψi
¬R
T hφ ` ψ, φi T hφ ` ψ, ¬ψi
∧R
T hφ ` ψ, φ ∧ ¬ψi
¬L
2m ¬(φ ∧ ¬ψ), 2m φ ` [m : ¬(φ ∧ ¬ψ), φ ` ψ]
2m L
2m ¬(φ ∧ ¬ψ), 2m φ ` [m : φ ` ψ]
2m L
2m ¬(φ ∧ ¬ψ), 2m φ ` [m : ` ψ]
2m R
2m ¬(φ ∧ ¬ψ), 2m φ ` 2m ψ
¬L
2m ¬(φ ∧ ¬ψ), 2m φ, ¬2m ψ `
∧L
2m ¬(φ ∧ ¬ψ) ∧ 2m φ ∧ ¬2m ψ `
¬R
` ¬(2m ¬(φ ∧ ¬ψ) ∧ 2m φ ∧ ¬2m ψ)
Theorem 2 ([21, 19]). For any sequent S, `G S, if and only if, `H S.
Corollary 1. For any sequent S, `G S, if and only if, |= S I .
19
4 Interpolation
We define the set of non-logical symbols Sym(φ) of a formula φ as follows:
– Sym(p) = {p};
– Sym(¬φ) = Sym(φ);
– Sym(φ ∧ ψ) = Sym(φ) ∪ Sym(ψ); and
– Sym(2m φ) = {m} ∪ Sym(φ).
The set of non-logical symbols of a (multi-)set of formulas is defined as expected.
For technical convenience, we consider an equivalent extension G0 of the derivation
system G, where formulas > are considered per se (not as notation). All rules in G are
also in G0 . Additionally, the initial sequent T hS, >i is also included in G0 .
Lemma 1 (Maehara’s Lemma). Let T hΓ ` ∆i be derivable in G, and let Γ1 , Γ2 and
∆1 , ∆2 be partitions of Γ and ∆, respectively. Then there is a formula β, called the
interpolant, such that T hΓ1 ` ∆1 , βi and T hβ, Γ2 ` ∆2 i are derivable in G0 , and
Sym(β) ⊆ (Sym(Γ1 ) ∪ Sym(∆1 )) ∩ (Sym(Γ2 ) ∪ Sym(∆2 )).
Proof. By induction on the height of the proof tree.
The base case is T hp, Γ ` ∆, pi. The interpolant β is then defined according to the
occurrence of propositions p in partitions:
T hp, Γ1 ` ∆1 , p, ¬>i T h¬>, Γ2 ` ∆2 i
T hΓ1 ` ∆1 , >i T h>, p, Γ2 ` p, ∆2 i
T hp, Γ1 ` ∆1 , pi T hp, Γ2 ` ∆2 , pi
T hΓ1 ` ∆1 , p, ¬pi T h¬p, p, Γ2 ` ∆2 i
Induction step. Assume the last inference is the following:
T hΓ ` ∆, φi T hΓ ` ∆, ψi
T hΓ ` ∆, φ ∧ ψi
By induction hypothesis, there are interpolants β1 and β2 for the upper tree hyper-
sequents. There are two possible cases according the occurrence of φ and ψ in the
respective partitions.
T hΓ1 ` ∆1 , φ, β1 i T hβ1 , Γ2 ` ∆2 i
T hΓ1 ` ∆1 , ψ, β2 i T hβ2 , Γ2 ` ∆2 i
T hΓ1 ` ∆1 , β1 i T hβ1 , Γ2 ` ∆2 , φi
T hΓ1 ` ∆1 , β2 i T hβ2 , Γ2 ` ∆2 , ψi
Depending on the occurrence of φ∧ψ in the partitions, we then construct the interpolant
φ as follows:
T hΓ1 ` ∆1 , φ ∧ ψ, β1 ∨ β2 i
T hβ1 ∨ β2 , Γ2 ` ∆2 i
T hΓ1 ` ∆1 , β1 ∧ β2 i
T hβ1 ∧ β2 , Γ2 ` ∆2 , φ ∧ ψi
In the induction step, now consider the last inference is
20
T h2m φ, Γ ` ∆ [m : φ, Γ 0 ` ∆0 ]i
T h2m φ, Γ ` ∆ [m : Γ 0 ` ∆0 ]i
By induction, there is an interpolant β for the upper tree hypersequent. By the occur-
rence of 2m φ in partitions, we distinguish two cases:
T h2m φ, Γ1 ` ∆1 , β [m : φ, Γ 0 ` ∆0 ]i
T hβ, Γ2 ` ∆2 [m : φ, Γ 0 ` ∆0 ]i
T hΓ1 ` ∆1 , β [m : φ, Γ 0 ` ∆0 ]i
T hβ, 2m φ, Γ2 ` ∆2 [m : φ, Γ 0 ` ∆0 ]i
We then construct the following interpolants:
T h2m φ, Γ1 ` ∆1 , 2m φ ∧ β [m : Γ 0 ` ∆0 ]i
T h2m φ ∧ β, Γ2 ` ∆2 [m : Γ 0 ` ∆0 ]i
T hΓ1 ` ∆1 , ¬2m φ ∨ β [m : Γ 0 ` ∆0 ]i
T h¬2m φ ∨ β, 2m φ, Γ2 ` ∆2 [m : Γ 0 ` ∆0 ]i
Consider now the last inference is the following:
T hΓ ` ∆ [m : ` φ, ST ]i
T hΓ ` ∆, 2m φ [ST ]i
We obtain the following interpolant β by induction:
T hΓ1 ` ∆1 , β [m : ` φ, ST ]i
T hβ, Γ2 ` ∆2 [m : ` φ, ST ]i
There are then two cases depending on the occurrence of 2m φ in partitions:
T hΓ1 ` ∆1 , 2m φ, ¬2m φ ∧ β [ST ]i
T h¬2m φ ∧ β, Γ2 ` ∆2 [ST ]i
T hΓ1 ` ∆1 , 2m φ ∨ β [ST ]i
T h2m φ ∨ β, Γ2 ` ∆2 , 2m φ [ST ]i
Theorem 3 (Craig Interpolation). For any two formulas φ and ψ, if |= φ → ψ, then
there is a formula β, such that |= φ → β, |= β → ψ and Sym(β) ⊆ Sym(φ) ∩
Sym(β), provided that there is a proposition p such that p ∈ Sym(φ) ∩ Sym(β).
Proof. Assume |= φ → ψ, then by Corollary 1, φ ` ψ is derivable in G. By Lemma 1,
there is a formula β, such that φ ` β and β ` φ are derivable in G0 . Let p ∈
Sym(φ) ∩ Sym(β). Now, let β 0 be obtained from β by replacing > by ¬(p ∧ ¬p).
It is straightforward that φ ` β and β ` φ are derivable in G, and hence (by Corol-
lary 1) |= φ → β and |= β → ψ.
21
5 Definability and Consistency
Definition 3 (Implicit definability). Let φ(p, p1 , . . . , pk ) be a formula, where p, p1 , . . . , pk
are propositions occurring in it. We say φ(p, p1 , . . . , pk ) defines p implicitly if
|= (φ(p, p1 , . . . , pk ) ∧ φ(p0 , p1 , . . . , pk )) → (p ↔ p0 )
where p 6= p0 .
Definition 4 (Explicit definability). Let φ(p, p1 , . . . , pk ) be a formula, where p, p1 , . . . , pk
are propositions occurring in it. We say φ(p, p1 , . . . , pk ) defines p explicitly, when
|= φ(p, p1 , . . . , pk ) → (p ↔ ψ)
where Sym(ψ) ⊆ Sym(φ(p, p1 , . . . , pk )) \ {p}.
Theorem 4 (Beth Definability). Let φ(p, p1 , . . . , pk ) be a formula, where p, p1 , . . . , pk
are propositions occurring in it. If φ(p, p1 , . . . , pk ) defines p implicitly, then φ(p, p1 , . . . , pk )
defines p explicitly.
Proof. From the implicit definability assumption, it is easy to see that
|= (φ(p, p1 , . . . , pk ) ∧ p) → (φ(p0 , p1 , . . . , pk ) → p0 )
By the Craig Interpolation Theorem 3, we then obtain
|= (φ(p, p1 , . . . , pk ) ∧ p) → ψ
|= ψ → (φ(p0 , p1 , . . . , pk ) → p0 )
where Sym(ψ) ⊆ Sym(φ(p, p1 , . . . , pk )) \ {p}.
Before definining the notion of consistency, we need a precise description of some
concepts. An axiom system is a finite set of formulas. An axiom sequence is a (possibly
empty) subset of an axiom system. We say a sequent S is derivable (provable) in G
from an axiom system A, if there is an axiom sequence A0 of A, such that `G A0 , S.
Definition 5 (Consistency). An axiom system is inconsistent if the empty sequent is
derivable from it. We say an axiom system is consistent if it is not inconsistent.
Theorem 5 (Robinson Joint Consistency). Consider two consistent axiom systems A1
and A2 , if for any formula φ, such that Sym(φ) ⊆ Sym(A1 ) ∩ Sym(A2 ), it is not the
case that both φ and ¬φ are derivable from A1 and A2 (or A2 and A1 ), respectively,
then A1 ∪ A2 is consistent.
Proof. We prove the contrapositive. If A1 ∪ A2 is not consistent, then there are two
axiom sequences A01 and A02 of A1 and A2 , resp., such that A1 , A2 ` are derivable
in G. Recall each A1 and A2 is consistent, then not empty. By Lemma 1, there is an
interpolant φ, where Sym(φ) ⊆ Sym(A1 ) ∩ Sym(A2 ), such that A1 ` φ and φ, A2 `
(hence A2 ` ¬φ) are both derivable in G0 . As in the proof of Theorem 3, it is straight
forward that both A1 ` φ and A2 ` ¬φ are also derivable in G by replaceing all the
occurrences of > in φ by ¬(p ∧ ¬p) for a p ∈ Sym(A1 ) ∪ Sym(A2 ).
22
6 Conclusions
In this paper, we describe a constructive proof of the Craig interpolation property. The
proof is based on the Maehara technique on a complete cut-free tree-hypersequent cal-
culus. An interpolant algorithm can easily be inferred from the proof. A complexity
analysis of this algorithm is prospected as further research. We are also interested in
constructive interpolation proofs for other more expressive modal logics, such as Km
with converse, CTL and the µ-calculus.
References
1. Beth, E.W.: On Padoa’s method in the theory of definition. Journal of Symbolic Logic 21(2)
(1956)
2. Bílková, M.: Uniform interpolation and propositional quantifiers in modal logics. Studia
Logica 85(1) (2007)
3. Blackburn, P., Benthem, J.F.A.K.v., Wolter, F.: Handbook of Modal Logic, Volume 3 (Studies
in Logic and Practical Reasoning). Elsevier Science Inc., New York, NY, USA (2006)
4. ten Cate, B., Franconi, E., Seylan, I.: Beth definability in expressive description logics. J.
Artif. Intell. Res. 48 (2013)
5. Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb.
Log. 44(1) (1979)
6. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof
theory. J. Symb. Log. 22(3) (1957)
7. D’Agostino, G.: Interpolation in non-classical logics. Synthese 164(3) (2008)
8. Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press,
Cambridge, MA, USA (2003)
9. Fitting, M., Kuznets, R.: Modal interpolation via nested sequents. Ann. Pure Appl. Logic
166(3) (2015)
10. Gabbay, D.M.: Craig’s interpolation theorem for modal logics. In: Hodges, W. (ed.) Confer-
ence in Mathematical Logic — London ’70. Lecture Notes in Mathematics. Springer (1972)
11. Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowl-
edge and belief. Artif. Intell. 54(2) (1992)
12. Hintikka, J.: Knowledge and Belief. Ithaca: Cornell University Press (1962)
13. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expressive de-
scription logics. In: Walsh, T. (ed.) IJCAI, Proceedings of the 22nd International Joint Con-
ference on Artificial Intelligence. IJCAI/AAAI (2011)
14. Madarász, J.X.: The Craig interpolation theorem in multi-modal logics. Bulletin of the Sec-
tion of Logic 3(24) (1995)
15. Maksimova, L.: Amalgamation and interpolation in normal modal logics. Studia Logica
50(3-4) (1991)
16. Maksimova, L.L.: Interpolation theorems in modal logics and amalgamable varieties of topo-
logical boolean algebras. Algebra and Logic 18(5) (1979)
17. Marx, M.: Interpolation in modal logic. In: Haeberer, A.M. (ed.) Algebraic Methodology and
Software Technology, 7th International Conference, AMAST, Proceedings. Lecture Notes in
Computer Science, vol. 1548. Springer (1998)
18. McMillan, K.L.: Interpolation and model checking. In: Clarke, E.M., Henzinger, T.A., Veith,
H., Bloem, R. (eds.) Handbook of Model Checking. Springer (2018)
23
19. Munoz-Toriz, J.P., Bárcenas, E., Martínez-Ruiz, I., Arrazola-Ramírez, J.R.E.: (Hy-
per)sequent calculi for the ALC(S4) description logics. Computación y Sistemas 20(1)
(2016)
20. Nguyen, L.A.: Analytic tableau systems and interpolation for the modal logics kb, kdb, k5,
KD5. Studia Logica 69(1) (2001)
21. Poggiolesi, F.: Sequent calculi for modal logic. Ph.D. thesis, Università degli Studi di
Firenze, Université Paris I Panthéon-Sorbonne (2008)
22. Robinson, A.: A result on consistency and its application to the theory of definition. Journal
of Symbolic Logic 25(2) (1960)
24