Conference 2009

Optimizing Coalgebraic Modal Logics

Daniel Hausmann^{a,2}

a DFKI Bremen, SKS

Abstract abstract hier, abstract da Keywords: Coalgebraic modal logic, heterogenous modal logic, automated reasoning

1 Introduction

…

2 Optimisations

An optimisation technique for satisfiability proofs of coalgebraic modal formulas is a coalgebra homomorphism, mapping states of a witness coalgebra to states of an optimized witness coalgebra (given a formula ϕ, coalgebra (A, α) is a witness of ϕ, whenever there is a state a ∈ A s.t. ϕ ∈ a). In general, the idea is to map bigger coalgebras to smaller coalgebras, thusly reducing the amount of necessary proof work.

In general, we are interested in finding as small as possible proofs for a given formula. Simplification by tautologies allows us to cut of short successfull branches or to shorten long successfull branches in the proof tree (without the need to completely explore them). Semantic branching allows to ensure that two or more sub-proofs (which are induced by a conjunction or a modal operator) are strictly disjoint in order to avoid repeated treatment of a sepcific formula. The technique of controlled backtracking allows us to cut of all branches in the proof tree which contain formulas that have already been shown to lead to success. Heuristics try to choose the shortest path through the proof tree that leads to success. Finally, the use of

1 Work forms part of DFG-project Generic Algorithms and Complexity Bounds in Coalgebraic Modal Logic (SCHR 1118/5-1)

2 Email: Daniel.Hausmann@dfki.de

This paper is electronically published in Electronic Notes in Theoretical Computer Science

                      URL: www.elsevier.com/locate/entcs

Hausmann

caching techniques turns (parts of) the proof tree into a proof graph, thusly eliminating the need for duplicate proofs while paying the price of possibly exponential storage needs.

The most important expectation with regards to any optimisation is of course that it must respect the soundness and completeness of the algorithm. Furthermore any optimisation involves some computations and might hence sometimes decrease the efficiency of the underlaying algorithm. Thus another important property of optimisations is, that its gain should ‘usually‘ be larger than the invested effort.

We describe the optimisation techniques (all of which being adoptations or generalisations of the techniques from Horrocks,Patel-Schneider, except the restriction to maximal applications of modal rules - Horrocks,Patel-Schneider considered only logics for which this restriction is admissable) in more detail:

2.1 Normalisation

First of all, we fix the syntactic form in which we assume all formulas to be. This is achieved by the process of normalisation of formulas which is in fact not an optimisation by itself, but rather a necessary condition for the usage of optimisations such as simplification by tautologies.

Syntactic construct Normalisation
⊥  ¬⊤
¬¬ϕ  ϕ
ϕ ∧ ψ  ¬(¬ϕ ∨ ¬ψ)
ϕ → ψ  ¬ϕ ∨ ψ
ϕ ↔ ψ  (ϕ → ψ) ∧ (ψ → ϕ)
ϕ ∨ ψ  ∪{ϕ, ψ}
∪{ϕ, (∪Γ)}  ∪({ϕ} ∪ Γ)

Fig. 1. Normalisation rules

The input formula is assumed to already contain only the standard modalities for each feature. Thus we normalize to truth, negation and generalized disjunction (where the collection of all disjuncts is treated as a set in order to remove duplicates and ordering).

2.2 Simplification by Tautologies

Optimisation by simplifaction rules makes use of specific (propositional or modal) tautologies in order to deterministically rewrite any appearing formulas in a proof. The application of simplification does not invoke any branching and is thus a linear process.

However, only tautologies with very few (and hence quickly checked for) assumptions should be used for simplification. Checking the assumptions of tautologies may involve the checking of syntactical equivalence of formulas. This task may be optimized by computing unique hashes for formulas and by then only checking for equality of the hash-values.

It is possible to distinguish two kinds of rules for the optimisation by simplification: Generic propositional rules which are the same for any coalgebraic modal logic and more specific modal simplification rules which may differ between any two concrete modal logics:

2.2.1 Propositional Simplification The following is a non-exhaustive set of prositional simplification rules on sequents:

