Theorem Proving for Non-normal Modal Logics*

Abstract

In this work we briefly summarize our recent contributions in the field of proof methods, theorem proving and countermodel generation for non-normal modal logics. We first recall some labelled sequent calculi for the basic system E and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. Then, we present PRONOM, a theorem prover and countermodel generator for non-normal modal logics implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof in the labelled calculi, otherwise it is able to extract a model falsifying it from an open, saturated branch.

Introduction

from 2A and 2¬A. Moreover, also 2> (whence the necessitation rule) has been rejected by some authors, on the base that a logical truth cannot be the object of an obligation.

Non-normal modal logics enjoy a simple semantic characterization in terms of Neighbourhood models: these are possible world models where each world is equipped with a set of neighbourhoods, each one being itself a set of worlds; the basic stipulation is that a modal formula 2A is true at a world w if the set of worlds which make A true belongs to the neighbourhoods of w. A family of logics is obtained by imposing further closure conditions on the set of neighbourhoods. Here we consider a variant of such a semantics, namely a bi-neighbourhood semantics: in a bi-neighbourhood model each world has associated a set of pairs of neighbourhoods, the idea being that the two components of a pair provide independently a positive and negative support for a modal formula. The two semantics are equivalent [ 4 ], however in the bi-neighbourhood semantics it is easier to generate countermodels.

As far as we know, very few proof methods have been provided for NNML, and existing automated reasoners are not able to provide a countermodel in presence of a failed proof. In this work we try to summarize some recent results in trying to fill this gap, namely we present some labelled sequent calculi introduced in [ 4 ] for the basic system E and standard extensions with axioms C, N and M, as well as PRONOM, a Prolog implementation of such calculi introduced in [ 3 ], which is able to either provide a closed tree when the submitted formula is valid or build a countermodel in both the bi-neighbourhood and the standard neighbourhood semantics otherwise. As far as we know, PRONOM is the first theorem prover that provides both proof search and countermodel generation for the whole cube of non-normal modal logics. Although there are no benchmarks, its performance seems promising: as an example, we have tested PRONOM over 8000 formulas randomly generated, obtaining that it answers in less than one second in the 86% of the tests. The program PRONOM, as well as all the Prolog source files, including those used for the performance evaluation, are available for free usage and download at http://193.51.60.97:8000/pronom/. 2

Non-normal Modal Logics

In this section, we present the classical cube of Non-Normal Modal Logics, both axiomatically and semantically. The latter is defined in terms of bi-neighbourhood models [ 4 ] and it is equivalent to the standard neighbourhood semantics.

Definition 1. Let Atm be a countable set of propositional variables and let p ∈ Atm. The language L contains formulas given by the following grammar:

A ::= p | ⊥ | > | A ∨ A | A ∧ A | A → A | 2A

The Non-normal modal logics considered in this work are shown in Figure 1. The minimal logic E in the language L is defined by adding to classical propositional logic the rule of inference

RE

A → B B → A ,

2A → 2B and can be extended further by choosing any combination of axioms M, C, and N (on the left in Figure 1), thus producing eight distinct logics: we obtain the classical cube, on the right in Figure 1.

M C N

I I I 2(A ∧ B) → 2A 2A ∧ 2B → 2(A ∧ B) 2>

EMC EC

EM E EMCN (K)

EMN ECN

EN the power set. We say also that: - M is an M-model if (α, β) ∈ Nb(w) implies β = ∅; - M is an N-model if for all w ∈ W there is α ⊆ W such that (α, ∅) ∈ Nb(w); - M is a C-model if (α1, β1), (α2, β2) ∈ Nb(w) implies (α1 ∩ α2, β1 ∪ β2) ∈ Nb(w). The forcing relation is defined as usual (we define [A] = {w ∈ W | w A}), whereas we have w 2A if and only if there is (α, β) ∈ Nb(w) s.t. α ⊆ [A] and β ⊆ [¬A].

In [ 4 ] it is shown that the bi-neighbourhood semantics characterises the whole cube of NNML, in the sense that: Theorem 1. A formula A is a theorem of E iff it is valid in all bi-neighbourhood models. The correspondence carries over to the extensions: A is a theorem of E+(M/C/N) iff it is valid respectively in all bi-neighbourhood M/N/C-models (including any combination of axioms/corresponding model conditions).

