Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Various powerful automated and interactive theorem proving systems (ATP and ITP, respectively) for first-order (FO) and higher-order (HO) logics have been developed over the past decades, including the first-order ATP E [1], the higher-order ATPs Satallax [2], LEO-II [3] and Leo-III [4], and the higher-order ITP Isabelle/HOL [5]. While many of these systems are meanwhile quite robust and mature, they often support reasoning in classical logics only. This is in contrast to the fact that non-classical logics have many topical applications in mathematics, computer science and beyond. In this work, we focus on the automation of quantified (multi-)modal logics [6] which can be fruitfully applied in the context of artificial intelligence, computational linguistics and rule-based reasoning. They also play an important role in various areas of philosophy, including ontology, (computer-)ethics, philosophy of mind and philosophy of science. Many challenging applications, however, as recently explored in metaphysics [7,8,9], require quantified and in particular higher-order quantified modal logics (HOMLs). But even for first-order non-classical logics only a small number of implemented systems is available to date, and the situation is even worse for higher-order quantified logics. In particular, the development of ATPs for HOMLs is still in its infancy, hence impeding more complex computer-assisted studies of relevant topics.

To overcome this situation, in this work we present the Modal Embedding Tool (MET for short) that bridges the above gap by enabling the employment of classical higher-order reasoning systems, including powerful HO ATPs, for reasoning in a broad variety of quantified modal logics. Recall that for quantified modal logics there exist multiple different notions of semantics, most of which usually used in different application domains. The exact semantics of a given quantified modal logic can be regarded a product of multiple individual semantical parameters, including:

  1. (i)

    Modal axiomatization: What properties hold for each modality? The properties range from axiom scheme K alone to the strong assumptions of logic S5, and any intermediate system (cf. the modal logic cube [6]).

  2. (ii)

    Quantification semantics: What are the domains of quantified variables? Usual choices include so-called cumulative, decreasing, constant and varying domain semantics.

  3. (iii)

    Rigidity: Is the meaning of a symbol the same in every possible world? Possible choices include rigid and world-dependent constant symbols.

Also, there exist different choices for logical consequence relations, including at least so-called local and global consequence [6]. When taking all possible parameter combinations into account this amounts to more than 120 different HOMLs.

Fig. 1.
figure 1

Working principle of the MET: A modal logic problem statement is given to the system which it then transforms and augments with suitable technical definitions. The resulting problem is formulated in classical logic and only valid if the original problem was valid.

Full size image

MET implements a shallow semantical embedding approach [10] in which formulas of modal logic are identified with specific terms of classical higher-order logic such that a notion of modal validity can be defined within HOL that coincides with the desired modal logic semantics. More concretely, a modal logic formulated in a suitable machine-readable syntax (cf. Figs. 2 and 3) is translated by MET to a problem statement in the de-facto standard TPTP THF syntax [11, 12] for HO ATP systems. The transformation process is thereby validity preserving and thus allows the use of common reasoning systems that do not support modal logic reasoning on their own. The process is visualized in Fig. 1. Although the here discussed approach involves an indirection over classical HOL, recent evaluations confirm that the reasoning effectivity of HO ATPs used in conjunction with MET are on a par with established modal logic reasoners [4]. Additionally, reasoning using MET is much more flexible than the employment of these special purpose systems as it allows a completely free choice of all relevant semantical parameters (supporting every existent normal modal logic) whereas native modal logic reasoners are limited to a small subset of modal logic systems and usually have fixed choices for quantification semantics, symbol rigidity and consequence. In fact, even more general modal logics are supported via a fine-grained control over the properties of individual quantification domains, modal operators, etc [13].

Whereas earlier work focused on the theoretical foundations [10], and the development of the automatic embedding procedure itself [13], in this paper, we present the prover-independent tool MET and its practical employment in relevant application scenarios.

Higher-Order Modal Logics. HOMLs as addressed here are extensions of HOL [14]. HOL provides \(\lambda \)-abstraction as an elegant means to denote unnamed functions, predicates and sets (by their characteristic functions). HOML, in turn, augments HOL with a set of modal operators \(\square ^i\), \(i \in I\), for some index set I, and is equipped with a suitable combination of HOL semantics and a Kripke-style modal semantics [13]. In our approach an adequate notion of Henkin semantics for both HOML and HOL is assumed [10, 13].