Operator Propositional Tautology
∨  ∪{⊤, ...} → ⊤
∪{⊥, ϕ_{1}, …, ϕ_{n}} → ∪{ϕ_{1}, …, ϕ_{n}}
∪{ϕ, ¬ϕ, …} → ⊤
∨∧  ∪{¬ϕ, (ϕ ∧ ψ)} → ψ

Fig. 2. Propositional tautologies used for simplification

The last propositional tautology represents boolean constraint propagation (BCP).

2.2.2 Modal Simplification A modal feature may or may not allow for reasonable simplification:

Modal Operator Modal Tautology
K  □⊤ → ⊤
□ϕ ∧ □ψ → □(ϕ ∧ ψ)
KD  □⊤ → ⊤
…  …
CKCEM  (⊤ ⇒ ⊤) → ⊤
(⊥ ⇒ ⊤) → ⊤
…  …

Fig. 3. Modal tautologies used for simplification

2.3 Maximal Application of Modal Rules

A single modal rule often describes in fact a set of modal rules, each of the rules treating a different combination of positive and/or negative literals of the respective feature. Given a sequent Γ to match, any such modal rule could be applied to Γ, as long as the conclusion of the rule is a subset of Γ. It may be observed however that it often suffices to consider maximal applications of the modal rules. An application (Γ_{1}, Γ′_{1}) of a modal rule to Γ_{1} ⊆ Γ is maximal if there is no formula ϕ in Γ \ Γ_{1} s.t. the conclusion of any the modal rule would still be of shape Γ_{1} ∪ {ϕ}.

Given a set of modal rules R_{M}, the restriction to maximal applications of rules from R_{M} is admissable whenever the provability of the premise of any non-maximal application of a rule from R_{M} implies that there is a maximal application of a rule R_{M} with a provable premise.

Such a restriction is admissable (and in fact highly recommended) for many modal logics (see Table 4)

A negative example is the feature of CK (or similarly, the feature of CKCEM):

Example 2.1 Let us consider the examplary sequent Γ = {¬(A_{1} ⇒ B_{0}), ¬(A_{2} ⇒ B_{0}), (A_{0} ⇒ B_{0})} and assume that A_{0} ↔ A_{1} but A_{1} ↮ A_{2}. The only maximal application of the modal rule CK would lead to three new sequents:

\frac{\frac{√}{A_{0} ↔ A_{1}}  \frac{⊥}{A_{1} ↔ A_{2}}  \frac{√}{¬B_{0}, B_{0}}}{¬(A_{1} ⇒ B_{0}), ¬(A_{2} ⇒ B_{0}), (A_{0} ⇒ B_{0})}

The second of these sequents is not provable by assumption, thus ϕ can not be shown to be provable.

However, using a non-maximal application of the modal rule CK to the subsequent Γ′ = {¬(A_{1} ⇒ B_{0}), (A_{0} ⇒ B_{0})} of Γ, the provability of ϕ may be shown:

\frac{\frac{√}{A_{0} ↔ A_{1}} \frac{√}{¬B_{0}, B_{0}}}{¬(A_{1} ⇒ B_{0}), ¬(A_{2} ⇒ B_{0}), (A_{0} ⇒ B_{0})}

Even though the restriction to maximal applications of the modal rule of CK is not admissable, it is possible to obtain a nearly equivalent optimisation of the proofs for CK by the use of intelligent modal heuristics (see 2.7).

2.4 Semantic Branching

The technique of semantic branching allows us to make sure that created subproofs are strictly disjoint. This prevents duplicate proofs a formulas which might otherwise appear in both sub-proofs. This technique may however enlarge the proof tree.

2.4.1 Propositional Semantic Branching In the propositional case, there is just one branching rule, the conjunction rule.

Example 2.2 Consider the sequent Γ = {A ∧ B, C ∧ A} and let A be provable, but let A induce a lengthy proof tree. The use of syntactic branching leads to following redundant proof tree:

Hausmann

Modal Operator Restriction allowed?
◇_{K}  Yes
◇_{KD}  Yes
◇_{Mon}  Yes
◇_{HM}  Yes
◇_{P}  Yes
◇_{G}  Yes
⇒_{CK}  No
⇒_{CK+CEM}  No
⇒_{CK+CM}  Yes
⇒_{SystemS}  Yes