It is instructive to recall also the standard neighbourhood semantics and see how the two semantics are related [ 4 ]. A standard neighbourhood model has the form M = hW, Ns, Vi, where W, V are as before, and Ns has type W −→ P(P(W)). The forcing relation for boxed formulas is: w 2A iff [A] ∈ Ns(w). In addition we may consider the following conditions: a model M is supplemented if α ∈ Ns(w) and α ⊆ β implies β ∈ Ns(w), it contains the unit if W ∈ Ns(w) for all w ∈ W, and it is closed under intersection if α, β ∈ Ns(w) implies α ∩ β ∈ Ns(w). It is easy to see that every standard model gives rise to a bi-neighbourhood model, by taking for each neighbourhood α ∈ Ns(x), the pair (α, W \ α). Moreover if the model is supplemented, contains the unit, or is closed under intersection the corresponding bi-neighbourhood model is an M/N/C model respectively. On the other hand every bi-neighbourhood model can be transformed into a standard model [ 4 ]: given a bi-neighbourhood model M = hW, Nb, Vi we can define the standard neighbourhood model M0 = hW, Ns, Vi by taking for all w ∈ W, Ns(w) = {γ ⊆ W | there is (α, β) ∈ Nb(w) s.t. α ⊆ γ and γ ⊆ W \ β}. It can be proved that the two models are equivalent and that the transformation preserves additional properties (supplementation etc.) whenever the bi-neighbourhood model is an M/N/C model. 3

The Labelled Sequent Calculi for Non-normal Modal Logics

In this section we describe the labelled calculi for NNML based on the bi-neighbourhood semantics introduced in [ 4 ]. The language LLS of labelled calculi extends L with a set W L = {x, y, z, ...} of world labels, and a set N L = {t, s, ...} of neighbourhood labels. We define positive neighbourhood terms, denoted by t1t2 · · · tn, as finite multisets1 of neighbourhood labels, with the unary multiset [a] representing an atomic term. Moreover, if t is a positive term, then t is a negative term. Negative terms t cannot be proper subterms, in particular they cannot be negated. The term τ and its negative counterpart τ are neighbourhood constants.

Intuitively, positive (resp. negative) terms represent the intersection (resp. the union) of their constituents, whereas t and t are the two members of a pair of neighbourhoods in bi-neighbourhood models.

The formulas of LLS are of the following kinds:

φ ::= x : A | t ∀ A | t ∃ A | x ∈ t | t ∈ N (x).

Sequents are pairs Γ ⇒ Δ of multisets of formulas of LLS .

The fully modular calculi LSE∗ are defined by the rules in Figure 2.

In analogy with the calculi for normal modal logics based on the relational semantics [ 9, 13 ], the calculi have separate left and right rules for logical constants. As an example, a derivation for the formula B → (2(A → A)), valid in the logic EN and computed by PRONOM, is shown in Figure 3.

In [ 4 ] it is shown that the calculi LSE∗ satisfy relevant structural properties (invertibility of the rules, admissibility of cut) and they allow to describe a decision procedure for the respective logics. This is obtained by controlling the backward application of the rules copying their principal formula into the premise(s), e.g. the rule R2. In order to obtain a terminating proof search, it is just needed to avoid multiple applications of this kind of rules in the same branch, by using the same formulas: as an example, in a given branch, it is useless to apply - backward - R2 more than once on a formula x : 2A, by considering the same t ∈ N (x).

1As a difference with [ 4 ] here terms are multisets rather than sets. This is uninfluential for the properties of the calculi. x : p,Γ ⇒ Δ,x : p axiom x : ⊥,Γ ⇒ Δ axiom⊥ Γ ⇒ Δ,x : > axiom> ΓΓ,x⇒: ¬ΔA,x⇒: AΔ L¬ ΓΓ,,xx::AA,x∧:BB⇒⇒ΔΔ L∧ Γ,x : A ⇒ Δ Γ,x : B ⇒ Δ L∨

Γ,x : A∨B ⇒ Δ Γ ⇒ Δ,x : A Γ,x : B ⇒ Δ L →

Γ,x : A → B ⇒ Δ x ∈xt∈,xt:,tA,t∀ A∀,ΓA,⇒Γ Δ⇒ Δ L ∀ x ∈t t,∃xA:,AΓ,⇒Γ⇒ΔΔ L ∃