2 A Syntax for HOML and Its Semantics

A standard ASCII-based machine-readable representation of HOL problems for ATP systems is given by the TPTP THF dialect [12]. This syntax is supported by most of the current HOL reasoners, including all HO systems mentioned in the beginning of Sect. 1. Since the syntax of HOML is a conservative extension of that of classical HOL, the THF representation language can as well easily be augmented by introducing the modal operators and as new primitive connectives, representing the modal connectives \(\square \) and \(\Diamond \), respectively (in a mono-modal settings). For multi-modal logics, there exist analogous operators that are additionally given an index as first argument and the formula as second argument. The remaining syntax coincides with standard THF and is described in the literature [12].

Fig. 2.
figure 2

Layout of a general modal logic problem. The first statement (ll. 2–4) specifies a concrete modal logic, the remaining statements (ll. 6–8) formulate the problem itself. The \(\langle \mathsf {name}_i \rangle \) serve as syntactic identifier for that statement, a \(\langle \mathsf {role}_i \rangle \) (usually set to or ) tells the reasoning system how to interpret the \(\langle \mathsf {formula}_i \rangle \) formulated in the presented augmented THF syntax. Lines starting with are comments.

Full size image

As sketched in Sect. 1, there is no single semantics of quantified modal logics. As a consequence, there is additional need for explicitly stating the semantical setting in which a problem is to be assessed by a reasoning system. This is realized in the here proposed syntax by including a meta-logical specification into the problem header. Such a specification statement is displayed in Fig. 2: In this logic specification, the identifiers , and specify the exact semantical settings for the rigidity of constant symbols, the quantification semantics and the consequence relation, respectively. Finally, specifies the properties of the modal connectives by means of fixed modal logic system names or, alternatively, a list of individual modal axiom schemes. The valid parameter values are given in Table 1.

The remaining placeholders of Fig. 2, \(\langle \mathsf {name} \rangle \), \(\langle \mathsf {role} \rangle \) and \(\langle \mathsf {formula} \rangle \), are standard and given by the TPTP language definition [11] to which we refer to for brevity. The semantics specification format presented in this paper is work-in-progress and stems from an ongoing TPTP language extension proposal.Footnote 1

Table 1. Semantic specification parameters. The parameter placeholders, written in angles \(\langle \cdot \rangle \), refer to the values for the logic specification of Fig. 2. The names of the modal logic system parameters (such as or ) refer to the respective systems from the modal logic cube [6]. The individual modal axiom schemes names (such as or ) are named similarly.
Full size table

3 Application Examples

In this section, the practical employment of MET for reasoning with relevant non-trivial problem statements is discussed. The first application example, a formulation of the wise men puzzle, incorporates the use of multiple inter-related modality operators and quantification beyond first-order. The second example focuses on the use of logic specification statements within the problem and illustrates the flexibility of the here presented reasoning approach.

Fig. 3.
figure 3

The wise men puzzle formulated in modal THF syntax. The term $box_int @ i represents a box operator \(\square ^i\) for which the set of integers serves as index set I. In this example, the common knowledge agent (the fool) is given by index 0, the remaining three agents by indexes 1, 2 and 3.

Full size image

3.1 Case Study: The Wise Men Puzzle

A classical example dealing with knowledge between agents and implicit knowledge transfer is the wise men puzzle (also known in a variation as muddy forehead puzzle). Epistemic logic, the logic about knowledge, can be interpreted as a form of multi-modal logic, were the modality operators represent knowing and are indexed with an agent’s identifier from an index set I (referring to the particular agent whose knowledge it addresses). As an example, the sentence “agent a knows \(\phi \)”, for an agent \(a \in I\), can be stated as \(\square ^a \phi \). While dealing with common knowledge scenarios, often an additional artificial agent (sometimes referred to as fool) is defined for allowing statements such as “everybody knows \(\phi \)”, represented by \(\square ^{\text {fool}} \phi \).