Fig. 4. Admissability of restriction to maximal application of modal rules

syntactic branching semantic branching
\frac{A  B}{A ∧ B}  \frac{A  ¬A, B}{A ∧ B}

Fig. 5. Syntactic vs. Semantic branching on conjunctions

\frac{\frac{\frac{\frac{√}{…}}{A} \frac{\frac{√}{…}}{A, C}}{A, A ∧ C}}{A ∧ B, A ∧ C}

Semantic branching on the other hand may lead to a much smaller proof tree:

\frac{\frac{\frac{\frac{√}{…}}{A, C} \frac{√}{¬A, A}}{A, C ∧ A} \frac{\frac{…}{B, C} \frac{\frac{√}{…}}{B, A}}{¬A, B, C ∧ A}}{A ∧ B, C ∧ A}

2.4.2 Modal Semantic Branching Modal rule needs to branch, i.e. have more than one sequent in its premise. How about CKCM? This branches 5 times and the respective sequents may overlap?

2.5 Boolean Constraint Propagation (BCP / Resolving)

This is just a propositional simplification. A modal simplification might be derived from it though. See 2.2!

2.6 Controlled Backtracking

The technique of controlled backtracking (also known as dependency directed backtracking) is in fact a special instance of caching. When this optimisation is employed, each formula ϕ in a sequent depends on a set #(ϕ) of formulas (namely on those formulas which introduced ϕ into the proof tree). Whenever a sequent turns out to be provable by an axiom, there are possibly several formulas involved in this process (e.g. the sequent Γ = {C, ¬C, D} for a propositional atom C is provable by the axiom Atom, the formulas C and ¬C are involved in this application of the axiom). These formulas are called promotors.

Fact 2.3 Given a set p of promotors, any sequent Γ s.t. p ⊆ Γ, is provable.

Due to Fact 2.3, it is not necessary to treat any open sequents between the current finished node in the proof graph and the node which introduced the last of the promotors.

To achieve this, a set of current dependency states is used, and whenever a sequent is provable by an axiom, the current set of dependency states is set to the union of the dependency sets of all the promotors. All those open sequents which are confronted during the following backtracking through the proof graph and which are created by a sequent which is not in the current set of dependency states, may be directly set to provable.

If a node in the proof graph which is contained in the current set of dependency states is reached, the current set of dependency states is set to ∅ and the proof may continue as usual.

The set of formulas on which a sequent Γ depends on is defined as follows (depending on the rule that introduces Γ):

• If Γ′ is obtained from Γ by means of normalisation or simplification, then #(Γ′) := #(Γ).

• If Γ′ is the only sequent in the rule application of a non-branching rule to Γ, then #(Γ′) := #(Γ)

• If Γ′_{1}, …, Γ′_{n} are n sequents from the premise of the rule application of a branching rule to Γ, the dependancy set of any formula ϕ ∈ ⋃_{i∈{1,...,n}} Γ_{i} is defined as follows: if ∀i ∈ {1, …, n}.ϕ ∈ Γ_{i}, then #(ϕ) := #(Γ), else #(ϕ) := Γ.

Inituitively, a single application of for instance the modal rule of K does not choose any subformulas of its conclusionary sequent to generate new sequents (this is already a consequence of the fact that this rule does not branch). Hence any introduced formulas will depend on those formulas on which the conclusionary sequent already depended. On the other hand, the modal rule of CK selects some subformulas (the antecedents) from its conclusionary sequent to be in the first sequent of the premise and others (the consequents) to be in the second sequent of the premise, thus a choice is made and the introduced formulas will directly depend

Feature Modal Rule(s)  Dependencies
K  \frac{Γ_{1} = ¬A_{1}, …, ¬A_{n}, B}{Γ = ¬◇A_{1}, …, ¬◇A_{n}, ◇B}  #(Γ_{1}) := #(Γ)
…  …  …
CK  \frac{Γ_{1} = A_{0} ↔ … ↔ A_{n}  Γ_{2} = ¬B_{1}, … ¬B_{n}, B_{0}}{Γ = ¬(A_{1} ⇒ B_{1}), …, ¬(A_{n} ⇒ B_{n}), (A_{0} ⇒ B_{0})} #(Γ_{1}, Γ_{2}) := Γ

