=Paper=
{{Paper
|id=Vol-3009/paper1
|storemode=property
|title=Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn
|pdfUrl=https://ceur-ws.org/Vol-3009/paper1.pdf
|volume=Vol-3009
|authors=Ruba Alassaf,Renate A. Schmidt,Uli Sattler
|dblpUrl=https://dblp.org/rec/conf/kr/AlassafSS21
}}
==Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn==
https://ceur-ws.org/Vol-3009/paper1.pdf
Resolution-Based Uniform Interpolation for
Multi-Agent Modal Logic Kn
Ruba Alassaf , Renate A. Schmidt , and Uli Sattler
University of Manchester, UK
{ruba.alassaf,renate.schmidt,uli.sattler}@manchester.ac.uk
Abstract. Research on uniform interpolation in modal logic has been
largely focused on the theoretical investigation of the problem. This pa-
per presents a system to compute uniform interpolants for a locally sat-
isfiable formula in the multi-agent modal logic Kn . The system is based
on a direct resolution approach. The idea of the system is that given a
formula φ and a signature as input, it computes the strongest local con-
sequence of φ over the input signature. We have shown that the system
is guaranteed to terminate, soundness and completeness can be shown
using model-theoretic proofs, and the worst-case space complexity bound
is double exponential. We illustrate how the system is used via examples.
Keywords: Uniform Interpolation · Resolution · Modal logic · Kn .
1 Introduction
Uniform interpolation is the task of computing a formula that captures all log-
ical consequences up to a given signature for a given formula. The problem of
computing a uniform interpolant is generally not decidable. We are interested in
logics that have the uniform interpolation property: that is, the property that
for any formula φ and any signature Σ, a uniform interpolant for φ over Σ exists
in the logic.
Uniform interpolation amounts to the second-order quantifier elimination
problem: given a formula with an existential second-order quantifier prefix, the
process of eliminating the second-order quantifiers is essentially the process of
producing a formula that does not contain the symbols that are being quantified.
A related notion is Craig interpolation. A logic has the Craig interpolation
property if given two formulas φ and ψ with a shared signature Σ such that
φ → ψ holds, there exists a middle formula φ0 such that φ → φ0 and φ0 → ψ
hold. A uniform interpolation method can be used to compute Craig interpolants
by performing uniform interpolation to keep the shared signature Σ.
The importance of having uniform interpolation methods stems from the
significant potential it has for applications. For example, in agent-based appli-
cations, it is often assumed that agents communicate using the same language.
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
16 Ruba Alassaf, Renate A. Schmidt and Uli Sattler
Uniform interpolation becomes very useful when this assumption is relaxed; it
can be used to allow an agent to express knowledge about a certain topic by
computing a view that only uses some signature symbols. This gives agents the
ability to share their knowledge with other agents who specialise in different
domains.
The modal logic community has focused on uncovering theoretical results. It
has been shown via constructive proofs that the modal logic K has the uniform
interpolation property [7, 14]. An approach to constructing uniform interpolants
was given in [2] for the modal logics K and T . Wolter [15] proved that the modal
logic S5 has the uniform interpolation property, and that uniform interpolation
for any normal single-agent modal logic can be generalised to its multi-agent case.
Recently, it was shown that K45n and KD45n have the uniform interpolation
property in [4]. It is known that S4 and K4 do not have the uniform interpolation
property [8].
This paper presents the first complete resolution-based system for computing
uniform interpolants in the multi-agent modal logic Kn . As far as the authors
know, the only other paper which considers this logic is [4]. Different from our
method, they construct a uniform interpolant by considering canonical formulas,
which are conceptually simple but, as the authors explicitly state, inefficient to
compute [4]. We show that our system has double exponential worst-case space
complexity. We prove that the termination of our method is guaranteed, and that
it is sound and complete. We are the first to use bisimulations to prove com-
pleteness for a resolution-based uniform interpolation system. We illustrate how
the method is used via examples. Due to the lack of space, proof are provided in
the full version of the paper which can be found here: https://personalpages.
manchester.ac.uk/staff/ruba.alassaf/publications.html
2 Preliminaries
We assume the reader is familiar with the multi-modal logic Kn [5, 10]. We use
F = (W, R) to denote a Kripke frame and M = (W, R, V ) to denote a Kripke
model. A formula φ is (locally) satisfiable in a model M, denoted M, w |= φ,
if there is a point w in W at which φ is true. A formula φ is (unconditionally)
satisfiable if it is true at some point in some model. A formula φ is globally
satisfied (or true) in a model M, denoted M |= φ, if it is true at every w in M.
A formula φ is valid if it is satisfied in all models over any frame F. A set of
formulae N is globally satisfied by a model M, denoted M |= N , if for each
formula φ in N , M globally satisfies φ.
We are interested in the problem of computing a uniform interpolant of a
locally satisfiable formula and a signature.
Definition 1 (Uniform Interpolation). Given a formula φ, a uniform inter-
polant of φ with respect to a signature Σ of propositional symbols is a formula φ0
such that:
1. φ0 does not contain symbols outside of Σ, and
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 17
2. for any modal formula ψ over Σ, we have that for all models M, M |= φ → ψ
iff for all models M, M |= φ0 → ψ.
3 Related Work
In this section, we outline the methods we found related to our method, and
explain how our method is different to these systems. A summary of the related
methods is given in Table 1. In the table, we give the logic over which each
method is defined, the expressivity of the input and output, and we state if the
method is complete.
The first method is a uniform interpolation algorithm of Bilkova [2]. In her
work, she describes an approach for constructing a uniform interpolant from
a table. She uses a sequent calculus to prove that her algorithm is sound and
complete.
The second is a resolution-based calculus introduced in Herzig and Men-
gin [9]. There are two differences to our method, the first is that the method
proposed by the present paper is for Kn which is an extension of K, and the
second is that we use a kind of labelling technique that allows us to flatten the
input and apply resolution almost classically.
There are three more resolution-based systems for computing uniform inter-
polation: the Scan approach [6] for first-order logic, and the Lethe system [11]
and the system of Ludwig and Konev [12], both for description logics. These
systems are designed for logics where a solution does not always exist. In the
case of Scan, the computation may not terminate [6]. In the case of Lethe,
nominals/definer symbols may remain in the solution [11], or solutions may be
approximated by a depth bound as in the method in [12]. We prove that a
solution is always achievable via our method in a finite number of steps and
without extending the logic or the signature. The completeness proofs provided
for these methods are based on consequence finding, whereas our proof uses
bisimulations. Moreover, compared to [11], the method we describe does not use
unification-based reasoning.
Finally, second-order quantifier elimination methods which can be used to
compute uniform interpolants often use Ackermann’s lemma [1]. Such methods
include the DLS algorithm [3] for second-order quantifier elimination of first-
order logic formulae, the MA system [13] for computing frame correspondence
properties for modal axioms and the Fame tool [16] computing semantic forget-
ting in description logic.
4 Uniform Interpolation Method U IKn for Kn
We start with a high-level description of our uniform interpolation system for
multi-modal logic Kn .
18 Ruba Alassaf, Renate A. Schmidt and Uli Sattler
U IKn Bilkova [2] Herzig Scan [6] Lethe [11] Ludwig DLS
& Mengin [9] & Konev [12] algorithm [3]
Logic Modal Modal Modal First-order Description Description First-order
logic logic logic logic logic logic logic
Method Resolution Sequent Resolution Resolution Resolution Resolution Ackermann
Input Kn (locally K (locally K (locally Full ALC ALC Full
Language satisfiable satisfiable satisfiable first-order (T box (T box) first-order
formula) formula) formula) logic +Abox) logic
Output Kn (locally K (locally K (locally Full ALCOµ ALC Full
Language satisfiable satisfiable satisfiable first-order (T box (T box) first-order
formula) formula) formula) logic +Abox) logic
Complete Yes Yes Yes No Yes No No
Table 1: A comparison between our method U IKn for Kn and related methods.
4.1 Overview
The calculus is based on resolution, with adaptations for modal logic. The idea
behind our approach is the following: for each symbol x outside the given sig-
nature Σ, we generate a sufficient set of conclusions for the given formula and
subsequently eliminate any formulae that contain x. We repeat the process for
all propositional symbols outside Σ.
The calculus uses special world symbols, or W -symbols for short, which are
propositional symbols that help in two related ways:
1. They are used to flatten the input formula to surface some parts of it. E.g.,
2(ψ ∨ 3φ) becomes 2W1 , W1 ⇒ ψ ∨ 3W2 and W2 ⇒ φ.
2. They allow our rules to detect legal inferences between the subformulae by
labelling them with a W -symbol. E.g., 2(x ∧ (¬x ∨ p)) becomes 2W , W ⇒ x
and W ⇒ ¬x ∨ p. Later on, we see that one of our rules allows us to apply
a resolution step on x.
The idea behind using W -symbols is similar to using constants in a labelled
tableau algorithm.
For a formula φ, a signature Σ, and an ordering over the symbols outside
the input signature Σ, the calculus is provided a clause set N0 = {W0 ⇒ φ} as
input, and applies its rules exhaustively to the formulae in the set until no rule
can be applied, resulting in a clause set of the form Nn = {W0 ⇒ φ1 , ..., W0 ⇒
φm }. The formula φ0 = φ1 ∧ . . . ∧ φm is then a uniform Σ-interpolant of φ, which
is proved later.
The role of W0 is to capture a specific world that satisfies φ. Any model M
that satisfies φ at point w can be extended to one that satisfies W0 and W0 ⇒ φ
in a non-vacuous way by setting w ∈ V (W0 ). In this extended model, W0 ⇒ φ
is globally and witnessed as non-vacuously true.
The process of constructing a uniform interpolant is iterative with respect to
the symbols outside Σ, and the ordering fixes the order in which these symbols
are eliminated. For some uniform interpolation problems, a good ordering may
allow the calculus to solve a problem in far fewer steps. For simplicity, and since
the ordering does not improve any worst-case complexity results, we can assume
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 19
that this ordering is arbitrary. We use x to denote the maximal propositional
symbol occurring in the current clause set Ni .
4.2 The Calculus
The rules of our uniform interpolant calculus are given in Figures 1, 2 and 3. Each
rule has a premise, some conditions and a conclusion. The rules are structured
with the premise above a horizontal line and the conclusion below it. The premise
(respectively conclusion) can be one or more clauses depending on which rule is
being applied. There are three types of rules in the calculus: preprocessing rules,
resolution rules, and elimination rules.
The preprocessing rules and the elimination rules are replacement rules; they
replace the premise in the current working clause set with the conclusion. The
resolution rules are saturation rules; they keep the premise and extend the clause
set with the conclusion. The rules can be applied in any order as long as the
conditions for each rule are met.
Generally, we can expect that for a formula in the clause set, it is preprocessed
into another formula, or formulae, that is then involved in a few resolution rule
applications and subsequently purified, if an elimination rule is applicable.
The clauses obtained and handled by our calculus are in a normal form.
They are all labelled with a W -symbol in the condition of the implication. We
can have a formula or another W -symbol in the consequence of the implication.
Concretely, for some W -symbols Wi and Wj , and some modal formula ψ, a clause
can be in the form
Wi ⇒ ψ or Wi ⇒ Wj .
If ψ is a disjunction of modal formulas, we assume that it is a set, i.e., there is
no repetition. This is essential for the correctness of the method. We use ⇒, in
contrast to →, to distinguish an implication that is generated by our system, to
maintain our normal form, from an implication provided as part of the input.
Semantically, they are identical.
To describe the different types of W -symbols, we introduce some terminology
and the function Corr which will be used in the conditions of our system, and
later on in the proofs.
Definition 2. Given a set N of clauses, the set Sw is the set of W -symbols
introduced for subformulas appearing under a modal operator via the world in-
troduction rule. We call these symbols base W -symbols.
The set Cw is the set of W -symbols introduced by the 2# rule. We call these
symbols combinatory W -symbols.
We define a function Corr that maps W -symbols to subsets of Sw as follows:
{Wi }, if Wi ∈ Sw
Corr(W ) ∪ Corr(W ), if W ∈ C where W and W come
n m i w n m
Corr(Wi ) =
from the premise of the Res 2#
rule that has introduced Wi .
20 Ruba Alassaf, Renate A. Schmidt and Uli Sattler
Intuitively, a base W -symbol is introduced to represent a subformula, and a
combinatory W -symbol can be seen as a unique representative of a subset of the
base W -symbols.
We now describe the three groups of rules which together make up our cal-
culus. We use N to refer to the current working clause set. We assume that x
is the current symbol we would like to eliminate, i.e., it is the maximal symbol
with respect to a given ordering for symbols outside Σ. The W -symbol Wi is
the ith W -symbol introduced during the inference process.
Preprocessing. The purpose of the preprocessing rules is to apply transforma-
tions to the members of the working clause set so that they can be handled by
the other rules. Generally, the idea is to surface symbols appearing in φ that are
not in Σ, i.e., to surface x in φ.
The normal form is based on pushing negation inwards, clausifying and ap-
plying structural transformation. The rules are applied in a lazy manner which
means their application can be deferred to whenever they are necessary. The
preprocessing rules are provided in Figure 1.
The first five rules are standard rules to transform modal formulae into nega-
tion normal form. The clausification rule distributes disjunction over conjunc-
tion. The world introduction rule performs structural transformation that flat-
tens the modal formulae. Consider a clause Wi ⇒ ¬¬ψ, the first negation normal
form rule replaces this clause with Wi ⇒ ψ, so the original clause is no longer
in the working set.
Resolution. The second type of rules are the resolution rules. The purpose of
these rules is to deduce a sufficient number of clauses/formulas to generate a
uniform interpolant. The rules are given in Figure 2.
The literal resolution rule is the heart of our calculus; it computes a formula
by resolving on a maximal symbol x if the premise is labelled with the same
W -symbol. The world resolution rule is used to propagate formulas labelled by
another W -symbol, which is essentially a resolution step between world symbols.
The 2# resolution rule is used to capture combinations of successor relations.
The second and third conditions are the blocking conditions; they aim to ensure
that the rule application is not redundant which is important for complexity,
and that the calculus does not infinitely introduce W -symbols which is essential
for termination.
Elimination. The last type of rules are the elimination rules. These rules are
responsible for eliminating symbols outside of Σ ∪ {W0 }. They are applied once
we have exhaustively applied the resolution rules to compute conclusions over Σ.
The rules are given in Figure 3.
The positive and negative purification rules replace a maximal symbol x,
occurring either positively or negatively, with >. The world elimination rule
collects modal formulas labelled with the same W -symbol, and replaces right
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 21
Negation Normal Form (1):
N, Wi ⇒ ¬¬φ1 ∨ φ2 provided that φ1 contains x.
N, Wi ⇒ φ1 ∨ φ2 φ2 may be empty.
Negation Normal Form (2):
N, Wi ⇒ ¬(φ1 ∧ φ2 ) ∨ φ3 provided that either φ1 or φ2
N, Wi ⇒ ¬φ1 ∨ ¬φ2 ∨ φ3 contain x. φ3 may be empty.
Negation Normal Form (3):
N, Wi ⇒ ¬(φ1 ∨ φ2 ) ∨ φ3 provided that either φ1 or φ2
N, Wi ⇒ ¬φ1 ∨ φ3 , Wi ⇒ ¬φ2 ∨ φ3 contain x. φ3 may be empty.
Negation Normal Form (4):
N, Wi ⇒ ¬3a φ1 ∨ φ2 provided that φ1 contains x.
N, Wi ⇒ 2a ¬φ1 ∨ φ2 φ2 may be empty.
Negation Normal Form (5):
N, Wi ⇒ ¬2a φ1 ∨ φ2 provided that φ1 contains x.
N, Wi ⇒ 3a ¬φ1 ∨ φ2 φ2 may be empty.
Implication Elimination:
N, Wi ⇒ (φ1 → φ2 ) ∨ φ3 provided that either φ1 or φ2
N, Wi ⇒ ¬φ1 ∨ φ2 ∨ φ3 contain x. φ3 may be empty.
Clausification:
N, Wi ⇒ (φ1 ∧ φ2 ) ∨ φ3 provided that either φ1 or φ2
N, Wi ⇒ φ1 ∨ φ3 , Wi ⇒ φ2 ∨ φ3 contain x. φ3 may be empty.
World Introduction (Int W):
provided that
N, Wi ⇒ #a φ1 ∨ φ2
N, Wi ⇒ #a Wj ∨ φ2 , Wj ⇒ φ1 (i) # ∈ {2, 3},
(ii) φ1 must contain x,
(iii) if φ2 contains x then x
must occur under a modal
operator, and
(iv) Wj is a fresh W -symbol,
and Corr(Wj ) = {Wj }.
φ2 may be empty.
Fig. 1: The preprocessing rules for U IKn calculus for the modal logic Kn . The
rules are replacement rules: each rule replaces the premise with an equisatisfiable
formula. In each rule, x is assumed to be the maximal symbol specified by the
given ordering on the symbols outside Σ occurring in the premises.
22 Ruba Alassaf, Renate A. Schmidt and Uli Sattler
Literal Resolution (Res):
Wi ⇒ ψ1 ∨ x Wi ⇒ ψ2 ∨ ¬x
ψ1 and/or ψ2 may be empty.
W i ⇒ ψ 1 ∨ ψ2
World Resolution (Res W):
Wi ⇒ ψ Wj ⇒ Wi provided that ψ contains x.
Wj ⇒ ψ ψ may be a W -symbol.
2# Resolution (Res 2#):
Wi ⇒ ψ1 ∨ 2a Wn Wi ⇒ ψ2 ∨ #a Wm
Wi ⇒ ψ1 ∨ ψ2 ∨ #a Wj , Wj ⇒ Wn , Wj ⇒ Wm
provided that:
(i) # ∈ {2, 3},
(ii) Corr(Wn ) ∩ Corr(Wm ) is empty,
(iii) if there is a Wk such that Corr(Wk ) = Corr(Wn )∪Corr(Wm ) then
Wj = Wk , otherwise Wj is a fresh W -symbol, and Corr(Wj ) =
Corr(Wn ) ∪ Corr(Wm ).
ψ1 and/or ψ2 may be empty.
Fig. 2: The resolution rules of the U IKn calculus for the modal logic Kn . The
rules given here are saturation rules: they add conclusions to the current working
clause set. We use x to refer to the maximal symbol in the working set specified
by a given ordering on the symbols outside Σ.
Positive Purification (+Pur):
provided that no more non-
N, Wi ⇒ ψ ∨ x
purification inference rules can
N, Wi ⇒ ψ ∨ >
be applied. ψ may be empty.
Negative Purification (-Pur):
provided that no more non-
N, Wi ⇒ ψ ∨ ¬x
purification inference rules can
N, Wi ⇒ ψ ∨ >
be applied. ψ may be empty.
World Elimination (Elm W):
N, Wi ⇒ ψ1 , . . . , Wi ⇒ ψn
Wi
N(ψ1 ∧···∧ψn )
provided that i 6= 0, ψ1 , . . . , ψn do not contain x or any W -symbol, and N only
contains Wi on the right hand side of ⇒ clauses. The expression Nψφ denotes
the set of clauses that is obtained by replacing each occurrence of φ in N by ψ.
Fig. 3: The purification and elimination rules of the U IKn calculus for modal
logic Kn . The rules are replacement rules: each rule replaces the premise with
an equisatisfiable formula. In each rule, x is assumed to be the maximal symbol
specified by the given ordering on the symbols outside Σ occurring in the
premises.
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 23
hand side occurrences of the W -symbol with the conjunction of these formulas,
effectively eliminating the W -symbol from the set of clauses.
4.3 Examples
In the following examples, we demonstrate how the U IKn system is used to
compute a uniform interpolant with respect to Σ = {p, q}. Starting from i = 0,
we use Ni to refer to the clause set that is obtained after applying the ith step
in the derivation.
Example 1. Consider a formula φ = (¬p ∨ 3x) ∧ (¬x ∨ 2q).
The input to the system is the set N0 = {W0 ⇒ (¬p ∨ 3x) ∧ (¬x ∨ 2q)}. The
only rule applicable to N0 is the clausification rule which gives
N1 = {W0 ⇒ ¬p ∨ 3x, W0 ⇒ ¬x ∨ 2q}.
Now we apply the world introduction rule to get
N2 = {W0 ⇒ ¬p ∨ 3W1 , W1 ⇒ x, W0 ⇒ ¬x ∨ 2q}.
The only applicable rules are the positive and negative purification rules. We
achieve
N3 = {W0 ⇒ ¬p ∨ 3W1 , W1 ⇒ >, W0 ⇒ > ∨ 2q}.
Eliminating W1 , we obtain
N4 = {W0 ⇒ ¬p ∨ 3>, W0 ⇒ > ∨ 2q}.
The Σ-uniform interpolant is φ0 = (¬p ∨ 3>) ∧ (> ∨ 2q).
Notice that this example illustrates the local flavour of the system. We see
that the occurrences of x at two different modal levels do not interact via any
resolution rule.
Example 2. Consider a formula φ = (¬p ∨ 3x) ∧ 2(¬x ∨ 2q). We start with the
set N0 = {W0 ⇒ (¬p ∨ 3x) ∧ 2(¬x ∨ 2q)}. Applying clausification to N0 we get
N1 = {W0 ⇒ ¬p ∨ 3x, W0 ⇒ 2(¬x ∨ 2q)}.
By applying the world introduction rule twice, we have
N3 = {W0 ⇒ ¬p ∨ 3W1 , W1 ⇒ x, W0 ⇒ 2W2 , W2 ⇒ ¬x ∨ 2q}.
The only applicable rule is the 23 rule, and it yields
N4 = N3 ∪ {W0 ⇒ ¬p ∨ 3W3 , W3 ⇒ W1 , W3 ⇒ W2 }.
By applying the world resolution rule twice, we obtain
N6 = N4 ∪ {W3 ⇒ x, W3 ⇒ ¬x ∨ 2q}.
24 Ruba Alassaf, Renate A. Schmidt and Uli Sattler
Now, we can apply the literal resolution rule which yields
N7 = N6 ∪ {W3 ⇒ 2q}.
We apply the positive and negative purification rules (4 applications) and achieve
N11 = { W0 ⇒¬p ∨ 3W1 , W1 ⇒>, W0 ⇒2W2 ,
W2 ⇒> ∨ 2q, W0 ⇒¬p ∨ 3W3 , W3 ⇒W1 ,
W3 ⇒W2 , W3 ⇒>, W3 ⇒> ∨ 2q,
W3 ⇒2q }.
Now, x does not appear anywhere. We eliminate the world variables W1 , W2 ,
W3 via the world elimination rule.
To eliminate W1 , we look for clauses labelled with W1 , in this case we only
have W1 ⇒ >. We remove W1 ⇒ > and replace each occurrence of W1 on the
right hand side of ⇒ with > as follows:
N12 = { W0 ⇒¬p ∨ 3>, W0 ⇒2W2 , W2 ⇒> ∨ 2q,
W0 ⇒¬p ∨ 3W3 , W3 ⇒>, W3 ⇒W2 ,
W3 ⇒> ∨ 2q, W3 ⇒2q }.
Similarly for W2 , we remove W2 ⇒ > ∨2q, and replace the other occurrences
of W2 with > ∨ 2q.
N13 = { W0 ⇒¬p ∨ 3>, W0 ⇒2(> ∨ 2q), W0 ⇒¬p ∨ 3W3 ,
W3 ⇒>, W3 ⇒> ∨ 2q, W3 ⇒2q }.
Finally, we eliminate W3 ,
N14 = { W0 ⇒¬p ∨ 3>, W0 ⇒2(> ∨ 2q),
W0 ⇒¬p ∨ 3(> ∧ (> ∨ 2q) ∧ 2q) }.
The uniform interpolant is
φ0 = (¬p ∨ 3>) ∧ (2(> ∨ 2q)) ∧ (¬p ∨ 3(> ∧ (> ∨ 2q) ∧ 2q)),
which is equivalent to φ0 = (¬p ∨ 32q) by standard simplifications.
4.4 Correctness
The output φ0 is correct if it is a uniform interpolant of a formula φ and a
signature Σ, produced in a finite number of steps. There are three issues at hand:
termination, soundness and completeness. We state the theorems and lemmas
that are relevant to these topics. For the proofs, we refer the reader to the full
version of the paper1 .
First are lemmas which are relevant to termination. We prove termination
by showing that any derivation uses a finite number of symbols, and we argue
that because of this, the calculus will stop generating new clauses.
Lemma 1. For a given formula φ and a signature Σ, the U IKn calculus intro-
duces a finite number of W -symbols.
1
https://personalpages.manchester.ac.uk/staff/ruba.alassaf/publications.html
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 25
Lemma 2. For a given formula φ and a signature Σ, the U IKn calculus will
stop generating new clauses.
Lemma 3. For a given formula φ and a signature Σ, the U IKn system will not
reintroduce a W -symbol that was eliminated before.
From Lemma 1, 2 and 3, we conclude the following theorem.
Theorem 1 (Termination). Given a formula φ and a signature Σ, the uni-
form interpolation system U IKn computes a formula φ0 in a finite number of
steps.
The following lemma addresses the space complexity of our system.
Lemma 4. The space complexity of the U IKn calculus is double exponentially
bounded in the length of the input.
The idea of the proof is to show each clause is exponentially bounded in the
length of the input n, and that the number of clauses produced by the system
is double exponentially bounded by n.
The next lemmas argue that the signature of φ0 is Σ.
Lemma 5. The U IKn system will always be able to eliminate every W -symbol
that is not W0 , using the world elimination rule.
Lemma 6. The U IKn system will always be able to eliminate symbols in the
signature of φ that are not in Σ.
Next, we state the soundness theorem.
Theorem 2 (Soundness). Given a formula φ and a signature Σ, the uniform
interpolation system U IKn computes a formula φ0 such that for any formula ψ
over Σ, we have that
if |= φ0 → ψ then |= φ → ψ.
For our completeness proof, we are interested in understanding models that
are invariant up to the satisfaction of Σ-modal formulas. Σ-modal formulas are
modal formulas described using a signature of propositional symbols Σ. For this
purpose, we use the following notion.
Definition 3 (Σ−bisimulation). Let (M, w) and (M0 , w0 ) be two Kripke mod-
els where M = (W, R, V ) and M0 = (W 0 , R0 , V 0 ). A Σ−bisimulation between
M and M0 is a relation ρ ⊆ W × W 0 such that wρw0 , and whenever uρu0 , the
following holds:
atoms u and u0 satisfy the same propositional symbols from Σ;
forth For all a, if uRa t, then there is a t0 such that u0 Ra0 t0 and tρt0 ;
back For all a, if u0 Ra0 t0 , then there is a t such that uRa t and tρt0 .
26 Ruba Alassaf, Renate A. Schmidt and Uli Sattler
The following is our completeness theorem.
Theorem 3 (Completeness). Given a formula φ and a signature Σ, the uni-
form interpolation system U IKn computes a formula φ0 such that, for any for-
mula ψ over Σ, we have that
if |= φ → ψ then |= φ0 → ψ.
Using proof by contradiction, we assume that |= φ → ψ but 6|= φ0 → ψ.
The assumption implies that there exists a counter-model M0 and a world w0
such that, M0 , w0 |= φ0 and M0 , w0 6|= ψ. We use Σ-bisimulation to prove by
induction that this is not possible.
5 Conclusion
The paper presented a resolution-based method to compute uniform interpolants
for the multi-agent modal logic Kn . It has been shown that our method termi-
nates, and is sound and complete. The space complexity was proven to be at
most double exponential in the length of the input. This work is intended to be
the basis of our future work. We would like to study logics which are known to
have the uniform interpolation property, and show that the presented system can
be extended to solve the uniform interpolation problem for more modal logics.
An implementation is being developed to demonstrate practicality.
References
1. Ackermann, W.: Untersuchungen über das Eliminationsproblem der mathematis-
chen Logik. Mathematische Annalen 110, 390–413 (1935)
2. Bı́lková, M.: Uniform interpolation and propositional quantifiers in modal logics.
Studia Logica: An International Journal for Symbolic Logic 85(1), 1–31 (2007)
3. Doherty, P., Lukaszewicz, W., Szalas, A.: Computing circumscription revisited: A
reduction algorithm. Journal of Automated Reasoning 18(3), 297–336 (1997)
4. Fang, L., Liu, Y., Van Ditmarsch, H.: Forgetting in Multi-agent Modal Logics. In:
Proc. IJCAI 2016. pp. 1066–1073. IJCAI/AAAI Press (2016)
5. Fitting, M.: Modal proof theory. In: Handbook of Modal Logic, vol. 3, pp. 85–138.
Elsevier (2007)
6. Gabbay, D.M., Ohlbach, H.J.: Quantifier elimination in second-order predicate
logic. In: Proceedings of the Third International Conference on Principles of
Knowledge Representation and Reasoning. pp. 425–435. KR’92, Morgan Kaufmann
(1992)
7. Ghilardi, S.: An algebraic theory of normal forms. Annals of Pure and Applied
Logic 71(3), 189 – 245 (1995)
8. Ghilardi, S., Zawadowski, M.: Undefinability of propositional quantifiers in the
modal system S4. Studia Logica 55(2), 259–271 (1995)
9. Herzig, A., Mengin, J.: Uniform interpolation by resolution in modal logic. In: Eu-
ropean Workshop on Logics in Artificial Intelligence. pp. 219–231. Springer (2008)
Resolution-Based Uniform Interpolation for Multi-Agent Modal Logic Kn 27
10. Horrocks, I., Hustadt, U., Sattler, U., Schmidt, R.: Computational modal logic. In:
Handbook of Modal Logic, vol. 3, pp. 181–245. Elsevier (2007)
11. Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting for ALC On-
tologies with ABoxes. In: Proceedings of the Twenty-Ninth AAAI Conference on
Artificial Intelligence. vol. 29, p. 175–181 (2015)
12. Ludwig, M., Konev, B.: Practical uniform interpolation and forgetting for ALC
TBoxes with applications to logical difference. In: Principles of Knowledge Repre-
sentation and Reasoning: Proceedings of the Fourteenth International Conference,
KR 2014. pp. 318–327 (2014)
13. Schmidt, R.A.: The Ackermann approach for modal logic, correspondence theory
and second-order reduction. Journal of Applied Logic 10(1), 52–74 (2012)
14. Visser, A.: Bisimulations, model descriptions and propositional quantifiers. Logic
Group Preprint Series 161 (1996)
15. Wolter, F.: Fusions of modal logics revisited. In: Advances in Modal Logic. pp.
361–379. CSLI (1998)
16. Zhao, Y., Schmidt, R.A.: Concept forgetting in ALCOI-ontologies using an
Ackermann approach. In: Proc. ISWC 2015. Lecture Notes in Computer Science,
vol. 9366, pp. 587–602. Springer (2015)