=Paper=
{{Paper
|id=Vol-2785/paper3
|storemode=property
|title=Theorem Proving for Non-normal Modal Logics
|pdfUrl=https://ceur-ws.org/Vol-2785/paper3.pdf
|volume=Vol-2785
|authors=Tiziano Dalmonte,Sara Negri,Nicola Olivetti,Gian Luca Pozzato
|dblpUrl=https://dblp.org/rec/conf/overlay/DalmonteNOP20
}}
==Theorem Proving for Non-normal Modal Logics==
https://ceur-ws.org/Vol-2785/paper3.pdf
Proceedings of the
2nd Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY),
September 25, 2020
Theorem Proving for Non-normal Modal Logics*
Tiziano Dalmonte1 , Sara Negri2 , Nicola Olivetti3 , and Gian Luca Pozzato4
1
Aix-Marseille University, Marseille, France
2
University of Helsinki, Helsinki, Finland
3
Aix-Marseille University, Marseille, France
4
Università di Torino, Torino, Italy
1
tiziano.dalmonte@lis-lab.fr
2
sara.negri@helsinki.fi
3
nicola.olivetti@lis-lab.fr
3
gianluca.pozzato@unito.it
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.
1 Introduction
Non-Normal Modal Logics (NNML for short) [1] are a generalization of ordinary modal logics that do not satisfy
some axioms or rules of minimal normal modal logic K. They have gained interest in several areas such as epistemic
and deontic reasoning, reasoning about games, and reasoning about “truth in most of the cases”.
As a first example, in epistemic reasoning, where 2A is read as “the agent knows/believes A”, it was early
observed [12] that NNML offers a partial solution to the problem of omniscience: a non-omniscient agent would not
necessarily be able to conclude that she knows (or believes) B from that fact that she knows both A and A → B,
that is 2B does not follows from 2A and 2(A → B). This corresponds to rejecting the K-axiom, or even more
strongly, the rule of monotonicity (RM) A → B implies 2A → 2B and possibly also the rule of necessitation (if
B is valid then also 2B is valid) as it corresponds to the assumption that the agent knows every logical validity. As
another example, in deontic logic, where 2A is interpreted as “it is obligatory that A”, NNML may offer a way-out
to some well-known paradoxes caused by standard (normal) deontic logic. The simplest example is Ross’ paradox
[11]: let M denotes “the letter is mailed” and B “the letter is burnt”, obviously M → (M ∨ B), but from 2M ,
i.e. the obligation of send the letter, it seems odd to conclude 2(M ∨ B), that is the obligation to send the letter
or to burn it. Again, in this case the “culprit” is the (RM) rule mentioned above. A similar analysis underlies the
gentle-murder paradox. Moreover normal deontic logic does not allow one to represent conflicting obligations: for
instance let A be “you go to the faculty meeting”, it may hold both 2A and 2¬A (the former because you are a
member of the academic staff, the latter because you have a more important thing to do), without wanting 2⊥, that
by (RM) would trivialize obligations. Here the critical point is axiom C which allows one to conclude 2(A ∧ ¬A)
* This work has been partially supported by the projects ANR project TICAMORE ANR-16-CE91-0002-01, the Academy of Finland project
1308664, INdAM project GNCS 2019 “METALLIC #2: METodi di prova per il ragionamento Automatico per Logiche non-cLassIChe #2”.
Copyright © 2020 for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
18 T. Dalmonte et al.
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
A→B B→A
RE ,
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.
EMCN (K)
M I 2(A ∧ B) → 2A EMC EMN
EM
C I 2A ∧ 2B → 2(A ∧ B) ECN
N I 2> EC
E
EN
Figure 1: Axioms characterizing extensions of NNML (left) and the classical cube of NNML (right).
We consider a variant of the standard neighbourhood semantics for NNML, called bi-neighbourhood semantics [4].
Definition 2. A bi-neighbourhood model is a tuple M = hW, Nb , Vi, where: (i) W is a non-empty set of worlds
(states); (ii) V : Atm 7→ P(W) is a valuation function, assigning to each propositional variable the set of worlds
where such a variable is true; (iii) Nb is a bi-neighbourhood function W −→ P(P(W) × P(W)), where P denotes
19
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 t1 t2 · · · 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).
1 As a difference with [4] here terms are multisets rather than sets. This is uninfluential for the properties of the calculi.
20 T. Dalmonte et al.
axiom axiom⊥ axiom>
x : p, Γ ⇒ ∆, x : p x : ⊥, Γ ⇒ ∆ Γ ⇒ ∆, x : >
Γ ⇒ ∆, x : A Γ, x : A ⇒ ∆
L¬ R¬
Γ, x : ¬A ⇒ ∆ Γ ⇒ ∆, x : ¬A
Γ, x : A, x : B ⇒ ∆ Γ ⇒ ∆, x : A Γ ⇒ ∆, x : B
L∧ R∧
Γ, x : A ∧ B ⇒ ∆ Γ ⇒ ∆, x : A ∧ B
Γ, x : A ⇒ ∆ Γ, x : B ⇒ ∆ Γ ⇒ ∆, x : A, x : B
L∨ R∨
Γ, x : A ∨ B ⇒ ∆ Γ ⇒ ∆, x : A ∨ B
Γ ⇒ ∆, x : A Γ, x : B ⇒ ∆ Γ, x : A ⇒ ∆, x : B
L→ R→
Γ, x : A → B ⇒ ∆ Γ ⇒ ∆, x : A → B
x ∈ t, x : A, t ∀ A, Γ ⇒ ∆ ∀
x ∈ t, Γ ⇒ ∆, x : A ∀
L R
x ∈ t, t ∀ A, Γ ⇒ ∆ Γ ⇒ ∆, t ∀ A
x ∈ t, x : A, Γ ⇒ ∆ ∃
x ∈ t, Γ ⇒ ∆, x : A, t ∃ A ∃
L R
t ∃ A, Γ ⇒ ∆ x ∈ t, Γ ⇒ ∆, t ∃ A
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
M τ ∈ N (x), Γ ⇒ ∆ Nτ
t ∈ N (x), y ∈ t, Γ ⇒ ∆ Nτ x ∈ τ, Γ ⇒ ∆
Γ⇒∆
t1 t2 · · · tn ∈ N (x), t1 ∈ N (x), t2 ∈ N (x), . . . , tn ∈ N (x), Γ ⇒ ∆
C
t1 ∈ N (x), ..., tn ∈ N (x), Γ ⇒ ∆
x ∈ t1 , . . . , x ∈ tn , Γ ⇒ ∆ x ∈ t1 , Γ ⇒ ∆ x ∈ t2 , Γ ⇒ ∆ . . . x ∈ tn , Γ ⇒ ∆
dec dec
x ∈ t1 t2 · · · tn , Γ ⇒ ∆ x ∈ t1 t2 · · · tn , Γ ⇒ ∆
Application conditions:
x is fresh in R ∀ and L ∃
, a is fresh in L2, and x occurs in the conclusion of N τ .
Figure 2: The rules of LSE∗ .
21
Figure 3: A derivation of B → (2(A → A)) computed by PRONOM in the logic EN.
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
proceeds in a similar way for the other rules. The ordering of the clauses is such that the application of the branching
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.
22 T. Dalmonte et al.
5 Conclusions
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 non-
normal 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.