Fig. 6. Propagation of dependencies over some examplary modal features

on the conclusionary sequent.

The following Lemmas establish that dependency directed backtracking as defined above is a sound optimisation technique for any coalgebraic model logic:

Lemma 2.4 Assume an application of any (possibly branching) rule:

\frac{Γ_{1}  …  Γ_{n}}{Γ}

Given a formula ϕ with dependency set #(ϕ), s.t. #(ϕ) ⊈ Γ, if ϕ is contained in any sequent of the premise, it is contained in all sequents of the premise

Lemma 2.5 Let the following be a (not yet fully explored) proof tree for Γ (where Γ_{j}^{i} denotes the sequent number j on level i):

\frac{\frac{\frac{\frac{\frac{√}{Γ_{1}^{n}}}{…}}{Γ_{1}^{2}}  …  Γ_{i}^{2}}{Γ_{1}^{1}}  …  Γ_{j}^{1}}{Γ}

Further, let #(√) denote the union of the dependency sets of those formulas which lead to the sucessfull treatment of Γ_{1}^{n} (i.e. the promotors of Γ_{1}^{n}). If for all Γ_{1}^{i} with 1 < i ≤ n, #(√) ⊈ Γ_{1}^{i}, and if #(√) ⊆ Γ_{1}^{1} (i.e. Γ_{1}^{1} is the first sequent on which any of the promotors depends), then Γ_{1}^{1} is provable (since any Γ_{j}^{i} with i > 1 is provable).

Proof. We try to find any Γ_{j}^{i} which is not provable. Since Γ_{1}^{n} is provable, any open sequent that could be not provable must have been created by a branching rule from the sequent Γ_{1}^{i−1}. However, since #(√) ⊈ Γ_{1}^{i−1}, the promotors are by Lemma 2.4 contained in Γ_{2}^{i}, thus Γ_{2}^{i} is by Fact 2.3 provable. This shows that any Γ_{j}^{i} with i > 1 and Γ_{1}^{1} are provable. □

2.7 Heuristics

A heuristic guides the search in the proof tree and chooses

(i) a premise from the set of all open premises, (ii) a meta-disjunction within this premise and (iii) one sequent within the selected meta-disjunction.

To this end, the heuristic assigns a priority to each open premise, each open meta disjunction and each open sequent.

The sequent with the highest overall priority will be the next to be explored. A reasonable heuristic helps (if possible) in finding a shorter way to show prov-

ability of a formula.

2.7.1 Propositional expansion first It is a reasonable tactic of expansion to first completely treat all propositional formulas in a sequent before considering the modal literals. This may be achieved by assigning high priority to those sequents, meta-disjunctions and premises which are introduced by the conjunction rule. Such sequents, meta-disjunctions and premises which are generated by an application of a modal rule are given a low priority.

2.7.2 Classic Heuristics On top of this preference of propositional expansion, one might add any other heuristic, such as for instance one of the following two classic heuristics (or even a combination of both):

• most appearing first: Assign the highest priority to open sequents that appear in the highest number of formulas. The priority of meta-disjunctions is defined to be the priority of the contained sequent. The priority of a premise is the maximum of the priorities of the contained meta-disjunctions.

• oldest first: …

2.7.3 Modal Heuristics Here is a specific modal heuristic for CK (a similar heuristic if suitable for CK-CEM). Note, that this heuristic is only applicable if caching is enabled:

Within any premise of a modal rule, the short sequents of the form A ↔ B are given the highest priority (in combination with caching, this leads to a complete partition of modal antecedents into equivalence classes).

Once this is done, we give high priority (e.g. 1) to maximal (w.r.t the cached equivalence classes) premises and priority of 0 to non-maximal premises (i.e. we do not treat non-maximal premises at all). As long as not all significant equivalences have yet been shown or refuted, the priority of a premise stays at a normal value (e.g. 0.5).

In combination with caching (of logical equivalences), this heuristic implements the optimizations of CK and CKCEM proposed in Hausmann,Schröder 2009.

2.8 Caching

Well, we do global caching. This is a bit troublesome in combination with dependency directed backtracking though (use the union of dependency sets, whenever a formula is introduced twice!).