ΓΓ⇒,x Δ:A,x⇒: ¬ΔA R¬ Γ ⇒ Δ,x : A Γ ⇒ Δ,x : B R∧ Γ ⇒ Δ,x : A∧B ΓΓ⇒⇒ΔΔ,,xx::AA,x∨:BB R∨ ΓΓ,⇒x:ΔA,⇒x:ΔA,→x:BB R → x ∈Γt⇒,ΓΔ⇒,tΔ,∀xA: A R ∀ x ∈xt∈,Γt,⇒Γ Δ⇒,xΔ:,tA,t∃ A∃ A R ∃ t ∈ N(x),t ∀ A,Γ ⇒ Δ,t ∃ A L2

x : 2A,Γ ⇒ Δ t ∈ N(x),Γ ⇒ Δ,x : 2A,t ∀ A t ∈ N(x),t ∃ A,Γ ⇒ Δ,x : 2A R2

t ∈ N(x),Γ ⇒ Δ,x : 2A t ∈ N(x),y ∈ t,Γ ⇒ Δ M τ ∈ N(x),Γ ⇒ Δ Nτ x ∈ τ,Γ ⇒ Δ Nτ

Γ ⇒ Δ t1t2···tn ∈ N(x),t1 ∈ N(x),t2 ∈ N(x),...,tn ∈ N(x),Γ ⇒ Δ C

t1 ∈ N(x),...,tn ∈ N(x),Γ ⇒ Δ x ∈x ∈t1,t1.t.2.,·x··∈tnt,nΓ,Γ⇒⇒ΔΔ dec x ∈ t1,Γ ⇒ Δ x ∈ t2,Γ ⇒ Δ ... x ∈ tn,Γ ⇒ Δ dec x ∈ t1t2···tn,Γ ⇒ Δ Application conditions: x is fresh in R ∀ and L ∃, a is fresh in L2, and x occurs in the conclusion of Nτ.

4 PRONOM: a Theorem Prover for Non-normal Modal Logics

In this section we briefly sketch the main features of PRONOM, a Prolog implementation of the labelled calculi LSE∗. The program comprises a set of clauses, each one of them implementing a sequent rule or an axiom of LSE and its extensions. The proof search is provided for free by the mere depth-first search mechanism of Prolog, without any additional ad hoc mechanism.

The Prolog implementation closely corresponds to the calculi: each rule is encoded by a Prolog clause of a predicate called terminating_proof_search. This correspondence ensures in principle both the soundness and completeness of the theorem prover. Termination of proof search is obtained by controlling the non-redundant application of the relevant rules. PRONOM provides both proof search and countermodel generation: it searches for a derivation of an input formula, but in case of failure, it generates a countermodel (in the bi-neighbourhood semantics as well in the standard neighbourhood semantics of [ 4 ]) of the formula. More in detail, the predicate terminating_proof_search tries to generate a derivation of the given input formula. First of all, if Γ ⇒ Δ is an instance of an axiom, the goal will succeed immediately by using the following clause: terminating_proof_search(Neigh,Gamma,Delta,...):

member([X,A],Gamma),member([X,A],Delta),!.

If Γ ⇒ Δ is not an instance of the axioms, then the first applicable rule will be chosen, e.g. if Neigh contains an element [X, List], such that List contains T, representing that t ∈ N(x), and Delta contains a formula [X,box A], representing that x : 2A belongs to the right hand side of the sequent, then the clause implementing the R2 rule will be chosen, and PRONOM will be recursively invoked on the premises of such a rule. PRONOM proceedsinasimilarwayfortheotherrules. Theorderingoftheclausesissuchthattheapplicationofthebranching rules is postponed as much as possible. As an example, the clause implementing R2 is as follows: terminating_proof_search(Neigh,Gamma,Delta,...,RBox):member([X,box A],Delta),member([X,NOfX],Neigh), member(T,NOfX),\+member([X,A,T],RBox),!, terminating_proof_search(Neigh,Gamma,[[forall,T,0,A]|Delta],... ...,[[X,A,T]|RBox]), terminating_proof_search(Neigh,[[exists,T,1,A]|Gamma],Delta,... ...,[[X,A,T]|RBox]).