A formulation of the wise men puzzle is given in Fig. 3. In the logic specification, the modalities (including the common knowledge modality) are given an S5 axiomatization to capture the usual assumptions about knowledge. Additionally, a varying domain semantics is used for this experiment. The modal operators \(\square ^a\) for some agent \(a \ne \mathrm {fool} \in I\) are related to common knowledge \(\square ^{\mathrm {fool}}\) using so-called bridge-rules stating that everything that is common knowledge is also known by the individual agents (cf. ll. 16–30). The common knowledge fact that the first two agents do not know their hat color is given by two axioms (ll. 33–34) and finally the conjecture that the third agent now knows its hat color is given by the conjecture (l. 37). The wise men problem in the presented formulation can be solved using MET in conjunction with Leo-III as reasoner back end in under 5s, cf. Appendix A for a detailed display of the tools usage.

3.2 Case Study: Experiments with Semantical Variations

In this case study, we focus on the flexibility the logic specification within a problem provides for experiments in different semantical settings. Figure 4 displays an example modal logic formula that is an instance of a corollary of Becker’s postulate [15]. It essentially expresses that everything that is possibly necessary it, in fact, necessary. Since this formula is obviously debatable, one might want to explicitly include or exclude this fact from a logical system. It is known from the literature, that Becker’s postulate is indeed valid in S5 modal logics but not in any weaker logic systems. Even without this knowledge, the MET allows to experimentally reproduce these results with only simple modification of the logic specification statements. To that end, each semantical setting can be formulated as logic specification and then transformed by MET to HOL problems. These HOL problems are then in turn given to HO reasoning systems for verifying or refuting the conjecture.

Fig. 4.
figure 4

A corollary of Becker’s postulate formulated in modal THF, representing the formula \(\forall P_{\iota \rightarrow o}\forall F_{\iota \rightarrow \iota }\forall X_\iota \exists G_{\iota \rightarrow \iota } (\Diamond \square P(F(X)) \Rightarrow \square P(G(X)))\).

Full size image

In the example of Becker’s postulate, the higher-order ATP system Leo-III and the counter-model finder Nitpick [16] verify the above claim. The systems produce proofs resp. explicit, finite, counter-models of the validity the conjecture in each modal logic system. The results of these experiments are summarized in Table 2. It can be seen that, for every modal logic system, the combination of both reasoners successfully assess the conjecture and yield the expected results. Each invocation of the reasoning systems (including the pre-processing by MET) takes less than 1 s. Note that both systems are in a sense complementary, i.e. theorem proving systems are usually stronger for proving the validity of a conjecture while counter-model finders focus on counter-satisfiability. Using both systems, positive and negative results can be established as desired.

The example of Becker’s postulate is chosen for demonstrative purposes. Similarly interesting formulas for certain modal logics such as Barcan’s formula (or its converse) can be analyzed analogously using MET [13]. In a more general setting, the semantical flexibility of the here presented approach allows for an empirical assessment of a formal system’s adequateness for a specific application; and to explore further, possibly unintended, consequences of a given formulation.

Table 2. Evaluation results of the validity of Becker’s postulate from Fig. 4. For each semantical setting, the factual validity of the postulate (Expected) and the actual results of Leo-III and Nitpick (Result) are presented. \(\checkmark \) and \(\times \) denote validity resp. invalidity of the postulate under the respective semantics as well as a system’s according result. A timeout of a system (i.e. no feasible result) is denoted \(\dagger \). Quantification semantics are abbreviated co and va for constant and varying domains, respectively.
Full size table

4 Summary and Further Work

In this work, a self-contained syntax for formulating higher-order modal logic problems was sketched that is used as input format to the Modal Embedding Tool. This stand-alone tool acts as external pre-processor for HO reasoning systems and emits for a given input problem statement an equivalent (wrt. validity) HOL problem formulated in standard THF syntax. MET is implemented in Java and freely available at GitHub under BSD-3 license.Footnote 2 The higher-order ATP system Leo-III additionally incorporates a version of MET for automatically embedding modal logic problems without any need for external pre-processing.

When used in conjunction with further powerful HO ATP systems, MET has many topical applications for reasoning in knowledge bases, legal reasoning, smart contracts and, more generally, in alethic, epistemic and deontic contexts. An adaption of MET for accepting RuleML input syntax [17], OWL [18] or further languages for rule-based reasoning is, thanks to the flexible underlying embedding approach, straight-forward and current work-in-progress [19]. The MET can also be extended to serve as a translation tool between these different representation formats.