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)