In case the predicate terminating_proof_search fails, on demand by the user, another predicate build_saturate_branch is invoked that computes an open saturated branch from which a countermodel is extracted. The predicate build_saturate_branch is in some sense “dual” of the proof search one: since the very objective of this predicate is to build an open, saturated branch in the sequent calculus, its clauses are essentially the same as the ones for the predicate terminating_proof_search, however rules introducing a branch in a backward proof search are implemented by pairs of (disjoint) clauses, each one representing an attempt to build an open saturated branch.

We have sketched labelled sequent calculi LSE∗ and the theorem prover and countemodel generator PRONOM for Non-normal modal logics, dealing with the whole cube of extensions of basic logic E with axioms C, M and N. Not many proof methods and theorem provers for NNML have been developed so far [ 2, 10, 5, 6, 7, 8 ]. In future research we intend to study some improvements of PRONOM like the use of free variables for term instantiation and the application of standard optimization techniques.

References

[1] B. F. Chellas . Modal Logic. Cambridge University Press, 1980 .

[2] T. Dalmonte , B. Lellmann , N. Olivetti , and E. Pimentel . Countermodel construction via optimal hypersequent calculi for non-normal modal logics . In S. N. Artëmov and A . Nerode, editors, Logical Foundations of Computer Science - International Symposium , LFCS 2020, Deerfield Beach, FL, USA, January 4- 7 , 2020 , Proceedings, volume 11972 of Lecture Notes in Computer Science, pages 27 - 46 . Springer, 2020 .

[3] T. Dalmonte , S. Negri , N. Olivetti , and G. L. Pozzato . PRONOM: proof-search and countermodel generation for non-normal modal logics . In M. Alviano, G. Greco, and F. Scarcello, editors, AI*IA 2019 - Advances in Artificial Intelligence - XVIIIth International Conference of the Italian Association for Artificial Intelligence , Rende, Italy, November 19-22 , 2019 , Proceedings, volume 11946 of Lecture Notes in Computer Science, pages 165 - 179 . Springer, 2019 .

[4] T. Dalmonte , N. Olivetti , and S. Negri . Non-normal modal logics: Bi-neighbourhood semantics and its labelled calculi . In G. Bezhanishvili, G. D'Agostino , G. Metcalfe , and T. Studer, editors, Advances in Modal Logic 12, proceedings of the 12th conference on Advances in Modal Logic , held in Bern, Switzerland, August 27-31 , 2018 , pages 159 - 178 . College Publications, 2018 .

[5] T. Dalmonte , N. Olivetti , and G. L. Pozzato . HYPNO: theorem proving with hypersequent calculi for nonnormal modal logics (system description) . In N. Peltier and V. Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conference, IJCAR 2020 , Paris, France, July 1-4 , 2020 , Proceedings, Part II , volume 12167 of Lecture Notes in Computer Science, pages 378 - 387 . Springer, 2020 .

[6] E. Giunchiglia , A. Tacchella , and F. Giunchiglia . Sat-based decision procedures for classical modal logics . Journal of Automated Reasoning , 28 ( 2 ): 143 - 171 , 2002 .

[7] H. Hansen . Tableau games for coalition logic and alternating-time temporal logic-theory and implementation . Master's thesis , University of Amsterdam, 2004 .

[8] B. Lellmann . Countermodels for non-normal modal logics via nested sequents . In N. Bezhanishvili and Y. Venema, editors, SYSMICS2019 - Booklet of Abstracts , pages 107 - 110 . Institute for Logic, Language and Computation University of Amsterdam, 2019 .

[9] S. Negri . Proof analysis in modal logic . J. Philosophical Logic , 34 ( 5-6 ): 507 - 544 , 2005 .

[10] S. Negri . Proof theory for non-normal modal logics: The neighbourhood formalism and basic results . IfCoLog J. Log. Appl , 4 ( 4 ): 1241 - 1286 , 2017 .

[11] A. Ross . Imperatives and logic . Theoria , 7 : 53 - 71 , 1941 .

[12] M. Y. Vardi . On epistemic logic and logical omniscience . In Theoretical aspects of reasoning about knowledge , pages 293 - 305 . Elsevier, 1986 .

[13] L. Viganó. Labelled Non-Classical Logics. Springer, 2000 .