Research on uniform interpolation in modal logic has been largely focused on the theoretical investigation of the problem. This paper presents a system to compute uniform interpolants for a locally satisfiable 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 consequence 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.
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 [
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 [
We assume the reader is familiar with the multi-modal logic Kn [
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 interpolant of φ with respect to a signature Σ of propositional symbols is a formula φ0 such that: 1. φ0 does not contain symbols outside of Σ, and 2. for any modal formula ψ over Σ, we have that for all models M, M |= φ → ψ iff for all models M, M |= φ0 → ψ. 3
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 [
The second is a resolution-based calculus introduced in Herzig and
Mengin [
There are three more resolution-based systems for computing uniform
interpolation: the Scan approach [
Finally, second-order quantifier elimination methods which can be used to
compute uniform interpolants often use Ackermann’s lemma [
Uniform Interpolation Method U IKn for Kn We start with a high-level description of our uniform interpolation system for multi-modal logic Kn.
UIKn
Bilkova [
logic logic Method Resolution Sequent
Input Kn (locally K (locally Language satisfiable satisfiable
formula) formula) Output Kn (locally K (locally Language satisfiable satisfiable
formula) formula) Complete Yes Yes
Herzig Scan [
Modal First-order Description Description First-order logic logic logic logic logic Resolution Resolution Resolution Resolution Ackermann Ksat(ilsoficaabllley firsFt-uolrlder (ATLboCx (TAbLoCx) firsFt-uolrlder formula) logic +Abox) logic Ksat(ilsoficaabllley firsFt-uolrlder A(TLCboOxμ (TAbLoCx) firsFt-uolrlder formula) logic +Abox) logic
Yes No Yes No No 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 signature Σ, 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.
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 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 introduction 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: Corr(Wi) = {Wi}, Corr(Wn) ∪ Corr(Wm), if Wi ∈ Sw if Wi ∈ Cw where Wn and Wm come from the premise of the Res 2# rule that has introduced Wi.
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 calculus. 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 transformations 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 applying 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 negation normal form. The clausification rule distributes disjunction over conjunction. The world introduction rule performs structural transformation that flattens 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 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 Negation Normal Form (1): Negation Normal Form (2):
N, Wi ⇒ ¬¬φ1 ∨ φ2
N, Wi ⇒ φ1 ∨ φ2 N, Wi ⇒ ¬(φ1 ∧ φ2) ∨ φ3
N, Wi ⇒ ¬φ1 ∨ ¬φ2 ∨ φ3 Negation Normal Form (3): provided that φ1 contains x. φ2 may be empty. provided that either φ1 or φ2 contain x. φ3 may be empty.
N, Wi ⇒ ¬(φ1 ∨ φ2) ∨ φ3 N, Wi ⇒ ¬φ1 ∨ φ3, Wi ⇒ ¬φ2 ∨ φ3 provided that either φ1 or φ2 contain x. φ3 may be empty.
Negation Normal Form (4): Negation Normal Form (5):
N, Wi ⇒ ¬3aφ1 ∨ φ2 N, Wi ⇒ 2a¬φ1 ∨ φ2 N, Wi ⇒ ¬2aφ1 ∨ φ2
N, Wi ⇒ 3a¬φ1 ∨ φ2 N, Wi ⇒ (φ1 → φ2) ∨ φ3
N, Wi ⇒ ¬φ1 ∨ φ2 ∨ φ3 Implication Elimination: Clausification:
N, Wi ⇒ (φ1 ∧ φ2) ∨ φ3
N, Wi ⇒ φ1 ∨ φ3, Wi ⇒ φ2 ∨ φ3 World Introduction (Int W):
N, Wi ⇒ #aφ1 ∨ φ2 N, Wi ⇒ #aWj ∨ φ2, Wj ⇒ φ1 provided that φ1 contains x. φ2 may be empty. provided that φ1 contains x. φ2 may be empty. provided that either φ1 or φ2 contain x. φ3 may be empty. provided that either φ1 or φ2 contain x. φ3 may be empty. provided that (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. Literal Resolution (Res):
Wi ⇒ ψ1 ∨ x Wi ⇒ ψ2 ∨ ¬x
Wi ⇒ ψ1 ∨ ψ2 World Resolution (Res W):
Wi ⇒ ψ Wj ⇒ Wi
Wj ⇒ ψ ψ1 and/or ψ2 may be empty. provided that ψ contains x. ψ may be a W -symbol. 2# Resolution (Res 2#):
N(Wψ1i∧···∧ψ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. 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 ∨ 2 } q .
Now we apply the world introduction rule to get
N2 = {W0 ⇒ ¬p ∨ 3W1, W1 ⇒ x, W0 ⇒ ¬x ∨ 2 } q .
The only applicable rules are the positive and negative purification rules. We achieve
N3 = {W0 ⇒ ¬p ∨ 3W1, W1 ⇒ >, W0 ⇒ > ∨ 2 } q .
Eliminating W1, we obtain
N4 = {W0 ⇒ ¬p ∨ 3>, W0 ⇒ > ∨ 2 } q .
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 ∨ 2 } q .
N4 = N3 ∪ {W0 ⇒ ¬p ∨ 3W3, W3 ⇒ W1, W3 ⇒ W2}.
By applying the world resolution rule twice, we obtain
N6 = N4 ∪ {W3 ⇒ x, W3 ⇒ ¬x ∨ 2 } q . Now, we can apply the literal resolution rule which yields
N7 = N6 ∪ {W3 ⇒ 2 } q .
We apply the positive and negative purification rules (4 applications) and achieve N11 = { W0 ⇒¬p ∨ 3W1,
W2 ⇒> ∨ 2q, W3 ⇒W2,
W1 ⇒>, W0 ⇒¬p ∨ 3W3, W3 ⇒>,
W0 ⇒2W2, W3 ⇒W1, 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>, W2 ⇒> ∨ 2q, W0 ⇒2W2, W3 ⇒>,
W3 ⇒W2, W0 ⇒¬p ∨ 3W3,
W3 ⇒> ∨ 2q, W3 ⇒2q }.
N13 = { W0 ⇒¬p ∨ 3>,
W3 ⇒>, Finally, we eliminate W3,
W0 ⇒2(> ∨ 2q), W3 ⇒> ∨ 2q,
W0 ⇒¬p ∨ 3W3,
W3 ⇒2q }.
W0 ⇒¬p ∨ 3(> ∧ (> ∨ 2q) ∧ 2q) }.
N14 = { W0 ⇒¬p ∨ 3>,
W0 ⇒2(> ∨ 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 introduces a finite number of W -symbols.
1 https://personalpages.manchester.ac.uk/staff/ruba.alassaf/publications.html 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 uniform 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 models where M = (W, R, V ) and M0 = (W0, 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 uRat, then there is a t0 such that u0Ra0t0 and tρt0; back For all a, if u0Ra0t0, then there is a t such that uRat and tρt0.
The following is our completeness theorem.
Theorem 3 (Completeness). 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 |= φ → ψ then |= φ0 → ψ.
Using proof by contradiction, we assume that |= φ → ψ but 6|= φ0 → ψ.
such that, M0, w0 |= φ0 and M0, w0 6|= ψ. We use Σ-bisimulation to prove by induction that this is not possible. 5
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 terminates, 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.