3 Global Caching Algorithm

This is an adoptation of the Algorithm from Pattinson et.al.

Key differences are

(i) We treat provability of formulas here instead of satisfiability. However, a formula is satisfiable whenever its negation is not provable.

(ii) The introduction of meta-disjunctions. (iii) X is a structured set now. This allows heuristics to first choose a premise to

treat, then choose a meta-disjunction from this premise and finally choose a sequent from the chosen meta-disjunction.

(iv) The propagation is optimized now. Instead of computing the fixpoints of all the undecided sequents every time, classes of coherent sequents are stored. The propagation checks only ’whether the new sequents decide any of the classes’.

3.1 The Graph

A sequent is a set of formulas. A meta-disjunction is a set of sequents. A premises is a set of meta-disjunctions.

A graph is a tuple (A, E, U, X, L_{1}, L_{2}) where A, E, U ⊆ Seq are sets of sequents, X ⊆ P rems is a set of premises.

Given a sequent Γ, we define the set of all possible rule applications to Γ, AR(Γ) = {(Γ, Σ) ∈ R}, the set of all obtainable premises AP (Γ) = {Σ | (Γ, Σ) ∈ AR(Γ)} and the set of all selections AS(Γ) = {(Σ, Γ′) | Σ ∈ AP (Γ) ∧ Γ′ ∈ Σ}.

We fix two effectively computable transitions between graphs:

• Expand: Given a sequent Γ that is contained in any meta-disjunction from any premise in X, this transition leads from a graph g to the graph g′ that is obtained from g by expanding Γ. To this end, X is extended by all the premises from AR(Γ) and Γ is removed from X (X′ = (X ∪ AP (Γ)) \ Γ). Furthermore, L_{1} is extended by all possible rule applications for Γ (L′_{1} = L_{1} ∪ AR(Γ)). Finally, L_{2} is extended by all possible selections for rule applications for Γ (L′_{2} = L_{2} ∪ AS(Γ)).

In conclusion, this procedure applies all applicable rules to Γ, marks all resulting premises as not yet expanded, marks Γ as expanded and stores the implied transitions in L_{1} and L_{2}.

For a fixed sequent Γ and a graph g, we denote the expansion of Γ in g by exp(g, Γ). If g′ = exp(g, Γ), we also write g →^{Γ}_{E} g′.

• Propagate: This procedure evaluates the given graph as far as yet possible: The sets X, L_{1} and L_{2} remain unchanged. The set of provable sequents however is extended by the least fixpoint of mL (A′ = A ∪ μ(mL)). The set of not provable sequents is extended by the greatest fixpoint of wL (E′ = E ∪ ν(wL)). Finally, those sequents that are known to be either provable or not provable are removed from the set of undecided sequents (U′ = U \ (A′ ∪ E′)). mL(X) = {Γ ∈ C | ∀.∃.∀.C ∪ A} wL(X) = {Γ ∈ C | ∃.∀.∃.C ∪ A}

Given a graph g, we denote the graph obtained by propagating in g by prp(g). If g′ = prp(g), we also write g →_{P} g′.

3.2 The Algorithm

In order to show the provability of a formula ϕ, we start off with the sequent Γ_{0} = {ϕ}.

Set g = (A = {∅}, E = ∅, U = {Γ_{0}}, X = AP (Γ_{0}), L_{1} = AR(Γ_{0}), L_{2} = AS(Γ_{0})). If X = ∅, return the current graph as result. Otherwise select any premise p from

X, select any meta-disjunction d from p and select any sequent Γ from d. Compute g′ = exp(g, Γ) s.t. g →^{Γ}_{E} g′. Optionally, compute g′′ = prp(g′) s.t. g′ →_{P} g′′. If Γ_{0} ∈ A′′ ∪ E′′, break and return the current graph.

Let A (E) be the set of provable (not provable) sequents from the resulting graph of the algorithm. If Γ_{0} ∈ A, return True, if Γ_{0} ∈ E, return False, otherwise return

Undecided.

3.3 Removing Caching

What if we propagate after every step and always ’empty’ the graph? Does it remove the caching while staying sound and complete and does it lead to PSPACE?

4 Conclusion

…