PRONOM: Proof-Search and Countermodel Generation for Non-normal Modal Logics

Abstract

We present PRONOM, a theorem prover and countermodel generator for non-normal modal logics. PRONOM implements some labelled sequent calculi recently introduced for the basic system $\mathbf {E}$ and its extensions with axioms M, N, and C based on bi-neighbourhood semantics. PRONOM is inspired by the methodology of and is implemented in Prolog. When a modal formula is valid, then PRONOM computes a proof (a closed tree) in the labelled calculi having that formula as a root in the labelled calculi, otherwise PRONOM is able to extract a model falsifying it from an open, saturated branch. The paper shows some experimental results, witnessing that the performances of PRONOM are promising.

Supported by the ANR project TICAMORE ANR-16-CE91-0002-01, the Academy of Finland project 1308664 and INdAM project GNCS 2019 “METALLIC #2”.

1 Introduction

Non-Normal Modal Logics (NNML for short) have been studied since the seminal works by C.I. Lewis, Scott, Lemmon, and Chellas (for an introduction see [3]) in the 1960s. They are a generalization of ordinary modal logics that do not satisfy some axioms or rules of minimal normal modal logic $\mathbf {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”.

In epistemic reasoning, where $\Box A$ is read as “the agent knows/believes A”, it was early observed [21] 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 \rightarrow B$, that is $\Box B$ does not follows from $\Box A$ and $\Box A \rightarrow \Box B$. This corresponds to rejecting the K-axiom, or even more strongly, the rule of monotonicity (RM) $A \rightarrow B$ implies $\Box A \rightarrow \Box B$ and possibly also the rule of necessitation (if B is valid then also $\Box B$ is valid) as it corresponds to the assumption that the agent knows every logical validity.

In deontic logic, where $\Box A$ 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 [20]: let M denotes “the letter is mailed” and B “the letter is burnt”, obviously $M \rightarrow (M \vee B)$, but from $\Box M$, i.e. the obligation of send the letter, it seems odd to conclude $\Box (M \vee 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 $\Box A$ and $\Box \lnot 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 $\Box \bot$, that by (RM) would trivialize obligations. Here the critical point is axiom C which allows one to conclude $\Box (A \wedge \lnot A)$ from $\Box A$ and $\Box \lnot A$. Moreover, also $\Box \top$ (whence the necessitation rule) has been rejected by some authors, on the base that a logical truth cannot be the object of an obligation.

A non-normal interpretation of modal operators has been considered in logics of Ability (see [18] and references therein) where the formula $\Diamond A$ is interpreted as “the agent has the ability of doing something which makes A true”; let R denote “Ann draws a red card” and B “Ann draws a black card”, clearly $\Diamond (R \vee B)$ holds as Ann can choose a card from a normal deck of cards that will be either red or black, but unless she has a “magical” ability, she cannot ensure that she will pick a red card or a black one, thus it is reasonable (or at least consistent) to assume both $\lnot \Diamond R$ and $\lnot \Diamond B$. But this shows that the logic of ability does not satisfy the C axiom (in the dual form): $\Diamond (A \vee B) \rightarrow \Diamond A \vee \Diamond B$. NNML have also some interest in the area of game logic, more precisely it turns out that Monotonic logic extended with axiom $\Diamond \top$ is a particular case of coalition logics, see [19].

Finally, $\Box A$ can be interpred as “A is true in almost all cases” [2], with this interpretation axiom C clearly fails, as the fact that A and B are independently true in “almost all cases” does not entail that $A \wedge B$ will also be such; a similar situation arises with a probabilistic reading of $\Box A$ as “A is true with high probability” [18].

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 $\Box A$ 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.

In this paper we describe PRONOM (theorem PROver for NOnnormal Modal logics) a Prolog theorem prover for the classical cube of non-normal modal logic¹. Not many theorem provers for NNML have been developed so far. Here is a brief account: in [8] optimal decision procedures are presented for the whole cube of NNML; these procedures reduce a validity/satisfiability checking in NNML to a set of SAT problems and then call an efficient SAT solver. For this reason they probably outperform any (implementation of) specific calculi for these logics, but they do not provide explicitly “proofs”, nor countermodels. A theorem prover for logic $\mathbf {EM}$ based on a tableaux calculus (very similar to the one in [10]) is presented in [9]: the system handles more complex Coalition Logic and Alternating Time Temporal logic, and it is implemented in ELAN, an environment for rewriting systems. Finally [11] presents a Prolog implementation of a non-normal modal logic containing both the $[\forall \forall ]$ and the $[\exists \forall ]$ modality; the fragment with just $[\exists \forall ]$ coincides with the logic $\mathbf {EM}$, which is covered also by our theorem prover.

The prover PRONOM implements the labelled sequent calculi presented in [4]. These calculi are based on bi-neighbourhood semantics, a variant of the neighbourhood semantics recalled above: 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 bi-neighbourhood semantics is particularly significant for logics without monotonicity and maybe of interest in itself. However the main reason to consider it, rather than the standard one, is that it is easier to generate countermodels in the bi-neighbourhood semantics than standard neighbourhood models. On the other hand, it is shown in [4] that the two semantics are equivalent, and more precisely standard neighbourhood models and bi-neighbourhood models can be constructively transformed into each other. The calculi are modular and make use of labels to represent both worlds and neighbourhoods in the syntax. They have invertible rules and provide a decision procedure for the respective logic. Because of the invertibility of the rules, a finite countermodel in the bi-neighbourhood semantics (whence in the standard one) can be directly extracted from a failed derivation.

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) of the formula.

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. 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, Neighbourhood Semantics and Labelled Calculi

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

Let $\mathsf {Atm}$ be a countable set of propositional variables. The language $\mathcal L$ contains formulas given by the following grammar: $A\,{:}{:}\!= p \mid \bot \mid \top \mid A \vee A \mid A \wedge A \mid A \rightarrow A \mid \Box A$, where $p\in \mathsf {Atm}$.

The minimal logic $\mathbf {E}$ in the language $\mathcal L$ is defined by adding to classical propositional logic the rule of inference

and can be extended further by choosing any combination of axioms M, C, and N below on the left, thus producing eight distinct logics (see the classical cube, below on the right).

We recall that axioms M and N are respectively equivalent to the rules RM ($A \rightarrow B$/$\Box A \rightarrow \Box B$) and RN (A/$\Box A$), and that axiom K ($\Box (A \rightarrow B) \rightarrow \Box A \rightarrow \Box B$) is derivable from M and C. As a consequence, we have that the top system $\mathbf {EMCN}$ is equivalent to the weakest normal modal logic $\mathbf {K}$.

We consider here a variant of the standard neighbourhood semantics for NNMLs, called bi-neighbourhood semantics [4].

Definition 1

A bi-neighbourhood model is a tuple

$$\mathcal M= \langle \mathcal W, \mathcal N_{b}, \mathcal V\rangle ,$$

where:

• $\mathcal W$ is a non-empty set of worlds (states)

• $\mathcal V$ is a valuation function

• $\mathcal N_{b}$ is a bi-neighbourhood function $\mathcal W\longrightarrow \mathcal P(\mathcal P(\mathcal W)\times \mathcal P(\mathcal W))$, where $\mathcal P$ denotes the power set.

We say that $\mathcal M$ is a M-model if $(\alpha , \beta )\in \mathcal N_{b}(w)$ implies $\beta =\emptyset$, it is a N-model if for all $w\in \mathcal W$ there is $\alpha \subseteq \mathcal W$ such that $(\alpha , \emptyset )\in \mathcal N_{b}(w)$, and it is a C-model if $(\alpha _1, \beta _1), (\alpha _2, \beta _2)\in \mathcal N_{b}(w)$ implies $(\alpha _1\cap \alpha _2, \beta _1\cup \beta _2)\in \mathcal N_{b}(w)$. The forcing relation for boxed formulas is as follows:

where [A] is, as usual, the truth set of A in $\mathcal W$ obtained by the valuation $\mathcal V$.

In [4] it is shown that the bi-neighbourhood semantics characterises the whole cube of NNMLs, in the sense that:

Theorem 1

A formula A is a theorem of $\mathbf {E}$ iff it is valid in all bi-neighbourhood models. The correspondence carries over to the extensions: A is a theorem of $\mathbf {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. A standard neighbourhood model has the form $\mathcal M= \langle \mathcal W, \mathcal N_{s}, \mathcal V\rangle$, where $\mathcal W$, $\mathcal V$ are as before, and $\mathcal N_{s}$ has type $\mathcal W\longrightarrow \mathcal P(\mathcal P(\mathcal W))$. The forcing relation for boxed formulas is: $w\Vdash \Box A$ iff $[A]\in \mathcal N_{s}(w)$. In addition we may consider the following conditions: a model $\mathcal M$ is supplemented if $\alpha \in \mathcal N_{s}(w)$ and $\alpha \subseteq \beta$ implies $\beta \in \mathcal N_{s}(w)$, it contains the unit if $\mathcal W\in \mathcal N_{s}(w)$ for all $w\in \mathcal W$, and it is closed under intersection if $\alpha , \beta \in \mathcal N_{s}(w)$ implies $\alpha \cap \beta \in \mathcal N_{s}(w)$.

It is easy to see that every standard model gives rise to a bi-neighbourhood model, by taking for each neighbourhood $\alpha \in \mathcal N_{s}(x)$, the pair $(\alpha , \mathcal W\setminus \alpha )$. Moreover if the model is supplemented, contains the unit, or is closed under intersection the corresponding bi-neighbourhood model is a 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 $\mathcal M= \langle \mathcal W, \mathcal N_{b}, \mathcal V\rangle$ we can define the standard neighbourhood model $\mathcal M' = \langle \mathcal W, \mathcal N_{s}, \mathcal V\rangle$ by taking for all $w\in \mathcal W$, $\mathcal N_{s}(w) = \{ \gamma \subseteq \mathcal P(W) \mid \,\,\text {there}\,\,\text {is}\,\,(\alpha , \beta )\in \mathcal N_{b}(w)\,\,\text {s.t.}\,\,\alpha \subseteq \gamma \,\,\text {and}\,\,\beta \subseteq \mathcal W\setminus \gamma \}$. 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 a M/N/C model. For logics without monotonicity the above transformation can be optimized in order to obtain a model whose size is polynomially bounded by the size of the original one [4].

We turn now to present the labelled calculi for NNMLs based on the bi-neighbourhood semantics. The language $\mathcal L_{\mathsf LS}$ of labelled calculi extends $\mathcal L$ with a set $WL=\{x, y, z, ...\}$ of world labels, and a set $NL=\{a, b, c, ...\}$ of neighbourhood labels. We define positive neighbourhood terms, written $[a_1, ..., a_n]$, as finite multisets² of neighbourhood labels, with the unary multiset [a] representing an atomic term. Moreover, if t is a positive term, then $\overline{t}$ is a negative term. Negative terms $\overline{t}$ cannot be proper subterms, in particular cannot be negated. The term $\tau$ and its negative counterpart $\overline{\tau }$ are neighbourhood constants.

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

The formulas of $\mathcal L_{\mathsf LS}$ are of the following kinds:

$$\phi \,{:}{:}\!= x: A \mid t\Vdash ^{\forall }A \mid t\Vdash ^{\exists }A \mid x\in t \mid t\in \mathcal N(x).$$

Sequents are pairs $\varGamma \Rightarrow \varDelta$ of multisets of formulas of $\mathcal L_{\mathsf LS}$. The fully modular calculi $\mathsf {LSE^*}$ are defined by the rules in Fig. 1.

Fig. 1.

The rules of $\mathsf {LSE^*}$.

The above version of the calculi are sound and complete for sequents that may appear in a backward proof search having at the root a single formula (these sequents belong to the class of regular sequents, see [4] for details). It is easy to see that in case of monotonic logics (i.e. logics containing M) the rule $R\Box$ can be simplified by eliminating the second premise. The reason is that an application of the rule $L\Vdash ^{\exists }$ to the term $\overline{t}$ will introduce an element $y\in \overline{t}$ in the antecedent, so that the sequent immediately succeeds by rule $M$. So we can replace the rule $R\Box$ with the following:

Moreover the rule $M$ can also be deleted as it is not applicable anymore.

3 Design of PRONOM

In this section we present a Prolog implementation of the labelled calculi recalled in Sect. 2. The program, called PRONOM, is inspired by the “lean” methodology of , even if it does not follow its style in a rigorous manner. The program comprises a set of clauses, each one of them implementing a sequent rule or an axiom of $\mathsf {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, following the line of the theorem provers for modal and conditional logics in [1, 7, 13,14,15,16,17] and for preferential reasoning [5] in [6]. In the case of $\mathbf {EM}$ we consider both the modular version like in Fig. 1, and the optimised version in which the rule $R\Box$ is replaced by $R\Box _{M}$.

PRONOM represents a sequent with Prolog lists Spheres, Gamma and Delta. Lists Gamma and Delta represent the left-hand side and the right-hand side of the sequent, respectively. Elements of Gamma and Delta are labelled formulas, implemented by Prolog lists with two, three or four elements, as follows:

• standard formulas are pairs [x,f], where x is a label and f is a formula;

• formulas of the form either $x \in t$ or $x \in \overline{t}$ are triples [x,0,t] ([x,1,t], respectively), where x is a label and t represents term t; the inner value, either 0 or 1, is used to distinguish between positive and negative terms, t and $\overline{t}$, respectively;

• formulas of the form $t\, \models ^{\exists }\, A$, or $t\, \models ^{\forall }\, A$, or $\overline{t}\, \models ^{\exists }\, A$, or $\overline{t} \,\models ^{\forall }\, A$ are represented by quadruples [exists,t,0,a], [forall,t,0,a], [exists,t,1,a], [forall,t,1,a], respectively.

The list Spheres contains pairs of the form [x,Items], where Items is the list of terms belonging to N(x). Symbols $\top$ and $\bot$ are represented by constants true and false, respectively, whereas connectives $\lnot$, $\wedge$, $\vee$, $\rightarrow$, and $\Box$ are represented by , , , , and . Propositional variables are represented by Prolog atoms. As an example, the Prolog lists

are used to represent the sequent $t \in N(x), y \in \overline{t}, y: A, t\, \models ^\forall \, A \wedge B \Rightarrow \overline{t}\, \models ^\exists \,A \wedge B, x: \Box A.$

Given a non-normal modal formula F represented by the Prolog term f, PRONOM executes the main predicate of the prover, called prove³, whose only two clauses implement the functioning of PRONOM: the first clause checks whether F is valid and, in case of a failure, the second one computes a model falsifying F. In detail, the predicate prove first checks whether the formula is valid by executing the predicate:

This predicate succeeds if and only if the sequent represented by the lists Spheres, Gamma and Delta is derivable. When it succeeds, the output term ProofTree matches with a representation of the derivation found by the prover. Further arguments RBox,RExist, and LAll are used in order to control the application of rules $R\Box$, $R\Vdash ^{\exists }$, and $L\Vdash ^{\forall }$, for obtaining a terminating proof search. More in detail, let us consider the rule $R\Box$, which is applied (backward) to a sequent of the form $t \in N(x), \varGamma \Rightarrow \varDelta , x: \Box A$: both the principal formulas $t \in N(x)$ and $x: \Box A$ are copied into the premises, then we need to prevent further applications of the same rule in a backward proof search. In order to control the application of this rule, the list RBox contains triples of the form [x,a,t] in order to keep trace of the fact that, in the current branch of the tree, the rule $R\Box$ has been already applied to $x: \Box A$ by using $t \in N(x)$. Therefore, the application of the rule is restricted by instantiating a Prolog variable T such that [X,A,T] does not belong to RBox. Similarly for RExist and LAll.

As an example, in order to prove that the sequent $x: \Box (A \wedge (B \vee C)) \Rightarrow x: \Box ((A \wedge B) \vee (A \wedge C))$ is valid in $\mathbf {E}$, one queries PRONOM with the goal:

Each clause of terminating_proof_search implements an axiom or rule of the sequent calculi $\mathsf {LSE}$ and extensions. To search for a derivation of a sequent $\varGamma \Rightarrow \varDelta$, PRONOM proceeds as follows. First of all, if $\varGamma \Rightarrow \varDelta$ is an instance of an axiom, the goal will succeed immediately by using the following clause:

The modular, unoptimised, version for logic $\mathbf {EM}$ has also the following clause:

If $\varGamma \Rightarrow \varDelta$ is not an instance of the axioms, then the first applicable rule will be chosen, e.g. if Spheres contains an element [X, List], such that List contains T, representing that $t \in N(x)$, and Delta contains a formula [X,box A], representing that $x: \Box A$ belongs to the right hand side of the sequent, then the clause implementing the $R\Box$ 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 $R\Box$ is as follows:

Line 5 implements the restriction on the application of the rule described above, and used in order to ensure a terminating proof search: given an instantiation of the Prolog variable T, the rule is applied only in case it has not been already applied by using the same T for the formula $x: \Box A$ in the current branch, namely [X,A,T] does not belong to RBox. Since the rule is invertible, Prolog cut ! is used in line 6 to eventually block backtracking.

When the predicate terminating_proof_search fails, then the initial formula is not valid, and PRONOM extracts a model falsifying such a formula from an open saturated branch. This is computed by executing the predicate:

This predicate has the same arguments of terminating_proof_search, with the exception of the fourth one: here the variable Model matches a description of an open, saturated branch obtained by applying the rules of the calculi to the initial formula. 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. As an example, the following clauses implement the saturation in presence of a boxed formula $x: \Box A$ in the right hand side of a sequent:

PRONOM will first try to build a countermodel by considering the left premise of the rule $R\Box$, corresponding to recursively invoking the predicate build_saturate_branch on the premise introducing $t \,\models ^\forall \, A$ in the right hand side of the sequent in line 6. In case of a failure, the saturation process is completed by considering the right premise of $R\Box$ introducing $\overline{t}\, \models ^\exists \, A$ by the recursive call of line 12.

Clauses implementing axioms for the predicate terminating_proof_search are replaced by the last clause, checking whether the current sequent represents an open and saturated branch:

Since this is the very last clause of the predicate build_saturate_branch, it is considered by PRONOM only if no other clause/rule is applicable, therefore the branch is saturated. The auxiliary predicate instanceOfAnAxiom checks whether the branch is open by proving that it is not an instance of the axioms. The third argument matches a term model representing the countermodel extracted from the lists Spheres, Gamma, and Delta.

The implementation of the calculi for extensions of $\mathbf {E}$ is very similar: given the modularity of the calculi $\mathsf {LSE^*}$, the systems implementing the extensions are easily obtained by adding clauses for both the predicates terminating_proof_search and build_saturate_branch corresponding to the rules specifically tailored for the extensions under consideration. The only exception is logic $\mathbf {EM}$, for which we give also an optimised version containing the rule $R\Box _{M}$ instead of $R\Box$. For the extensions of $\mathbf {EM}$ we only propose the version with $R\Box _{M}$ in place of $R\Box$.

PRONOM can be used by means of a simple web interface, implemented in php and allowing the user to check whether a non-normal modal formula is valid by using a computer or a mobile device. The web interface also allows the user to choose the modal system to adopt, namely $\mathbf {E}$ or one of the extensions mentioned in Sect. 2. When a formula is valid, PRONOM builds a pdf file showing a derivation in the sequent calculus $\mathsf {LSE}$ (or one of its extensions) as well as the source file. Otherwise, a countermodel falsifying the initial formula is displayed. Prolog source codes and experimental results are also available. Some pictures of PRONOM are shown in Figs. 2, 3 and 4.

Fig. 2.

Home page of PRONOM. When the user wants to check whether a formula F is valid, then (i) he selects the non-normal modal logic to use, (ii) he types F in the form and (iii) clicks the button in order to execute the calculi.

Fig. 3.

When a formula is valid, PRONOM computes a pdf file as well as a source file of a derivation.

Fig. 4.

When a formula is not valid, PRONOM computes and displays a counter model falsifying it.

4 Performance of PRONOM

The performance of PRONOM seems to be promising. We have tested it by running SWI-Prolog, version 7.6.4, on an Apple MacBook Pro, 2.7 GHz Intel Core i7, 8GB RAM machine. We have performed two kinds of experiments: 1. We have tested PRONOM over sets of valid formulas in the basic system $\mathbf {E}$ as well as in each considered extension; 2. We have tested PRONOM on randomly generated formulas, fixing different time limits, numbers of propositional variables, and levels of nesting of connectives.

Concerning 1, we have considered around hundred valid formulas obtained by generalizing schemas of valid formulas by varying some crucial parameters, like the modal degree of a formula (the level of nesting of the $\Box$ connective). For instance, we have considered the following schemas (valid in all systems):

$$\begin{aligned}&(\Box (\Box (A_1 \wedge (B_1 \vee C_1)) \wedge \dots \wedge \Box (A_n \wedge (B_n \vee C_n)))) \rightarrow \\&(\Box (\Box ((A_1 \wedge B_1) \vee (A_1 \wedge C_1)) \wedge \dots \wedge \Box ((A_n \wedge B_n) \vee (A_n \wedge C_n))) \end{aligned}$$

$$(\Box ^n C_1 \wedge \dots \wedge \Box ^n C_j \wedge \Box ^n A) \rightarrow (\Box ^n A \vee \Box ^n D_1 \vee \dots \vee \Box ^n D_k)$$

We have obtained encouraging results: Table 1 reports results for $\mathbf {E}$, from which it can be observed that PRONOM is able to answer in less than one second on more than the $75 \%$ of the tests, also on valid formulas with high modal degrees.

Table 1. Number of timeouts of PRONOM over 91 valid formulas in $\mathbf {E}$.

Concerning 2, we have tested PRONOM for $\mathbf {E}$ over 1000 random formulas, obtaining the experimental results of Table 2. It is worth observing that, even in case formulas are generated from 7 different atomic variables and with a high level of nesting (10), PRONOM is able to answer in more than $80 \%$ of the cases within a time limit of 10 ms.

The random generation often leads to not valid formulas; as a consequence, this kind of tests has been useful also in order to evaluate the performance of PRONOM in computing countermodels: indeed, we have considered the number of timeouts in the execution of the top-level predicate prove described in the previous section, including the extraction of a countermodel in case of a failure in the proof search. Again, the experimental results seems to be adequate, and the time required for the generation of a counter model of a not valid formula is negligible with respect to the time needed to perform the whole computation.

Table 2. Percentage of timeouts in 1000 random tests (system $\mathbf {E}$).

Fig. 5.

Percentages of timeouts of PRONOM over valid formulas in extensions of $\mathbf {E}$.

Fig. 6.

Percentage of timeouts in 1000 random tests for extensions of $\mathbf {E}$.

We have repeated the above experiments also for all the extensions of $\mathbf {E}$ considered by PRONOM, and we have obtained the results in Figs. 5 and 6.

It is worth noticing that the above experimental results refer to the Prolog component of PRONOM only, thus they do not take into account the effort of the graphical interface in computing the pdf file of the derivation. Since the web application often requires a long time to answer, we are currently working on improving the performances of PRONOM in such a way that the interface will first provide an answer about the validity of the formula, whereas the generation of the /pdf file will be performed only if this option is explicitly selected by the user by clicking a suitable button. Moreover, we are planning to perform more accurate tests following the approach of [8], where randomly generated formulas can be obtained by selecting different degrees of probability about their validity.

5 Conclusions

We have described a Prolog Theorem prover for non-normal modal logics. As far as we know ours is the first program that provides both proof-search and countermodel generation for the whole cube of NNML. It implements directly, concisely, and modularly the labelled sequent calculi presented in [4]. The system provides both proof-search and countermodel construction: given a formula to check, the system outputs either a derivation or a countermodel of the formula, the latter in the bi-neighbourhood semantics, a variant of the standard neighbourhood semantics. Although the implementation does not make use of any optimization or any sophisticated data structure, its performances are encouraging. In future research we intend to study some improvements like the use of free variables for term instantiation and other optimisations. We also intend to implement an automated and efficient transformation of the bi-neighbourhood countermodels into standard neighbourhood models, as shown in [4].