Abstract. The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)". The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by Łukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.

## 1 Introduction

Research in Automated Deduction, also known as Automated Theorem Proving (ATP), has resulted in systems with a remarkable performance. Yet, deep mathematical theorems or otherwise complex statements still withstand any of the systems' attempts to find a proof. The present paper is motivated by the thesis that the reason for the failure in more complex problems lies in the local orientedness of all our current methods for proof search like resolution or connection calculi in use.

In order to find out more global features for directing proof search we start out here to study the structures of proofs for complex formulas in some detail and compare human proofs with those generated by systems. Complex formulas of this kind have been considered by Łukasiewicz in [19]. They are complex in the sense that current systems require tens of thousands or even millions of search steps for finding a proof if any, although the length of the formulas is very short indeed. How come that Łukasiewicz found proofs for those formulas although he could never carry out more than, say, a few hundred search steps by hand? Which global strategies guided him in finding those proofs? Could we discover such strategies from the formulas' global features?

By studying the proofs in detail we hope to come closer to answers to those questions. Thus it is proofs, rather than just formulas or clauses as usually in

c The Author(s) 2021

A. Platzer and G. Sutcliffe (Eds.): CADE 2021, LNAI 12699, pp. https://doi.org/10.1007/978-3-030-79876-5\_4 58–75, 2021.

ATP, which is in the focus of our study. In a sense we are aiming at an ATPoriented part of Proof Theory, a discipline usually pursued in Logic yet under quite different aspects. This meta-level perspective has rarely been taken in ATP for which reason we cannot rely on the existing conceptual basis of ATP but have to build an extensive conceptual basis for such a study more or less from scratch.

This investigation thus analyzes structures of, and operations on, proofs for formulas of the form "axiom(s) and rule(s) imply goal(s)". It renders condensed detachment, a logical rule historically introduced in the course of studying these complex proofs, as a restricted form of the Connection Method (CM) in ATP. All this is pursued with the goal of enhancing proof search in ATP in mind. As noted, our investigations are guided by a close inspection into proofs by Łukasiewicz and Meredith. In fact, the work presented here amounts at the same time to a very detailed reconstruction of those historical proofs.

The rest of the paper is organized as follows: In Sect. 2 we introduce the problem and a formal human proof that guides our investigations and compare different views on proof structures. We then reconstruct in Sect. 3 the historical method of condensed detachment in a novel way as a restricted variation of the CM where proof structures are represented as terms. This is followed in Sect. 4 by results on reducing the size of such proof terms for application in proof shortening and restricting the proof search space. Section 5 presents a detailed feature table for the investigated human proof, and Sect. 6 shows first experiments where the features and new techniques are used to supplement the inputs of ATP systems with lemmas. Section 7 concludes the paper. Supplementary technical material including proofs is provided in the report [37]. Data and tools to reproduce the experiments are available at http://cs.christophwernhard.com/cd.

#### 2 Relating Formal Human Proofs with ATP Proofs

In 1948 Jan Łukasiewicz published a formal proof of the completeness of his shortest single axiom for the implicational fragment (IF), that is, classical propositional logic with implication as the only logic operator [19]. In his notation the implication p → q is written as Cpq. Following Frank Pfenning [27] we formalize IF on the meta-level in the first-order setting of modern ATP with a single unary predicate P to be interpreted as something like "provable" and represent the propositional formulas by terms using the binary function symbol i for implication. We will be concerned with the following formulas.

IF can be axiomatized by the set of the three axioms Simp, Peirce and Syll, known as Tarski-Bernays Axioms. Alfred Tarski in 1925 raised the problem to

$$\overbrace{\operatorname{\mathbf{P}i(i(ipq,r),i(ipp,isp))}}^{\mathbf{4}} \land \overbrace{\operatorname{\mathbf{P}x \land \operatorname{\mathbf{P}ixy \to \operatorname{\mathbf{P}y}}}^{\mathbf{1}}}^{\mathbf{1}} \land \overbrace{\operatorname{\mathbf{P}i(ipq,i(iqr,ipr))}}^{\mathbf{1}}$$

Fig. 1. *ŁDS* along with its five unifiable connections.

characterize IF by a single axiom and solved it with very long axioms, which led to a search for the shortest single axiom, which was found with the axiom nicknamed after him in 1936 by Łukasiewicz [19]. In 1948 he published his derivation that Łukasiewicz entails the three Tarski-Bernays Axioms, expressed formally by the method of substitution and detachment. Detachment is also familiar as modus ponens. Łukasiewicz's proof involves 34 applications of detachment. Among the Tarski-Bernays axioms Syll is by far the most challenging to prove, hence his proof centers around the proof of Syll, with Peirce and Simp spinning off as side results. Carew A. Meredith presented in [24] a "very slight abridgement" of Łukasiewicz's proof, expressed in his framework of condensed detachment [28], where the performed substitutions are no longer explicitly presented but implicitly assumed through unification. Meredith's proof involves only 33 applications of detachment. In our first-order setting, detachment can be modeled with the following meta-level axiom.

$$\text{Det } \stackrel{\text{def}}{=} \forall xy \left( \mathbb{P}x \land \mathbb{P}ixy \to \mathbb{P}y \right).$$

In Det the atom Px is called the minor premise, Pixy the major premise, and Py the conclusion. Let us now focus on the following particular formula.

$$LDS \stackrel{\text{def}}{=} Luka\\sie wicz \wedge Det \to Syml.$$

"Problem ŁDS" is then the problem of determining the validity of the first order formula ŁDS. In view of the CM [1,2,3], a formula is valid if there is a spanning and complementary set of connections in it. In Fig. 1 ŁDS is presented again, nicknames dereferenced and quantifiers omitted as usual in ATP, with the five unifiable connections in it. Observe that p, q, r, s on the left side of the main implication are variables, while p, q,r on the right side are Skolem constants. Any CM proof of ŁDS consists of a number of instances of the five shown connections. Meredith's proof, for example, corresponds to 491 instances of Det, each linked with three instances of its five incident connections.

Figure 2 compares different representations of a short formal proof with the Det meta axiom. There is a single axiom, Syll Simp, and the theorem is ∀pqrstu Pi(p, i(q, i(r, i(s, i(t, ius))))). Figure 2a shows the structure of a CM proof. It involves seven instances of Det, shown in columns D1,...,D7. The major premise Pixiyi is displayed there on top of the minor premise Pxi, and the (negated) conclusion ¬Pyi, where xi, yi are variables. Instances of the axiom appear as literals ¬Pai, with ai a shorthand for the term i(i(ipiqi, ri), iqiri). The rightmost literal Pg is a shorthand for the Skolemized theorem. The clause instances are linked through edges representing connection instances. The edge

Fig. 2. A proof in different representations.

labels identify the respective connections as in Fig. 1. An actual connection proof is obtained by supplementing this structure with a substitution under which all pairs of literals related through a connection instance become complementary.

Figure 2b represents the tree implicit in the CM proof. Its inner nodes correspond to the instances of Det, and its leaf nodes to the instances of the axiom. Edges appear ordered to the effect that those originating in a major premise of Det are directed to the left and those from a minor premise to the right. The goal clause Pg is dropped. The resulting tree is a full binary tree, i.e., a binary tree where each node has 0 or 2 children. We observe that the ordering of the children makes the connection labeling redundant as it directly corresponds to the tree structure.

Figure 2c presents the proof in Meredith's notation. Each line shows a formula, line 1 the axiom and lines 2–4 derived formulas, with proofs annotated in the last column. Proofs are written as terms in Polish notation with the binary function symbol D for detachment where the subproofs of the major and minor premise are supplied as first and second, resp., argument. Formula 4, for example, is obtained as conclusion of Det applied to formula 2 as major premise and as minor premise another formula that is not made explicit in the presentation, namely the conclusion of Det applied to formula 3 as both, major and minor, premises. An asterisk marks the goal theorem.

Figure 2d is like Fig. 2b, but with a different labeling: Node labels now refer to the line in Fig. 2c that corresponds to the subproof rooted at the node. The blank node represents the mentioned subproof of the formula that is not made explicit in Fig. 2b. An inner node represents a condensed detachment step applied to the subproof of the major premise (left child) and minor premise (right child).

Figure 2e shows a DAG (directed acyclic graph) representation of Figure 2d. It is the unique maximally factored DAG representation of the tree, i.e., it has no multiple occurrences of the same subtree. Each of the four

Fig. 3. Proof MER, Meredith's refinement [24] of Łukasiewicz's proof [19].

proof line labels of Fig. 2c appears exactly once in the DAG.

We conclude this introductory section with reproducing Meredith's refinement of Łukasiewicz's completeness proof in Fig. 3, taken from [24]. Since we will often refer to this proof, we call it MER. There is a single axiom (1), which is Łukasiewicz . The proven theorems are Syll (17), Peirce (18) and Simp (19). In addition to line numbers also the symbol n appears in some of the proof terms. Its meaning will be explained later on in the context of Def. 19. For now, we can read n just as "1". Dots are used in the Polish notation to disambiguate numeric identifiers with more than a single digit.

#### 3 Condensed Detachment and a Formal Basis

Following [4], the idea of condensed detachment can be described as follows: Given premises F → G and H, we can conclude G , where G is the most general result that can be obtained by using a substitution instance H as minor premise with the substitution instance F → G as major premise in modus ponens. Condensed detachment was introduced by Meredith in the mid-1950s as an evolution of the earlier method of substitution and detachment, where the involved substitutions were explicitly given. The original presentations of condensed detachment are informal by means of examples [28,17,29,25], formal specifications have been given later [16,13,4]. In ATP, the rendering of condensed detachment by hyperresolution with the clausal form of axiom Det is so far the prevalent view. As overviewed in [23,31], many of the early successes of ATP were based on condensed detachment. Starting from the hyperresolution view, structural aspects of condensed detachment have been considered by Robert Veroff [34] with the use of term representations of proofs and linked resolution. Results of ATP systems on deriving the Tarski-Bernays axioms from Łukasiewicz are reported in [27,39,22,23,11]. Our goal in this section is to provide a formal framework that makes the achievements of condensed detachment accessible from a modern ATP view. In particular, the incorporation of unification, the interplay of nested structures with explicitly and implicitly associated formulas, sharing of structures through lemmas, and the availability of proof structures as terms.

Our notation follows common practice [6] (e.g., s ≥· t expresses that t subsumes s, and s ☎ t that t is a subterm of s) with some additions [37]. For formulas F we write the universal closure as ∀F, and for terms s, t, u we use s[t → u] to denote s after simultaneously replacing all occurrences of t with u.

#### 3.1 Proof Structures: D-Terms, Tree Size and Compacted Size

In this section we consider only the purely structural aspects of condensed detachment proofs. Emphasis is on a twofold view on the proof structure, as a tree and as a DAG (directed acyclic graph), which factorizes multiple occurrences of the same subtree. Both representation forms are useful: the compacted DAG form captures that lemmas can be repeatedly used in a proof, whereas the tree form facilitates to specify properties in an inductive manner. We call the tree representation of proofs by terms with the binary function symbol D D-terms.

Definition 1. (i) We assume a distinguished set of symbols called primitive D-terms. (ii) A D-term is inductively specified as follows: (1.) Any primitive D-term is a D-term. (2.) If d1 and d2 are D-terms, then D(d1, d2) is a D-term. (iii) The set of primitive D-terms occurring in a D-term d is denoted by Prim(d). (iv) The set of all D-terms that are not primitive is denoted by D.

A D-term is a full binary tree (i.e, a binary tree in which every node has either 0 or 2 children), where the leaves are labeled with symbols, i.e., primitive D-terms. An example D-term is

$$d \stackrel{\text{def}}{=} \mathsf{D}(\mathsf{D}(1,1), \mathsf{D}(\mathsf{D}(1,\mathsf{D}(1,1)), \mathsf{D}(1,\mathsf{D}(1,1)))),\tag{i}$$

which represents the structure of the proof shown in Fig. 2 and can be visualized by the full binary tree of Fig. 2d after removing all labels with exception of the leaf labels. The proof annotations in Fig. 2c and Fig. 3 are D-terms written in Polish notation. The expression D2D33 in line 4 of Fig. 2, for example, stands for the D-term D(2, D(3, 3)). Prim(D(2, D(3, 3))) = {2, 3}.

A finite tree and, more generally, a finite set of finite trees can be represented as DAG, where each node in the DAG corresponds to a subtree of a tree in the given set. It is well known that there is a unique minimal such DAG, which is maximally factored (it has no multiple occurrences of the same subtree) or, equivalently, is minimal with respect to the number of nodes, and, moreover, can be computed in linear time [7]. The number of nodes of the minimal DAG is the number of distinct subtrees of the members of the set of trees. There are two useful notions of measuring the size of a D-term, based directly on its tree representation and based on its minimal DAG, respectively.

Definition 2. (i) The tree size of a D-term d, in symbols t-size(d), is the number of occurrences of the function symbol D in d. (ii) The compacted size of a D-term d is defined as c-size(d) def = |{e ∈D| d ☎ e}|. (iii) The compacted size of a finite set D of D-terms is defined as c-size(D) def = |{e ∈D| d ∈ D and d ☎ e}|.

The tree size of a D-term can equivalently be characterized as the number of its inner nodes. The compacted size of a D-term is the number of its distinct compound subterms. It can equivalently be characterized as the number of the inner nodes of its minimal DAG. As an example consider the D-term d defined in formula (i), whose minimal DAG is shown in Fig. 2e. The tree size of d is t-size(d)=7 and the compacted size of d is c-size(d)=4, corresponding to the cardinality of the set {e ∈D| d ☎ e} of compound subterms of d, i.e., {D(1, 1), D(1, D(1, 1)), D(D(1, D(1, 1)), D(1, D(1, 1))), d}.

As will be explicated in more detail below, each occurrence of the function symbol D in a D-term corresponds to an instance of the meta-level axiom Det in the represented proof. Hence the tree size measures the number of instances of Det in the proof. Another view is that each occurrence of D in a D-term corresponds to a condensed detachment step, without re-using already proven lemmas. The compacted size of a D-term is the number of its distinct compound subterms, corresponding to the view that the size of the proof of a lemma is only counted once, even if it is used multiply. Tree size and compacted size of D-terms appear in [34] as CDcount and length, respectively.

#### 3.2 Proof Structures, Formula Substitutions and Semantics

We use a notion of unifier that applies to a set of pairs of terms, as convenient in discussions based on the CM [1,9,8].

Definition 3. Let M be a set of pairs of terms and let σ be a substitution. (i) σ is said to be a unifier of M if for all {s, t} ∈ M it holds that sσ = tσ. (ii) σ is called a most general unifier of M if σ is a unifier of M and for all unifiers σ of M it holds that σ ≥· σ. (iii) σ is called a clean most general unifier of M if it is a most general unifier of M and, in addition, is idempotent and satisfies Dom(σ) ∪ VRng(σ) ⊆ Var (M).

The additional properties required for clean most general unifiers do not hold for all most general unifiers.3 However, the unification algorithms known from the literature produce clean most general unifiers [9, Remark 4.2]. If a set of pairs of terms has a unifier, then it has a most general unifier and, moreover, also a clean most general unifier.

Definition 4. (i) If M is a set of pairs of terms that has a unifier, then mgu(M) denotes some clean most general unifier of M. M is called unifiable and mgu(M) is called defined in this case, otherwise it is called undefined. (ii) We make the convention that proposition, lemma and theorem statements implicitly assert their claims only for the case where occurrences of mgu in them are defined.

3 The inaccuracy observed by [13] in early formalizations of condensed detachment can be attributed to disregarding the requirement Dom(σ) ∪ VRng(σ) ⊆ Var (M).

Since we define mgu(M) as a clean most general unifier, we are permitted to make use of the assumption that it is idempotent and that all variables occurring in its domain and range occur in M. Convention 4.ii has the purpose to reduce clutter in proposition, lemma and theorem statements.

The structural aspects of condensed detachment proofs represented by D-terms, i.e., full binary trees, will now be supplemented with associated formulas. Condensed detachment proofs, similar to CM proofs, involve different instances of the input formulas (viewed as quantifier-free, e.g., clauses), which may be considered as obtained in two steps: first, "copies", that is, variants with fresh variables, of the input formulas are created; second a substitution is applied to these copies. Let us consider now the first step. The framework of D-terms permits to give the variables in the copies canonical designators with an index subscript that identifies the position in the structure, i.e., in the D-term, or tree.

Definition 5. For all positions p and positive integers i let xi p and yp denote pairwise different variables.

Recall that positions are path specifiers. For a given D-term d and leaf position p of d the variables xi p are for use in a formula associated with p which is the copy of an axiom. Different variables in the copy are distinguished by the upper index i. If p is a non-leaf position of d, then yp denotes the variable in the conclusion of the copy of Det that is represented by p. In addition, yp for leaf positions p may occur in the antecedents of the copies of Det. The following substitution shiftp is a tool to systematically rename position-associated variables while preserving the internal relationships between the index-referenced positions.

Definition 6. For all positions p define the substitution shiftp as follows: shiftp def = {yq → yp.q | q is a position}∪{xi q → xi p.q | i ≥ 1 and q is a position}.

The application of shiftp to a term s effects that p is prepended to the position indexes of all the position-associated variables occurring in s. The association of axioms with primitive D-terms is represented by mappings which we call axiom assignments, defined as follows.

Definition 7. An axiom assignment α is a mapping whose domain is a set of primitive D-terms and whose range is a set of terms whose variables are in {xi -| i ≥ 1}. We say that α is for a D-term d if Dom(α) ⊇ Prim(d).

We define a shorthand for a form of Łukasiewicz that is suitable for use as a range element of axiom assignments. It is parameterized with a position p.

$$Luka sie wicz\_p \stackrel{\text{def}}{=} \mathfrak{i}(\mathfrak{i}(\mathfrak{i}(x\_p^1, x\_p^2), x\_p^3), \mathfrak{i}(\mathfrak{i}(x\_p^3, x\_p^1), \mathfrak{i}(x\_p^4, x\_p^1))).\tag{\text{ii}}$$

The mapping {1 → Łukasiewicz -} is an axiom assignment for all D-terms d with Prim(d) = {1}. The second step of obtaining the instances involved in a proof can be performed by applying the most general unifier of a pair of terms that constrain it. The tree structure of D-terms permits to associate exactly one such pair with each term position. Inner positions represent detachment steps and leaf positions instances of an axiom according to a given axiom assignment. The following definition specifies these constraining pairs.

Definition 8. Let d be a D-term and let α be an axiom assignment for d. For all positions p ∈ Pos(d) define the pair of terms pairingα(d, p) def = {yp, α(d|p)shiftp} if p ∈ Leaf Pos(d) and {yp.1, i(yp.2, yp)} if p ∈ InnerPos(d).

A unifier of the set of pairings of all positions of a D-term d equates for a leaf position p the variable yp with the value of the axiom assignment α for the primitive D-term at p, after "shifting" variables by p. This "shifting" means that the position subscript of the variables in the axiom argument term α(d|p) is replaced by p, yielding a dedicated copy of the axiom argument term for the leaf position p. For inner positions p the unifier equates yp.1 and i(yp.2, yp), reflecting that the major premise of Det is proven by the left child of p.

The substitution induced by the pairings associated with the positions of a D-term allow to associate a specific formula with each position of the D-term, called the in-place theorem (IPT). The case where the position is the top position is distinguished as most general theorem (MGT).

Definition 9. For D-terms d, positions p ∈ Pos(d) and axiom assignments α for d define the in-place theorem (IPT) of d at p for α, Iptα(d, p), and the most general theorem (MGT) of d for α, Mgtα(d), as (i) Iptα(d, p) def = P(ypmgu({pairingα(d, q) | q ∈ Pos(d)})). (ii) Mgtα(d) def = Iptα(d, ).

Since Ipt and Mgt are defined on the basis of mgu, they are undefined if the set of pairs of terms underlying the respective application of mgu is not unifiable. Hence, we apply the convention of Def. 4.ii for mgu also to occurrences of Ipt and Mgt. If Ipt and Mgt are defined, they both denote an atom whose variables are constrained by the clean property of the underlying application of mgu. The following proposition relates IPT and MGT with respect to subsumption.

Proposition 10. For all D-terms d, positions p ∈ Pos(d) and axiom assignments α for d it holds that Iptα(d, p) ≥· Mgtα(d|p).

By Prop. 10, the IPT at some position p of a D-term d is subsumed by the MGT of the subterm d|p of d rooted at position p. An intuitive argument is that the only constraints that determine the most general unifier underlying the MGT are induced by positions of d|p, that is, below p (including p itself). In contrast, the most general unifier underlying the IPT is determined by all positions of d.

The following lemma expresses the core relationships between a proof structure (a D-term), a proof substitution (accessed via the IPT) and semantic entailment of associated formulas.

Lemma 11. Let d be a D-term and let α be an axiom assignment for d. Then for all p ∈ Pos(d) it holds that: (i) If p ∈ Leaf Pos(d), then ∀P(α(d|p)) |= Iptα(d, p). (ii) If p ∈ InnerPos(d), then Det ∧ Iptα(d, p.1) ∧ Iptα(d, p.2) |= Iptα(d, p).

Based on this lemma, the following theorem shows how Detachment together with the axioms in an axiom assignment entail the MGT of a given D-term.

Theorem 12. Let d be a D-term and let α be an axiom assignment for d. Then Det ∧ - p∈Leaf Pos(d) ∀P(α(d|p)) |= ∀Mgtα(d).

Theorem 12 states that Det together with the axioms referenced in the proof, that is, the values of α for the leaf nodes of d considered as universally closed atoms, entail the universal closure of the MGT of d for α. The universal closure of the MGT is the formula exhibited in Meredith's proof notation in the lines with a trailing D-term, such as lines 2–19 in Fig. 3.

#### 4 Reducing the Proof Size by Replacing Subproofs

The term view on proof trees suggests to shorten proofs by rewriting subterms, that is, replacing occurrences of subproofs by other ones, with three main aims: (1) To shorten given proofs, with respect to the tree size or the compacted size. (2) To investigate given proofs whether they can be shortened by certain rewritings or are closed under these. (3) To develop notions of redundancy for use in proof search. A proof fragment constructed during search may be rejected if it can be rewritten to a shorter one.

It is obvious that if a D-term d is obtained from a D-term d by replacing an occurrence of a subterm e with a D-term e such that t-size(e) ≥ t-size(e ), then also t-size(d) ≥ t-size(d ). Based on the following ordering relations on D-terms, which we call compaction orderings, an analogy for reducing the compacted size instead of the tree size can be stated.

Definition 13. For D-terms d, e define (i) d ≥c e def = {f ∈D| d ✄ f}⊇{f ∈ D | e ✄ f}. (ii) d >c e def = d ≥c e and e ≥c d.

The relations d ≥c e and d >c e compare D-terms d and e with respect to the superset relationship of their sets of those strict subterms that are compound terms. For example, D(D(D(1, 1), 1), 1) >c D(1, D(1, 1)) because {D(1, 1), D(D(1, 1), 1)} ⊇ {D(1, 1)}.

Theorem 14. Let d, d , e, e be D-terms such that e occurs in d, and d = d[e → e ]. It holds that (i) If e ∈ D and e ≥c e , then c-size(d) ≥ c-size(d ). (ii) If e >c e , then sc-size(d) > sc-size(d ), where, for all D-terms d sc-size(d) def = d☎e c-size(e).

Theorem 14.i states that if d is the D-term obtained from d by simultaneously replacing all occurrences of a compound D-term e with a "c-smaller" D-term e , i.e., e ≥c e , then the compacted size of d is less or equal to that of d. As stated with the supplementary Theorem 14.ii, the sc-size is a measure that strictly decreases under the strict precondition e >c e , which is useful to ensure termination of rewriting. The following proposition characterizes the number of D-terms that are smaller than a given D-term w.r.t the compaction ordering ≥c.

Proposition 15. For all D-terms d it holds that |{e | d ≥c e and Prim(e) ⊆ Prim(d)}| = (c-size(d) − 1 + |Prim(d)|)2 + |Prim(d)|.

By Prop. 15, for a given D-term d, the number of D-terms e that are smaller than d with respect to ≥c is only quadratically larger than the compacted size of d and thus also than the tree size of d. Hence techniques that inspect all these smaller D-terms for a given D-term can efficiently be used in practice.

According to Theorem 12, a condensed detachment proof, i.e., a D-term d and an axiom assignment α, proves the MGT of d for α along with instances of the MGT. In general, replacing subterms of d should yield a proof of at least these theorems. That is, a proof whose MGT subsumes the original one. The following theorem expresses conditions which ensure that subterm replacements yield a proof with a MGT that subsumes original one.

Theorem 16. Let d, e be D-terms, let α be an axiom assignment for d and for e, and let p1,...,pn, where n ≥ 0, be positions in Pos(d) such that for all i, j ∈ {1,...,n} with i = j it holds that pi ≤ pj . If for all i ∈ {1,...,n} it holds that Iptα(d, pi) ≥· Mgtα(e), then Mgtα(d) ≥· Mgtα(d[e]p1 [e]p2 ... [e]pn ).

Theorem 16 states that simultaneously replacing a number of occurrences of possibly different subterms in a D-term by the same subterm with the property that its MGT subsumes each of the IPTs of the original occurrences results in an overall D-term whose MGT subsumes that of the original overall D-term. The following theorem is similar, but restricted to a single replaced occurrence and with a stronger precondition. It follows from Theorem 16 and Prop. 10.

Theorem 17. Let d, e be D-terms and let α be an axiom assignment for d and for e. For all positions p ∈ Pos(d) it then holds that if Mgtα(d|p) ≥· Mgtα(e), then Mgtα(d) ≥· Mgtα(d[e]p).

Simultaneous replacements of subterm occurrences are essential for reducing the compacted size of proofs according to Theorem 14. For replacements according to Theorem 17 they can be achieved by successive replacements of individual occurrences. In Theorem 16 simultaneous replacements are explicitly considered because the replacement of one occurrence according to this theorem can invalidate the preconditions for another occurrence. Theorem 17 can be useful in practice because the precondition Mgtα(d|p) ≥· Mgtα(e) can be evaluated on the basis of α, e and just the subterm d|p of d, whereas determining Iptα(d, p) for Theorem 16 requires also consideration of the context of p in d. Based on Theorems 16 and 14 we define the following notions of reduction and regularity.

Definition 18.  For D-terms e the D-term d[e → e ] is then obtained by C-reduction from d for α if e >c e , Mgtα(e ) is defined, and for all positions p ∈ Pos(d) such that d|p = e it holds that Iptα(d, p) ≥· Mgtα(e ). The D-term d is called C-reducible for α if and only if there exists a D-term e such that d[e → e ] is obtained by C-reduction from d for α. Otherwise, d is called C-regular.

If d is obtained from d by C-reduction, then by Theorem 16 and 14 it follows that Mgtα(d) ≥· Mgtα(d ), c-size(d) ≥ c-size(d ) and sc-size(d) > sc-size(d ). Cregularity differs from well known concepts of regularity in clausal tableaux (see, e.g., [14]) in two respects: (1) In the comparison of two nodes on a branch (which is done by subsumption as in tableaux with universal variables) for the upper node the stronger instantiated IPT is taken and for the lower node the more weakly instantiated MGT. (2) C-regularity is not based on relating two nested subproofs, but on comparison of all occurrences of a subproof with respect to all proofs that are smaller with respect to the compaction ordering.

Proofs may involve applications of Det where the conclusion Py is actually independent from the minor premise Px. Any axiom can then serve as a trivial minor premise. Meredith expresses this with the symbol n as second argument of the respective D-term. Our function simp-n simplifies D-terms by replacing subterms with n accordingly on the basis of the preservation of the MGT.

Definition 19. If d is a D-term and α is an axiom assignment for d, then the n-simplification of d with respect to α is the D-term simp-nα(d), where simp-n is the following function: simp-nα(d) def = d, if d is a primitive D-term; simp-nα(D(d1, d2)) def = D(simp-nα- (d1), n) if Mgtα-D(d1, n) = MgtαD(d1, d2), where α = α ∪ {n → k} for a fresh constant k; simp-nα(D(d1, d2)) def = D(simp-nα(d1),simp-nα(d2)), else.

#### 5 Properties of Meredith's Refined Proof

Our framework renders condensed detachment as a restricted form of the CM. This view permits to consider the expanded proof structures as binary trees or D-terms. On this basis we obtain a natural characterization of proof properties in various categories, which seem to be the key towards reducing the search space in ATP. Table 1 shows such properties for each of the 34 structurally different subproofs of proof MER (Fig. 3). Column M gives the number of the subproof in Fig. 3. We use the following short identifiers for the observed properties:

Structural Properties of the D-Term. These properties refer to the respective subproof as D-term or full binary tree. DT, DC, DH: Tree size, compacted size, height. DKL, DKR: "Successive height", that is, the maximal number of successive edges going to the left (right, resp.) on any path from the root to a leaf. DP: Is "prime", that is, DT and DC are equal. DS: Relationship between the subproofs of major and minor premise. Identity is expressed with =, the subterm and superterm relationships with ✁ and ✄, resp., and the compaction ordering relationship (if none of the other relationships holds) with <c and >c. In addition it is indicated if a subproof is an axiom or n. DD: "Direct sharings", that is, the number of incoming edges in the DAG representation of the overall proof of all theorems. DR: "Repeats", that is, the total number of occurrences in the set of expanded trees of all roots of the DAG.

Properties of the MGT. These properties refer to the argument term of the MGT of the respective subproof. TT, TH: Tree size (defined as for D-terms) and height. TV: Number of different variables occurring in the term. TO: Is "organic" [21], that is, the argument term has no strict subterm s such that P(s) itself is a theorem. We call an atom weakly organic (indicated by a gray bullet) if it is not organic and the argument term is of the form i(p, t) where p is a variable that does not occur in the term t and P(t) is organic. For axiomatizations of fragments of propositional logic, organic can be checked by a SAT solver.

Regularity. RC: The respective subproof as D-term is C-regular (see Def. 18).

Table 1. Properties of all subproofs of the proof MER [24] shown in Fig. 3.

Comparisons with all Proofs of the MGT. These properties relate to the set of all proofs (as D-terms) of the MGT of the respective subproof. MT, MC: Minimal tree size and minimal compacted size of a proof. These values can be hard to determine such that in Table 1 they are often only narrowed down by an integer interval. To determine them, we used the proof MER, proofs obtained with techniques described in Sect. 6, and enumerations of all D-terms with defined MGT up to a given tree size or compacted size.

Properties of Occurrences of the IPTs. The respective subproof has DR occurrences in the set of expanded trees of the roots of the DAG, where each occurrence has an IPT. The following properties refer to the multiset of argument terms of the IPTs of these occurrences. ITU , ITM: Maximal tree size and rounded median of the tree size. IHU , IHM: Maximal height and rounded median of the height. In Table 1 these values are much larger than those of the corresponding columns for the MGT, i.e, TT and TH, illustrating Prop. 10.

## 6 First Experiments

First experiments based on the framework developed in the previous sections are centered around the generation of lemmas where not just formulas but, in the form of D-terms, also proofs are taken into account. This leads in general to preference of small proofs and to narrowing down the search space by re-

Table 2. Proof dimensions of various proofs of problem *ŁDS*.

stricted structuring principles to build proofs. The experiments indicate novel potential calculi which combine aspects from lemma-based generative, bottomup, methods such as hyperresolution and hypertableaux with structure-based approaches that are typically used in an analytic, goal-directed, way such as the CM. In addition, ways to generate lemmas as preprocessing for theorem proving are suggested, in particular to obtain short proofs. This resulted in a refinement of Łukasiewicz's proof [19], whose compacted size is by one smaller than that of Meredith's refinement [24] and by two than Łukasiewicz's original proof.

Table 2 shows compacted size DC, tree size DT and height DH of various proofs of ŁDS. Asterisks indicate that n-simplification was applied with reducing effect on the system's proof. Proof (1.) is the one by Łukasiewicz [19], translated into condensed detachment, proof (2.) is proof MER (Fig. 3) [24]. Rows (3.)–(5.) show results from Prover9 , where in (5.) the value of max\_depth was limited to 7, motivated by column TH of Table 1. Proof (4.) illustrates the effect of nsimplification.4 For proofs (6.)–(9.) additional axioms were supplied to Prover9 and CMProver [5,35,36], a goal-directed system that can be described by the CM. Columns indicate the lemma computation method, the number of lemmas supplied to the prover and the time used for lemma computation. Method PrimeCore adds the MGTs of subproof 18 from Table 1 and all its subproofs as lemmas. Subproof 18 is the largest subproof of proof MER that is prime and can be characterized on the basis of the axiom – almost uniquely – as a proof that is prime, whose MGT has no smaller prime proof and has the same number of different variables as the axiom, i.e., 4, and whose size, given as parameter, is 17. Method ProofSubproof is based on detachment steps with a D-term and a subterm of it as proofs of the premises, which, as column DS of Table 1 shows, suffices to justify all except of two proof steps in MER. It proceeds in some analogy to the given clause algorithm on lists of D-terms: If d is the given D-term, then the inferred D-terms are all D-terms that have a defined MGT and are of the form D(d, e) or D(e, d), where e is a subterm of d. To determine which of the inferred D-terms are kept, values from Table 1 were taken as guide, including RC and TO. The first parameter of ProofSubproof is the number of iterations of the "given D-term loop". Proof (9.) can be combined with Peirce and Syll to the overall proof with compacted size 32, one less than MER. The maximal value of DKL is shown as second parameter, because, when limited to 7, proof (9.)

4 All machine results refer to a system with Intel i7-8550U CPU and 16 GB RAM. Results for further systems: *KRHyper*∗ [26]: 1.610 s, DC: 73; *E 2.5* [30]: 30 s, proof length 91; *Vampire 5.4.1* [33] –mode casc -t 300: 128 s, proof length 144.

cannot be found. Proof (10.), which has a small tree size, was obtained from (8.) by rewriting subproofs with a variation of C-reduction that rewrites single term occurrences, considering also D-terms from a precomputed table of small proofs.

## 7 Conclusion

Starting out from investigating Łukasiewicz's classic formal proof [19], via its refinement by Meredith [24] we arrived at a formal reconstruction of Meredith's condensed detachment as a special case of the CM. The resulting formalism yields proofs as objects of a very simple and common structure: full binary trees which, in the tradition of term rewriting, appear as terms, D-terms, as we call them. To form a full proof, formulas are associated with the nodes of D-terms: axioms with the leaves and lemmas with the remaining nodes, implicitly determined from the axioms through the node position and unification. The root lemma is the most general proven theorem. Lemmas also relate to compressed representations of the binary trees, for example as DAGs, where the re-use of a lemma directly corresponds to sharing the structure of its subproof. For future work we intend to position our approach also in the context of earlier works on proofs, proof compression and lemma introduction, e.g., [38,12], and think of compressing D-Terms in forms that are stronger than DAGs, e.g., by tree grammars [18].

The combination of formulas and explicitly available proof structures naturally leads to theorem proving methods that take structural aspects into account, in various ways, as demonstrated by our first experiments. This goes beyond the common clausal tableau realizations of the CM, which in essence operate by enumerating uncompressed proof structures. The discussed notions of regularity and lemma generation methods seem immediately suited for further investigations in the context of first-order theorem proving in general. For other aspects of the work we plan a stepwise generalization by considering further single axioms for the implicational fragment IF [21,19,32], single axioms and axiom pairs for further logics [32], the about 200 condensed detachment problems in the LCL domain of the TPTP, problems which involve multiple non-unit clauses, and adapting D-terms to a variation of binary resolution instead of detachment. In the longer run, our approach aims at providing a basis for approaches to theorem proving with machine learning (e.g. [10,15]). With the reification of proof structures more information is available as starting point. As indicated with our exemplary feature table for Meredith's proof, structural properties are considered thereby from a global point of view, as a source for narrowing down the search space in many different ways in contrast to just the common local view "from within a structure", where the narrowing down is achieved for example by focusing on a "current branch" during the construction of a tableau. A general lead question opened up by our setting is that for exploring relationships between properties of proof structures and the associated formulas in proofs of meaningful theorems. One may expect that characterizations of these relationships can substantially restrict the search space for finding proofs.

Acknowledgments. We appreciate the competent comments of all the referees.

## References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

**Efficient Local Reductions to Basic Modal Logic***-*

> Fabio Papacchini1 , Cl´audia Nalon2 , Ullrich Hustadt1 , and Clare Dixon4

1 Department of Computer Science, University of Liverpool, UK<EMAIL_ADDRESS>2 Department of Computer Science, University of Bras´ılia<EMAIL_ADDRESS>3 Department of Computer Science, University of Manchester<EMAIL_ADDRESS>
**Abstract.** We present novel reductions of the propositional modal logics KB, KD, KT, K4 and K5 to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover KSP to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover KSP performs well when compared with a specialised resolution calculus for these logics and with the built-in reductions of the first-order ˘ prover SPASS.

#### **1 Introduction**

The main motivation for reducing problems in one logic (the source logic) to 'equivalent' problems in another logic (the target logic) is to exploit results and tools for the target logic to solve theoretical or practical problems in the source logic. For propositional modal logics this approach has been researched extensively for reductions of the satisfiability problem in these logics to the satisfiability problem in 'stronger' logics such as first-order logic [10,20], the second-order theory of n successors [6], simple type theory [4], and regular grammar logics [19].

An alternative approach is to reduce propositional modal logics to a 'weaker' logic, in particular, the basic modal logic K. For extensions of K with one of the axioms B, D, alt1, T, and 4, Kracht [12] defines reduction functions of their global and local satisfiability problem to the corresponding problem in K and proves their correctness. He also defines a reduction function for K5, the extension of K with 5, to K4, but this reduction is incorrect as not all theorems of K4 are theorems of K5. Several features of Kracht's approach are relevant to our work. First, as is not uncommon in modal logic, he treats the modal operator ✸ as abbreviation for ¬✷¬, that is, ✷ is the only modal operator occurring in modal formulae. Second, the basic idea underlying his reduction functions

- C. Dixon was partially supported by the EPSRC funded RAI Hubs FAIR-SPACE (EP/R026092/1) and RAIN (EP/R026084/1), and the EPSRC funded programme Grant S4 (EP/N007565/1).

c The Author(s) 2021

A. Platzer and G. Sutcliffe (Eds.): CADE 2021, LNAI 12699, pp. 76 92, 2021. https://doi.org/10.1007/978-3-030-79876-5 5 –

is for a given modal formula ϕ to generate sufficiently many instances Δ of a modal axiom Λ so that ϕ is KΛ-satisfiable iff ϕ ∧ Δ is K-satisfiable. Third, Kracht is only concerned with preservation of the computational complexity of the satisfiability problem under consideration, as well as the preservation of other theoretical properties. For instance, the local satisfiability problem in the modal logics covered by Kracht is PSPACE-complete. So, it is sufficient to ensure that Δ is polynomial in size with respect to ϕ. As Kracht himself concludes, his method offers a uniform way of transferring results about one modal logic to another, but may not be as useful for practical applications.

In [16,15] we have introduced a new normal form for basic multi-modal logic, called Separated Normal Form with Modal Levels, SNFml, that uses labelled modal clauses. These labels refer to the level within a tree Kripke structure at which a modal clause holds. This can be seen as a compromise between approaches that label formulae with worlds at unspecified level [1,3] and approaches that label formulae with paths [5,23]. A combination of a normal form transformation for modal formulae and a resolution-based calculus for labelled modal clauses can then be used to decide local and global satisfiability in basic modal logic. In [17,18] we have presented KSP, an implementation of that calculus, together with an experimental evaluation that indicates that KSP performs well if propositional variables are evenly spread across a wide range of modal levels within the formulae one wants to decide.

A feature of SNFml is its use of additional propositional symbols as 'surrogates' for subformulae of a modal formula ϕ. In the following we take advantage of the availability of those surrogates to provide a novel transformation from extensions of K with a single one of the axioms B, D, T, 4 and 5 to SNFml. Another novel aspect is that we modify the normal form so that it uses sets of modal levels as labels instead of a single modal level. In K we only need a definition of a surrogate at the modal level at which the corresponding subformula occurs in ϕ. But in KB, KT, K4 and K5, we need a definition at every reachable modal level, of which there can be many. We call the resulting normal form, *Separated Normal Form with Sets of Modal Levels*, SNFsml.

The structure of the paper is as follows. In Section 2 we recap common concepts of propositional modal logic including its syntax and semantics. Section 3 defines SNFsml and the reductions of K, KB, KD, KT, K4 and K5 to SNFsml. Correctness is proved in Section 4. Related work is discussed in Section 5. In Section 6 we compare the performance of a combination of our reductions and the modal-layered resolution calculus implemented in prover KSP with resolution calculi specifically designed for the logics under consideration and with translation-based approaches built into the first-order theorem prover SPASS.

#### **2 Preliminaries**

The language of modal logic is an extension of the language of propositional logic with a unary modal operator ✷ and its dual ✸. More precisely, given a denumerable set of *propositional symbols*, P = {p, p0, q, q0, t, t0,...} as well as propositional *constants* **true** and **false**, *modal formulae* are inductively defined as follows: Constants and propositional symbols are modal formulae. If ϕ and ψ are modal formulae, then so are ¬ϕ, (ϕ ∧ ψ), (ϕ ∨ ψ), (ϕ → ψ), ✷ϕ, and ✸ϕ. We also assume that ∧ and ∨ are associative and commutative operators and consider, e.g., (p∨(q∨r)) and (r∨(q∨p)) to be identical formulae. We often omit parentheses if this does not cause confusion. By var(ϕ) we denote the set of all propositional symbols occurring in ϕ. This function straightforwardly extends to finite sets of modal formulae. A *modal axiom (schema)* is a modal formula ψ representing the set of all instances of ψ.

A *literal* is either a propositional symbol or its negation; the set of literals is denoted by L. We denote by ¬l the *complement* of the literal l ∈ L, that is, ¬l denotes ¬p if l is the propositional symbol p, and ¬l denotes p if l is the literal ¬p. A *modal literal* is either ✷l or ✸l, where l ∈ L.

A *(normal) modal logic* is a set of modal formulae which includes all propositional tautologies, the axiom schema ✷(ϕ → ψ) → (✷ϕ → ✷ψ), called the *axiom* K, is closed under modus ponens (if ϕ and ϕ → ψ then ψ) and the rule of necessitation (if ϕ then ✷ϕ).

K is the weakest modal logic, that is, the logic given by the smallest set of modal formulae constituting a normal modal logic. By KΣ we denote an *extensions* of K by a set Σ of axioms.

The standard semantics of modal logics is the *Kripke semantics* or *possible world semantics*. A *Kripke frame* F is an ordered pair W, R where W is a non-empty set of *worlds* and R is a binary (accessibility) relation over W. A *Kripke structure* M over P is an ordered pair F, V where F is a Kripke frame and the *valuation* V is a function mapping each propositional symbol in P to a subset V (p) of W. We say M = F, V is *based on the frame* F. A *rooted Kripke structure* is an ordered pair M,w0 with w0 ∈ W. To simplify notation, in the following we write W, R, V and W, R, V, w0 instead of W, R, V and W, R, V , w0, respectively.

Satisfaction (or truth) of a formula at a world w of a Kripke structure M = W, R, V is inductively defined by:

M,w |= **true**; M,w |= **false**; M,w |= p iff w ∈ V (p), where p ∈ P; M,w |= ¬ϕ iff M,w |= ϕ; M,w |= (ϕ ∧ ψ) iff M,w |= ϕ and M,w |= ψ; M,w |= (ϕ ∨ ψ) iff M,w |= ϕ or M,w |= ψ; M,w |= (ϕ → ψ) iff M, w |= ¬ϕ or M,w |= ψ; M,w |= ✷ϕ iff for every v, wRv implies M,v |= ϕ; M,w |= ✸ϕ iff there is v, wRv and M,v |= ϕ.

If M,w |= ϕ holds then M is a *model* of ϕ, ϕ is *true at* w *in* M and M *satisfies* ϕ. A modal formula ϕ is *satisfiable* iff there exists a Kripke structure M and a world w in M such that M,w |= ϕ. A modal formula ϕ is *globally true* or *valid* in a Kripke structure M if it is true at all worlds of M; it is *valid* if it is valid in all Kripke structures.

**Table 1.** Modal axioms and relational frame properties

In the following we are interested in extensions of K with the axiom schemata shown in Table 1. Each of these axiom schemata defines a class of Kripke frames where the accessibility relation R satisfies the first-order property stated in the table. Given a normal modal logic L with corresponding class of frames F, we say a modal formula ϕ is L*-satisfiable* iff there exists a frame F ∈ F, a valuation V and a world w0 ∈ F such that F, V, w0 |= ϕ.

A *path rooted at* w *of length* k, k ≥ 0, in a frame F = W, R is a sequence w = (w0, w1,...,wk) where for every i, 1 ≤ i ≤ k, wi−1 R wi. We say that the path (w0, w1,...,wk) *connects* w0 *and* wk. For a path w = (w0,...,wk) and world wk+1 with wk R wk+1, w ◦ wk+1 denotes the path (w0,...,wk, wk+1). A path (w0) of length 0 is identified with its root w0. We denote the set of all paths rooted at a world w0 in F by F [w0] and the set of all paths by F . The function trm : F → W maps every path w = (w0,...,wk) to its terminal world wk while the function len : F → N maps every path w = (w0, w1,...,wk) to its length k.

A rooted Kripke structure M = W, R, V, w0 is a *rooted tree Kripke structure* iff R is a tree, that is, a directed acyclic connected graph where each node has at most one predecessor, with *root* w0. It is a *rooted tree Kripke model* of a modal formula ϕ iff W, R, V, w0 |= ϕ. In a rooted tree Kripke structure with root w0 for every world wk ∈ W there is exactly one path w connecting w0 and wk; the *modal level of* wk *(in* M*), denoted by* mlM(wk), is given by len( w).

Let F = W, R be a Kripke frame with w ∈ W. The *unravelling* F u[w] *of* F *at* w is the frame W , R where:

**–** W = F [w] is the set of all rooted paths at w in F;

**–** for all v, w ∈ W , if w = v ◦ w for some w ∈ W, then v R w.

Let F = W, R and F = W , R be two Kripke frames. A function f : W → W is a *p-morphism* (or a *bounded morphism*) from F to F if the following holds: **–** if vRw, then f(v) R f(w).

**–** if f(u) R w, then there exists v ∈ W s.t. f(v) = w and uRv.

Analogously for Kripke models. For F = W, R, M = F, V , w0, and M = F u[w0],V,(w0), the function trm is a p-morphism from M to M .

When considering local satisfiability, the following holds (see, [8]):

**Theorem 1.** *Let* ϕ *be a modal formula. Then* ϕ *is* K*-satisfiable iff there is a finite rooted tree Kripke structure* M = F, V, w0 *such that* M,w0 |= ϕ*.*

```
ϕ ∧ ϕ ⇒ ϕ
   ϕ ∨ ϕ ⇒ ϕ
ϕ ∧ true ⇒ ϕ
                ϕ ∧ ¬ϕ ⇒ false
                ϕ ∨ ¬ϕ ⇒ true
              ϕ ∧ false ⇒ false
                                  ✷true ⇒ true
                                  ✸false ⇒ false
                                ϕ ∨ false ⇒ ϕ
                                                    ¬true ⇒ false
                                                    ¬false ⇒ true
                                                  ϕ ∨ true ⇒ true
                                                                   ¬¬ϕ ⇒ ϕ
```
**Table 2.** Rewriting Rules for Simplification

For the normal form transformation presented in the next section we assume that any modal formula ϕ has been simplified by exhaustively applying the rewrite rules in Table 2 and is in Negation Normal Form (NNF), that is, a formula where only propositional symbols are allowed in the scope of negations. We say that such a formula is in *simplified NNF*.

## **3 Layered Normal Form with Sets of Levels**

A formula to be tested for satisfiability is first transformed into a normal form called *Separated Normal Form with Sets of Modal Levels*, SNFsml, whose language extends that of modal logic with labels consisting of sets of modal levels. Informally, we write S : ϕ, where S is a set of natural numbers, to denote that a formula ϕ is true at modal levels ml ∈ S. We write : ϕ instead of N : ϕ.

We introduce some notation that will be used in the following. Let S+ = {l+ 1 ∈ N | l ∈ S}, S− = {l−1 ∈ N | l ∈ S}, and S≥ = {n | n ≥ min(S)}, where min(S) is the least element in S. Note that the restriction of the elements being in N implies that S− cannot contain negative numbers.

The labels in SNFsml work as a kind of *weak* universal operator, allowing us to talk about formulae that are satisfied at all worlds in a given set of modal levels. Formally, we restrict ourselves to rooted tree Kripke structures M = W, R, V, w0 and if S is a set of modal levels, then by M[S] we denote the set of worlds that are at a modal level in S, that is, M[S] = {w ∈ W | mlM(w) ∈ S}. The satisfaction of labelled formulae in a rooted tree Kripke structure M is then defined as follows:

M |= S : ϕ iff for every world w ∈ M[S], we have M,w |= ϕ.

If M |= S : ϕ, then we say that S : ϕ holds in M. Note that if S = ∅, then M |= S : ϕ trivially holds. For a set Φ of labelled formulae, M |= Φ iff M |= S : ϕ for every S : ϕ in Φ, and we say Φ is K*-satisfiable*.

A labelled modal formula is then an SNFsml clause iff it is of one of the following forms:

where S ⊆ N and l, l , lb are propositional literals with 1 ≤ b ≤ r, r ∈ N. Positive and negative modal clauses are together known as *modal clauses*. We regard a literal clause as a set of literals, that is, two clauses are the same if they contain the same set of literals.

We assume that the set P of propositional symbols is partitioned into two infinite sets Q and T such that for every modal formula ψ we have var(ψ) ⊂ Q and there exists a propositional symbol tψ ∈ T uniquely associated with ψ.

Given a modal formula ϕ in simplified NNF and L ∈ {K,KB,KD,KT,K4,K5}, then we can obtain a set ΦL of clauses in SNFsml such that ϕ is L-satisfiable iff ΦL is K-satisfiable as ΦL = {{0} : tϕ} ∪ ρL({0} : tϕ → ϕ), where ρL is defined as follows:

$$\begin{aligned} \rho\_L(S:t \to \mathtt{true}) &= \emptyset \\ \rho\_L(S:t \to \mathtt{false}) &= \{S: \neg t\} \\ \rho\_L(S:t \to (\psi\_1 \land \psi\_2)) &= \{S: \neg t \lor \eta(\psi\_1), S: \neg t \lor \eta(\psi\_2)\} \cup \delta\_L(S, \psi\_1) \cup \delta\_L(S, \psi\_2) \\ \rho\_L(S:t \to \psi) &= \{S: \neg t \lor \psi\} \end{aligned}$$

if ψ is a disjunction of literals

$$\rho\_L(S:t \to (\psi\_1 \lor \psi\_2)) = \{ S: \neg t \lor \eta(\psi\_1) \lor \eta(\psi\_2) \} \cup \delta\_L(S, \psi\_1) \cup \delta\_L(S, \psi\_2)$$

$$\text{if } \psi\_1 \lor \psi\_2 \text{ is not a disjoint of literals}$$

$$\rho\_L(\mathcal{S}:t \to \neg \diamond \psi) = \{ \mathcal{S}:t \to \neg \diamond \eta(\psi) \} \cup \delta\_L(\mathcal{S}^+, \psi)$$

$$\begin{aligned} \rho\_L(S:t \to \diamondsuit \psi) &= \{ S:t \to \diamondsuit \eta(\psi) \} \cup \delta\_L(S^+, \psi) \\ \rho\_L(S:t \to \square \psi) &= P\_L(S:t \to \square \psi) \cup \Delta\_L(S:t \to \square \psi) \end{aligned}$$

where η and δL are defined as follows:

$$\eta(\psi) = \begin{cases} \psi, & \text{if } \psi \text{ is a} \\ & \text{liter} \\ t\_{\psi}, & \text{otherwise} \end{cases} \qquad \delta\_L(S, \psi) = \begin{cases} \emptyset, & \text{if } \psi \text{ is a} \\ & \text{liter} \\ \rho\_L(S: t\_{\psi} \to \psi), & \text{otherwise} \end{cases}$$

and functions PL, ΔL are defined as shown in Table 3. The function η maps a propositional literal ψ to itself while it maps every other modal formula ψ to a new propositional symbol tψ ∈ T uniquely associated with ψ. We call tψ the *surrogate* of ψ or simply a surrogate. The functions PKB and PK5 introduce additional propositional symbols, called *supplementary propositional symbols*, t✷¬t✷ψ ∈ T and t✸t✷ψ ∈ T, respectively, that do not correspond to subformulae of the formula we are transforming.

Intuitively, PKB is based on the following consideration: Take a world w in a Kripke structure M with a symmetric accessibility relation R. If there exists a world v with wRv such that M,v |= ✷ψ, then M,w |= ψ. Now, take the contrapositive of that statement: If M,w |= ψ, then for every world v with wRv, M,v |= ✷ψ. Equivalently, M,w |= ψ or M,w |= ✷¬✷ψ. This is expressed by the formula η(ψ) ∨ t✷¬t✷ψ . For PK5 , the formula t✸t✷ψ → ✷t✸t✷ψ expresses an instance of axiom schema 5, ✸ϕ → ✷✸ϕ, with ϕ = ✷ψ, i.e., ✸✷ψ → ✷✸✷ψ. The contrapositive of axiom schema 5 is ✸✷ϕ → ✷ϕ, equivalent to ¬✸✷ϕ ∨ ✷ϕ. For ϕ = ψ this is expressed by the formula ¬t✸t✷ψ ∨ t✷ψ. For the formula ¬t✸t✷ψ → ✷¬t✷ψ, consider ¬✸✷ψ. By duality of ✷ and ✸, this is

**Table 3.** Transformation of ✷-formulae in modal logic L

equivalent to ¬¬✷¬✷ψ and ✷¬✷ψ. So, ¬✸✷ψ → ✷¬✷ψ in every normal modal logic, not only K5. The remaining labelled formulae introduced by PKB and PK5 ensure that supplementary propositional symbols are defined. For the remaining logics the additional clauses are also based directly on the axiom schemata.

To simplify presentation in the following, we define a function ηf as follows:

$$\begin{aligned} \eta\_f(\varphi\_1 \wedge \varphi\_2) &= \eta(\varphi\_1) \wedge \eta(\varphi\_2) & \eta\_f(\varphi\_1 \vee \varphi\_2) &= \eta(\varphi\_1) \vee \eta(\varphi\_2) \\ \eta\_f(\Box \varphi) &= \Box \eta(\varphi) & \eta\_f(\Diamond \varphi) &= \Diamond \eta(\varphi) \end{aligned}$$

and we treat the two clauses S : ¬tψ1∧ψ2 ∨ η(ψ1) and S : ¬tψ1∧ψ2 ∨ η(ψ2) resulting from the normal form transformation of ψ1 ∧ ψ2 as a single 'clause' S : ¬tψ1∧ψ2 ∨ ηf (ψ1 ∧ ψ2). We also interchangeably write S : ¬t✷ψ ∨ ηf (✷ψ) for S : t✷ψ → ηf (✷ψ) and, analogously, S : ¬t✸ψ ∨ ηf (✸ψ) for S : t✸ψ → ηf (✸ψ). We then call any clause of the form S : ¬tψ ∨ ηf (ψ) a *definitional clause*.

**Definition 1.** *Let* Φ *be a set of* SNFsml *clauses. We say* tψ ∈ T occurs at level ml in Φ *iff either*

**Definition 2.** *Let* Φ *be a set of* SNFsml *clauses. Then* Φ *is* definition-complete *iff for every* tψ ∈ T *and every level* ml*, if* tψ *occurs at level* ml *in* Φ *then there exists a clause* S : ¬tψ ∨ ηf (ψ) *in* Φ *with* ml ∈ S*.*

**Theorem 2.** *Let* L ∈ {K,KB,KD,KT,K4,K5}*. Then* ΦL = {{0} : tϕ} ∪ ρL({0} : tϕ → ϕ) *is definition-complete.*

*Proof.* By induction over the computation of ΦL. It is straightforward to see that the transformation of labelled formulae S : t → (ψ1 ∧ ψ2) and S : t → (ψ1 ∨ ψ2) only introduces surrogates at levels in S and ΔL then adds definitional clauses for those surrogates. The transformation of a labelled formula S : t✸ψ → ✸ψ may introduce a surrogate at levels in S+ and δL(S+, ψ) then adds definitional clauses for those surrogates. The transformation of a labelled formula S : t✷ψ → ✷ψ depends on the logic L. We can see that for every level at which a new surrogate occurs in PL(S : t✷ψ → ✷ψ), then ΔL(S : t✷ψ → ✷ψ) contains a definitional clause for it at that level.

#### **4 Correctness**

Due to space constraints we only prove the correctness of the transformation for KB. We first state several lemmata that are used in the correctness proofs for all logics.

**Lemma 1.** *Let* Φ *be a set of definitional clauses such that every* tψ *occurring in* Φ *is an element of* T *and all other propositional symbols occurring in* Φ *are in* Q*. Let* M = W, R, V, w0 *be a rooted Kripke structure. Let* W , R *be the unravelling of* W, R *at* w0*. Let* M = W , R, V Σ,(w0) *be a Kripke structure such that*

**–** V Σ(p) = { w ∈ W | trm( w) ∈ V (p)} *for every propositional symbol* p ∈ Q*, and* **–** V Σ(tψ) = { w ∈ W | M, w |= ψ} *for every surrogate* tψ ∈ T ∩ var(Φ)*. Then* M |= Φ*.*

**Lemma 2.** *Let* ϕ *be a* L*-satisfiable modal formula in simplified NNF where* L *is a normal modal logic and let* Φ = {{0} : tϕ} ∪ ρK ({0} : tϕ → ϕ)*. Let* M = W, R, V, w0 *be a rooted* K *model of* ϕ*. Let* W , R *be the unravelling of* W, R *at* w0*. Let* M = W , R, V , (w0) *be a Kripke structure such that*

**Lemma 3.** *Let* M = W, R, V, w0 *be a rooted Kripke structure. Let* W , R *be the unravelling of* W, R *at* w0*. Let* M = W , R, V Σ,(w0) *where* V Σ(p) = { w ∈ W | trm( w) ∈ V (p)} *for every propositional symbol* p ∈ Q*.*

*Then for every modal formula* ψ *over* Q *and for every world* w ∈ W *,* M, w |= ψ *iff* M,trm( w) |= ψ*.*

**Lemma 4.** *Let* ϕ *be a modal formula in simplified NNF. Let* ΦK = {{0} : tϕ}∪ρK ({0} : tϕ → ϕ)*. Let* Φ *with* ΦK ⊆ Φ *be a definition-complete set of* SNFsml *clauses, let* M = W, R, V, w0 *be a tree* K *model of* Φ *and let* M = W, R ,V,w0 *be such that*

*Then* M |= Φ*.*

*(4a)* R ⊆ R *;*

*Then* M , w0 |= ϕ*.*

Theorems 3 and 4 now state the correctness of our transformation for KB.

**Theorem 3.** *Let* ϕ *be a modal formula in simplified NNF. Let* ΦB = {{0} : tϕ} ∪ ρKB ({0} : tϕ → ϕ)*. If* ϕ *is* KB*-satisfiable, then* ΦB *is* K*-satisfiable.*

*Proof.* The main idea is to show that given a rooted KB model of ϕ, then a small variation of its unravelling is a rooted tree K model of ΦB.

Let M = W, R, V, w0 be a rooted KB model of ϕ with M,w0 |= ϕ and symmetric relationship R. Let W , R be the unravelling of W, R at w0. Let M B = W , R, VB ,(w0) where

Note that VB is well-defined as for every surrogate tψ ∈ T, ψ only contains propositional symbols in Q. Let ΦK = {{0} : tϕ} ∪ ρK ({0} : tϕ → ϕ).

We now consider the clauses occurring in ΦB and show that they hold in M B . By Lemma 2 it follows that M B |= ΦK . Also, all definitional clauses in ΦB \ ΦK are true in M B by Lemma 1.

Next consider clauses of the form

$$(1)\ S': \eta(\psi) \lor t\_{\Box \neg t\_{\Box \psi}} \qquad\qquad\text{(2)}\ S': t\_{\Box \neg t\_{\Box \psi}} \to \Box \neg t\_{\Box \psi}.$$

where t✷ψ is a surrogate for ✷ψ. These are not in ΦK . We show both are true in M B . We do so by first considering that t✷¬t✷ψ is true at a world and then that it is false.

Case (a): Let w ∈ M B [S ] with M B , w |= t✷¬t✷ψ . Clearly, M B , w |= η(ψ) ∨ t✷¬t✷ψ . Also, by definition of M B , MB , w |= ✷¬✷ψ. So, for every v ∈ W with w R v, M B , v |= ¬✷ψ. As t✷ψ is a surrogate for ✷ψ, by definition of V B, v ∈ V B(t✷ψ) and M B , v |= ¬t✷ψ. Thus, M B , w |= ✷¬t✷ψ and, by the semantics of implication, M B , w |= t✷¬t✷ψ → ✷¬t✷ψ.

Case (b): Let w ∈ M B [S ] with M B , w |= t✷¬t✷ψ . Clearly, by the semantics of implication, M B , w |= t✷¬t✷ψ → ✷¬t✷ψ. Also, by definition of V B, w ∈ V B(t✷¬t✷ψ ) implies M B , w |= ✷¬✷ψ which in turn implies M B , w |= ✸✷ψ. So, there exists v ∈ W with wR v and M B , v |= ✷ψ. Since trm is a p-morphism from M B to M, trm( w) R trm(v).  Since M B , v |= ✷ψ, M B , u |= ψ. As trm is a p-morphism and M,trm(u) |= ψ and since trm( w) = trm(u), M,trm( w) |= ψ. By Lemma 3, from M,trm( w) |= ψ we obtain M B , w |= ψ. If ψ is a literal, then η(ψ) = ψ and M, w |= η(ψ). If ψ is not a literal, then η(ψ) = tψ and from M B , w |= ψ, by definition of VB , w ∈ VB (tψ) and M B , w |= tψ. So, M, w |= η(ψ) ∨ t✷¬t✷ψ .

Thus, in both cases, for arbitrary w ∈ M B [S ], η(ψ)∨t✷¬t✷ψ and t✷¬t✷ψ → ✷¬t✷ψ and therefore Clauses (1) and (2) are true in M B .

**Theorem 4.** *Let* ϕ *be a modal formula in simplified NNF. Let* ΦB = {{0} : tϕ} ∪ ρKB ({0} : tϕ → ϕ)*. If* ΦB *is* K*-satisfiable, then* ϕ *is* KB*-satisfiable.*

*Proof.* The main idea is to show that given a rooted tree K model of ΦB , its symmetric closure is a rooted KB model of ϕ.

Let M = W, R, V, w0 be a rooted tree K model of ΦB . Let MB = W, RB , V B , w0 be a structure such that

Let ΦK = {{0} : tϕ} ∪ ρK ({0} : tϕ → ϕ). We show that MB |= ΦB satisfies the three preconditions of Lemma 4. By Lemma 4 this in turn implies that MB |= ϕ.

Case (a): Assume wRv. As M,w |= t✷ψ and M,w |= t✷ψ → ✷η(ψ), we have M,w |= ✷η(ψ). As wRv, M,v |= η(ψ). As η(ψ) is a literal and V B = V we obtain MB , v |= η(ψ). So, MB , w |= t✷ψ → ✷η(ψ).

Case (b): Assume v is not reachable from w via R. Then wRB v was introduced by the symmetric closure operation on R and we must have vRw. That is, v is a R-predecessor of w and from w ∈ M[S] it follows that v ∈ M[S−]. So, (7) M,v |= η(ψ) ∨ t✷¬t✷ψ and (8) M,v |= t✷¬t✷ψ → ✷¬t✷ψ. From vRw, M,w |= t✷ψ and (8), it follows that M,v |= ¬t✷¬t✷ψ . This together with (7) implies M,v |= η(ψ). As η(ψ) is a literal and V B = V we obtain MB , v |= η(ψ). So, MB , w |= t✷ψ → ✷η(tψ).

Case (a) and Case (b) together show that Property (6) holds.

**–** For Condition (4c) let (9) S : t✷ψ → ✷tψ be in ΦB , v, w ∈ W, mlM(w) = ml ∈ S (i.e., w ∈ M[S]) and w RB v. We need to show that there exists a clause S : ¬tψ ∨ ηf (ψ) in ΦB with v ∈ M[S ].

As in the previous case w RB v implies either wRv or vRw. In the first case mlM(v) = ml + 1 while in the second case mlM(v) = ml − 1.

As ΦB contains Clause (9), tψ occurs at level ml+1 in ΦB . By definition of ρKB , ΦB also contains the clause (10) S− : tψ ∨t✷¬t✷ψ . As ml ∈ S, ml−1 ∈ S− and therefore tψ also occurs at level ml −1 in ΦB . By Theorem 2, ΦB is definitioncomplete, so there must be a clause S : ¬tψ ∨ ηf (ψ) in ΦB such that ml + 1 and ml − 1 in S .

**Theorem 5.** *Let* ϕ *be a modal formula in simplified NNF,* L ∈ {K,KB,KD,KT, K4,K5}*, and* ΦL = {{0} : tϕ} ∪ ρL({0} : tϕ → ϕ)*. Then* ϕ *is* L*-satisfiable iff* ΦL *is* K*-satisfiable.*

## **5 Comparison With Related Work**

The approaches most closely related to ours are Kracht's reductions of normal modal logics to basic modal logic [11,12], the global modal resolution calculus [14], and Schmidt and Hustadt's axiomatic translation principle for translations of normal modal logics to first-order logic [24].

The first significant difference to our approach is that Kracht's reductions and the axiomatic translation exclude the modal operator ✸ from the language and only consider the modal operator ✷.

In order to present Kracht's approach, we need some additional notions. Let sf(ϕ), dg(ϕ), and |S| denote the set of all subformulae of ϕ, the maximum nesting of modal operators in ϕ, and the cardinality of the set S, respectively. Let ✸0ψ = ✷0ψ = ✷<1ψ = ψ, ✷<n+1ψ = (ψ ∧ ✷✷<nψ), ✷n+1ψ = ✷✷nψ, and ✸n+1ψ = ✸✸nψ. We can then define a reduction function ρK L for a normal modal logic L in {KB,KD,KT,K4} as follows:

$$\rho\_L^{\mathbb{K}}(\varphi) = \begin{cases} \varphi \wedge \Box^{<|\mathfrak{sl}(\varphi)|+1} P\_{\mathbb{K}\mathfrak{l}}^{\mathbb{K}}(\varphi), & \text{for } L = \mathbb{K}4 \\ \varphi \wedge \Box^{<\deg(\varphi)+1} P\_L^{\mathbb{K}}(\varphi) & \text{otherwise} \end{cases}$$

where P K KB (ϕ)= {¬ψ → ✷¬✷ψ | ✷ψ ∈ sf(ϕ)} P K KD(ϕ)= {¬✷**false**} P K K4 (ϕ)= {✷ψ → ✷✷ψ | ✷ψ ∈ sf(ϕ)} P K

KT (ϕ)= {✷ψ → ψ | ✷ψ ∈ sf(ϕ)} Kracht shows that ϕ is L-satisfiable iff ρK L(ϕ) is K-satisfiable. There are three differences to our approach. First, P K L (ϕ) will include an axiom instance for every occurrence of a subformula ¬✷ψ, equivalent to ✸¬ψ, in ϕ. In contrast, our approach requires no logic specific treatment of such subformulae. Second, the use of ✷<nP K L (ϕ) in ρK L means that the axiom instance is available at every modal level. This means, for example, that for ϑ1 = ✸100(¬p ∧ ✷p), the formula ρK KT (ϑ1) contains the axiom instance ✷p → p over 100 times, although it is only required at the level at which ✷p occurs. Third, this is further compounded if the formula ψ in ✷ψ is itself a complex formula. We try to avoid that by using a surrogate propositional symbol tψ instead, but this will only have a positive effect if the definitional clauses for tψ do not have to be repeated.

The global modal resolution (GMR) calculus operates on SNFK clauses, that is, clauses of the form

$$
\Box^\*(\mathbf{start} \to \bigvee\_{b=1}^r l\_b) \quad \Box^\*(\mathbf{true} \to \bigvee\_{b=1}^r l\_b) \quad \Box^\*(l' \to \bigcirc l) \quad \Box^\*(l' \to \neg\bigcirc l)
$$

**Table 4.** Inference rules in [14] for K5 (EUC1 and EUC2).

where l, l , lb are propositional literals with 1 ≤ b ≤ r, r ∈ N, and ✷∗ is the universal operator. The calculus has specific inference rules for normal modal logics such as KB, KD, KT, K4, K5. Table 4 shows the two additional rules for K5, the only logic for which there are rules for both ✷ and ¬✷¬, i.e., ✸. These inference rules can be seen to perform an 'on-the-fly' computation of a transformation. Note that the clauses produced by PK5 differ from those produced by GMR for K5. Implicitly, our results here also show that it should be possible to eliminate EUC1 from the GMR calculus.

For the axiomatic translation, we only present the function P RS L that computes the logic dependent first-order clausal formulae that are part of the overall translation.

$$\begin{split} P^{\mathsf{RS}}\_{\mathsf{K}\mathsf{S}}(\Box\psi) &= \{ \forall x(\neg Q\_{\Box\psi}(y) \lor \neg R(x,y) \lor Q\_{\psi}(x)) \mid \Box\psi \in \mathsf{sf}(\varphi) \} \\ P^{\mathsf{RS}}\_{\mathsf{K}\mathsf{D}}(\Box\psi) &= \{ \forall x(\neg Q\_{\Box\psi}(x) \lor Q\_{\neg\Box\neg\psi}(x)) \mid \Box\psi \in \mathsf{sf}(\varphi) \} \\ P^{\mathsf{RS}}\_{\mathsf{K}\mathsf{T}}(\Box\psi) &= \{ \forall x(\neg Q\_{\Box\psi}(x) \lor Q\_{\psi}(x)) \mid \Box\psi \in \mathsf{sf}(\varphi) \} \\ P^{\mathsf{RS}}\_{\mathsf{K}\mathsf{I}}(\Box\psi) &= \{ \forall xy(\neg Q\_{\Box\psi}(x) \lor \neg R(x,y) \lor Q\_{\Box\psi}(y)) \mid \Box\psi \in \mathsf{sf}(\varphi) \} \\ P^{\mathsf{RS}}\_{\mathsf{K}\mathsf{S}}(\Box\psi) &= \{ \forall xy(\neg Q\_{\Box\psi}(y) \lor \neg R(x,y) \lor Q\_{\Box\psi}(x)), \\ &\qquad \forall xy(\neg Q\_{\Box\neg\Box\psi}(y) \lor \neg R(x,y) \lor Q\_{\Box\neg\Box\psi}(x)) \mid \Box\psi \in \mathsf{sf}(\varphi) \} \end{split}$$

The predicate symbols Qψ correspond to our surrogate symbols tψ. The clausal formulae used in the treatment of KT and K4 are translations of the SNFml clauses we use (or vice versa). KB and K5 are handled in a different way as the first-order clausal formulae refer directly the accessibility relation and can therefore more easily express the transfer of information to a predecessor world. The universal quantification over worlds also means that the constraints expressed by the formulae hold at all modal levels without the need of any repetition.

In Section 6 we will also use the relational and semi-functional translation of modal logics to first-order logic combined with structural transformation to clause normal form. In both approaches ✷ψ is translated as ∀xy(¬Q✷ψ(x) ∨ ¬R(x, y)∨Qψ, while ✸ψ becomes ∀x∃y(¬Q✸ψ(x)∨R(x, y)) and ∀x∃α(¬Q✸ψ(x)∨ R(x, [xα])) in the relational and semi-functional translation, respectively. Then, depending on the modal logics, further formulae representing the semantic properties of the accessibility R are added. For the relational translation these will simply be the formulae in the fourth column of Table 1. The semi-functional translation uses collections of partial accessibility function in addition to the accessibility relation. A predicate def is used to represent on which worlds a partial

accessibility function is defined. For each modal logic there is then again a background theory consisting of formulae over def and R that represents the properties of the underlying accessibility relation which is added to the translation of a formula. For example, for K5 the background theory is: ∀xy∀αβ((¬def(x) ∨ def(y))∧(¬def(w0)∨R(w0, [w0α]))∧(¬def(x)∨ ¬def(y)∨R([xα], [yβ]))), where w0 is a constant representing the root world in a rooted Kripke structure.

## **6 Evaluation**

We have compared the performance of the following approaches: (i) the combination of our reductions with the modal-layered resolution (MLR) calculus for SNFml clauses [15] implemented in the modal theorem prover KSP, with three different refinements for resolution inferences on labelled propositional clauses; (ii) the global modal resolution (GMR) calculus, also implemented in KSP, with three different refinements for resolution inferences on propositional clauses; (iii) the combinations of the relational and semi-functional translation of modal logics to first-order logic with ordered first-order resolution implemented in the first-order theorem prover SPASS. In total this gives us eight different approaches to compare. The axiomatic translation is currently not implemented in SPASS. Other provers, such as LEO-III [26], LWB [9], MleanCoP [21], do not have built-in support for the full range of logics considered here. LoTREC 2.0 [7] supports all the logics, but is not intended as automatic theorem prover.

The modal-layered resolution calculus operates on SNFml clauses, that is, clauses of the form

$$ml: \bigvee\_{b=1}^r l\_b \qquad ml: l' \to \Box l \qquad ml: l' \to \Diamond l$$

where ml ∈ N ∪ {} and l, l , lb are propositional literals with 1 ≤ b ≤ r, r ∈ N. In the implementation of the reductions presented in Section 3, we take a SNFsml clause S : ψ simply as an abbreviation of the set of SNFml clauses {ml : ψ | ml ∈ S}. Note that this also means that we will have to repeat similar resolution inferences for different modal levels.

KSP [13] implements the reductions presented in Section 3 as well as a normal form transformation of modal formulae to sets of SNFK clauses. It implements both the MLR and the GMR calculus. Resolution inferences between (labelled) propositional clauses can either be unrestricted (cplain option), restricted by an ordering (cord option), that is, clauses can only be resolved on their maximal literals with respect to an ordering chosen by the prover in such a way to preserve completeness, restricted to negative resolution (cneg option), that is, one of the premises in an inference has to be a negative clause, or restricted to positive resolution. We do not include the last option in our evaluation as it typically performs worse. KSP also implements a range of simplification rules that are applied to modal formulae before their transformation to normal form. Of those we have enabled pure literal elimination (early ple option), simplification using the Box Normal Form [22] and Prenex Normal Form (bnfsimp and prenex

**Table 5.** Experimental results on LWB benchmark collection

options) [17]. For clause processing, unit resolution and pure elimination are enabled (unit, lhs unit, and ple options).

SPASS 3.9 [27,28] supports automated reasoning in extended modal logics, including all logics considered here, PDL-like modal logics as well as description logics. It includes eight different translations of modal logics to first-order logic. In our evaluation we have used the relational translation and the semifunctional translation. For the local satisfiability problem in KB to K5, for the relational translation we have added the first-order frame properties given in Table 1 while for the semi-functional translation we have added the background theories devised by Nonnengart [20]. For the transformation to first-order clausal form, we have enabled renaming of quantified subformulae. The only inference rules used are ordered resolution and ordered factoring, the reduction rules used are condensing, backward subsumption and forward subsumption. For the relational and semi-functional translation for K, KB, KD, and KT we thereby obtain a decision procedure, while for the other logics we do not. For K4 and K5, the fragment of first-order clausal logic corresponding to the semi-functional translation of modal formula and their background theories is decidable by ordered resolution with selection [25]. However, the non-trivial ordering and selection function required is not currently implemented in SPASS.

For our evaluation we have chosen the LWB basic modal logic benchmark collection [2], with 20 formulae in each of 18 parameterised classes. For K, all formulae in 9 classes are satisfiable while all formulae in the other 9 classes are unsatisfiable. In their negation normal form, 63% of modal operators are ✷ and 37% are ✸ operators. We have used the collection for each of the six logics. If a formula is unsatisfiable in K then it remains unsatisfiable in the other five logics, while the opposite is not true. As we move to logics other than K, it is also no longer the case that all formulae in a class have the same satisfiability status.

The third column in Table 5 indicates the total number of satisfiable and unsatisfiable formulae for each logic. In the last two lines of the table we sum up the results for all logics. The last eight columns in the table show how many formulae each of the approaches were able to solve with a time limit of 100 CPU seconds for each formula. Benchmarking was performed on a PC with an AMD Ryzen 5 5600X CPU @ 4.60GHz max and 32GB main memory using Fedora release 33 as operating system.

As we can see, the new reductions combined with the modal-layered resolution (MLR) calculus and ordered resolution refinement (cord) perform best, achieving the highest number of solved formulae in 8 out of 12 individual categories in the table, on two of those equal with the global modal resolution (GMR) calculus. On 3 categories, GMR outperfoms MLR. On both satisfiable and unsatisfiable formulae in K5 this can be seen as evidence that 'on-the-fly' transformation offers a (slight) advantage over our approach given that the additional clauses hold universally in both approaches. For SPASS we see a clear advantage of the semi-functional translation over the relational one, on both satisfiable and unsatisfiable formulae.

# **7 Conclusion and Future Work**

We have presented new reductions of propositional modal logics KB, KD, KT, K4, K5 to Separated Normal Form with Sets of Modal Levels. We have shown experimentally that these reductions allow us to reason effectively in these logics.

The obvious next step is to consider extensions of the basic modal logic K with combinations of the axioms B, D, T, 4, and 5. Unfortunately, a simple combination of the reductions for each of the axioms is not sufficient to obtain a satisfiability-preserving reduction for the such modal logics. An example is the simple formula ¬p ∧ ✸✸✷p which is KB4-unsatisfiable. If we define

$$\begin{aligned} P\_{\mathsf{KB4}}(S:t\_{\Box\psi}\to\Box\psi) &= P\_{\mathsf{KB}}(S:t\_{\Box\psi}\to\Box\psi)\cup P\_{\mathsf{KA}}(S:t\_{\Box\psi}\to\Box\psi),\\ \Delta\_{\mathsf{KB4}}(S:t\_{\Box\psi}\to\Box\psi) &= \delta\_{\mathsf{KB4}}(\star,\psi),\end{aligned}$$

that is, PKB4 is the union of PKB and PK4 , then the clause set obtained from {{0} : t0} ∪ ρKB4 ({0} : t0 → ¬p ∧ ✸✸✷p) is K-satisfiable. The same issue also occurs in the axiomatic translation of modal logics to first-order logic where the translation for KB4 is not simply the combination of the translations for KB and K4 [24, Theorem 5.6]. We are currently exploring solutions to this problem.

Regarding practical applications, it would be advantageous to have an implementation of a calculus that operates directly SNFsml clauses. This would greatly reduce the number of inference steps performed on satisfiable formulae and simplify proof search in general. Again, such an implementation is future work.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

#### **Isabelle's Metalogic: Formalization and Proof Checker***-*

Tobias Nipkow and Simon Roßkopf

Technical University of Munich, Munich, Germany

**Abstract.** Isabelle is a generic theorem prover with a fragment of higherorder logic as a metalogic for defining object logics. Isabelle also provides proof terms. We formalize this metalogic and the language of proof terms in Isabelle/HOL, define an executable (but inefficient) proof term checker and prove its correctness w.r.t. the metalogic. We integrate the proof checker with Isabelle and run it on a range of logics and theories to check the correctness of all the proofs in those theories.

#### **1 Introduction**

One of the selling points of proof assistants is their trustworthiness. Yet in practice soundness problems do come up in most proof assistants. Harrison [11] distinguishes errors in the logic and errors in the implementation (and cites examples). Our work contributes to the solution of both problems for the proof assistant Isabelle [31]. Isabelle is a generic theorem prover: it implements M, a fragment of intuitionistic higher-order logic, as a metalogic for defining object logics. Its most developed object logic is HOL and the resulting proof assistant is called Isabelle/HOL [25,24]. The latter is the basis for our formalizations.

Our first contribution is the first complete formalization of Isabelle's metalogic. Thus our work applies to all Isabelle object logics, e.g. not just HOL but also ZF. Of course Paulson [30] describes M precisely, but only on paper. More importantly, his description does not cover polymorphism and type classes, which were introduced later [26]. The published account of Isabelle's proof terms [4] is also silent about type classes. Yet type classes are a significant complication (as, for example, Kunˇcar and Popescu [18] found out).

Our second contribution is a verified (against M) and executable checker for Isabelle's proof terms. We have integrated the proof checker with Isabelle. Thus we can guarantee that every theorem whose proof our proof checker accepts is provable in our definition of M. So far we are able to check the correctness of moderatly sized theories across the full range of logics implemented in Isabelle.

Although Isabelle follows the LCF-architecture (theorems that can only be manufactured by inference rules) it is based on an infrastructure optimized for

- Supported by Wirtschaftsministerium Bayern under DIK-2002-0027//DIK0185/03 and DFG GRK 2428 ConVeY

c The Author(s) 2021

A. Platzer and G. Sutcliffe (Eds.): CADE 2021, LNAI 12699, pp. https://doi.org/10.1007/978-3-030-79876-5\_6 93–110, 2021.

performance. In particular, this includes multithreading, which is used in the kernel and has once lead to a soundness issue1 . Therefore we opt for the "certificate checking" approach (via proof terms) instead of verifying the implementation.

This is the first work that deals directly with what is implemented in Isabelle as opposed to a study of the metalogic that Isabelle is meant to implement. Instead of reading the implementation you can now read and build on the more abstract formalization in this paper. The correspondence of the two can be established for each proof by running the proof checker.

Our formalization reflects the ML implementation of Isabelle's terms and types and some other data structures. Thus a few implementation choices are visible, e.g. De Bruijn indices. This is necessary because we want to integrate our proof checker as directly as possible with Isabelle, with as little unverified glue code as possible, for example no translation between De Bruijn indices and named variables. We refer to this as our *intentional implementation bias*. In principle, however, one could extend our formalization with different representations (e.g. named terms) and prove suitable isomorphisms. Our work is purely proof theoretic; semantics is out of scope.

The formalization can be found in the Archive of Formal Proofs[28].

#### **2 Related Work**

Harrison [11] was the first to verify some of HOL's metatheory and an implementation of a HOL kernel in HOL itself. Kumar *et al.* [13] formalized HOL including definition principles, proved its soundness and synthesized a verified kernel of a HOL prover down to the machine language level. Abrahamsson [2] verified a proof checker for the OpenTheory [12] proof exchange format for HOL.

Wenzel [38] showed how to interpret type classes as predicates on types. We follow his approach of reflecting type classes in the logic but cannot remove them completely because of our intentional implementation bias (see above). Kunˇcar and Popescu [15,16,17,18] focus on the subtleties of definition principles for HOL with overloading and prove that under certain conditions, type and constant definitions preserve consistency. ˚Aman Pohjola *et al.* [1] formalize [15,18].

Adams [3] presents HOL Zero, a basic theorem prover for HOL that addresses the problem of how to ensure that parser and pretty-printer do not misrepresent formulas.

Let us now move away from Isabelle and HOL. Sozeau *et al.* [36] present the first implementation of a type checker for the kernel of Coq that is proved correct in Coq with respect to a formal specification. Carneiro [6] has implemented a highly performant proof checker for a multi-sorted first order logic and is in the process of verifying it in its own logic.

We formalize a logic with bound variables, and there is a large body of related work that deals with this issue (e.g. [37,21,7]) and a range of logics and systems with special support for handling bound variables (e.g. [33,34,35]). We found that De Bruijn indices worked reasonably well for us.

1 https://mailmanbroy.in.tum.de/pipermail/isabelle-dev/2016-December/007251.html

## **3 Preliminaries**

Isabelle types are built from type variables, e.g. *a*, and (postfix) type constructors, e.g. *a list*; the function type arrow is ⇒. Isabelle also has a type class system explained later. The notation t :: τ means that term t has type τ . Isabelle/HOL provides types *a set* and *a list* of sets and lists of elements of type *a*. They come with the following vocabulary: function set (conversion from lists to sets), (#) (list constructor), (@) (append), |*xs*| (length of list *xs*), *xs* ! *i* (the *i*th element of *xs* starting at 0), list-all2 *p* [*x* 1, . . ., *x* m] [*y*1, . . ., *y*n]=(*m* = *n* ∧ *p x* 1 *y*1 ∧ ... ∧ *p x* n *y*n) and other self-explanatory notation.

The Field of a relation *r* is the set of all *x* such that (*x* , ) or ( ,*x* ) is in *r*.

There is also the predefined data type

**datatype** - *a option* = None | Some - *a*

The type τ 1 τ 2 abbreviates τ 1 ⇒ τ 2 *option*, i.e. partial functions, which we call *maps*. Maps have a domain and a range:

dom *m* = {*a* | *m a* = None} ran *m* = {*b* | ∃ *a*. *m a* = Some *b*}.

Logical equivalence is written = instead of ←→.

## **4 Types and Terms**

A *name* is simply a string. Variables have type *var* ; their inner structure is immaterial for the presentation of the logic.

The logic has three layers: terms are classified by types as usual, but in addition types are classified by *sorts*. A *sort* is simply a set of class names. We discuss sorts in detail later.

Types (typically denoted by *T*, *U*, . . . ) are defined like this:

**datatype** *typ* = Ty *name* (*typ list*) | Tv *var sort*

where Ty κ [*T*1,...,*T*n] represents the Isabelle type (*T*1,. . .,*T*n) κ and Tv *a S* represents a type variable *a* of sort *S* — sorts are directly attached to type variables. The notation *T* → *U* is short for Ty *"fun"* [*T*,*U* ], where *"fun"* is the name of the function type constructor.

Isabelle's terms are simply typed lambda terms in De Bruijn notation:

**datatype** *term* = Ct *name typ* | Fv *var typ* | Bv *nat* | Abs *typ term* | (*·*) *term term*

A term (typically *r*, *s*, *t*, *u* . . . ) can be a typed constant Ct *c T* or free variable Fv *v T*, a bound variable Bv *n* (a De Brujin index), a typed abstraction Abs *T t* or an application *t · u*.

The term-has-type proposition has the syntax *Ts* τ *t* : *T* where *Ts* is a list of types, the context for the type of the bound variables.

τ Ct *T* : *T* τ Fv *T* : *T i* < |*Ts*| *Ts* τ Bv *i* : *Ts* ! *i*

$$\begin{array}{c} T \ \# \ T s \vdash\_{\tau} t : T' \\ \hline Ts \vdash\_{\tau} \mathsf{Abs} \ T \ t : T \to T' \\ \hline Ts \vdash\_{\tau} u : U \qquad Ts \vdash\_{\tau} t : U \to T \\ \hline Ts \vdash\_{\tau} t \cdot u : T \end{array}$$

We define τ *t* : *T* = [] τ *t* : *T*.

Function fv :: *term* ⇒ (*var* × *typ*) *set* collects the free variables in a term. Because bound variables are indices, fv *t* is simply the set of all (*v*, *T*) such that Fv *v T* occurs in *t*. The type is an integral part of a variable.

A *type substitution* is a function of type *var* ⇒ *sort* ⇒ *typ*. It assigns a type to each type variable and sort pair. We write \$\$ *T* or \$\$ *t* for the overloaded function which applies such a type substitution to all type variables (and their sort) occurring in a type or term. The *type instance* relation is defined like this:

*T*1 - *T*2 = (∃ -. -\$\$ *T*2 = *T*1)

We also need to β-contract a term Abs *T t · u* to something like "*t* with Bv *0* replaced by *u*". We define a function subst-bv such that subst-bv *u t* is that β-contractum. The definition of subst-bv is shown in the Appendix and can also be found in the literature (e.g. [23]).

In order to abstract over a free (term) variable there is a function bind-fv (*v*, *T*) *t* that (roughly speaking) replaces all occurrences of Fv *v T* in *t* by Bv *0*. Again, see the Appendix for the definition. This produces (if Fv *v T* occurs in *t*) a term with an unbound Bv *0*. Function Abs-fv binds it with an abstraction:

Abs-fv *vTt=* Abs *T* (bind-fv (*v*, *T*) *t*)

While this section described the syntax of types and terms, they are not necessarily wellformed and should be considered pretypes/preterms. The wellformedness checks are described later.

#### **5 Classes and Sorts**

Isabelle has a built-in system of type classes [22] as in Haskell 98 except that class constraints are directly attached to variable names: our *Tv a* [*C* ,*D*,. . .] corresponds to Haskell's (C a, D a, ...) => ... a ....

A *sort* is Isabelle's terminology for a set of (class) names, e.g. {*C* ,*D*,. . .}, which represent a conjunction of class constraints. In our work, variables *S*, *S* etc. stand for sorts.

Apart from the usual application in object logics, type classes also serve an important metalogical purpose: they allow us to restrict, for example, quantification in object logics to object-level types and rule out meta-level propositions.

Isabelle's type class system was first presented in a programming language context [29,27]. We give the first machine-checked formalization. The central data structure is a so-called *order-sorted signature*. Intuitively, it is comprised of a set of class names, a partial subclass ordering on them and a set of *type constructor signatures*. A type constructor signature κ :: (*S* 1, . . ., *S* k) *c* for a type constructor κ states that applying κ to types *T*1, . . ., *T*k such that *T*i has sort *S*i (defined below) produces a type of class *c*. Formally:

# **type synonym** *osig* = ((*name* × *name*) *set* × (*name* (*class sort list*)))

To explain this formalization we start from a pair (*sub*,*tcs*) :: *osig* and recover the informal order-sorted signature described above. The set of classes is simply the Field of the *sub* relation. The *tcs* component represents the set of all type constructor signatures κ :: (*Ss*) *c* (where *Ss* is a list of sorts) such that *tcs* κ = Some *dm* and *dm c* = Some *Ss*. Representing κ :: (*Ss*) *c* as a triple, we define

$$TCS = \{ (\kappa, Ss, c) \mid \exists \, domf. \; tcs \; \kappa = \mathsf{Some} \; domf \land \; domf \; c = \mathsf{Some} \; Ss \} $$

*TCS* is the translation of *tcs*, the data structure close to the implementation, to an equivalent but more intuitive version *TCS* that is close to the informal presentations in the literature.

The subclass ordering *sub* can be extended to a subsort ordering as follows:

$$S\_1 \le\_{sub} S\_2 = \left( \forall \ c\_2 \in S\_2. \ \exists \ c\_1 \in S\_1. \ c\_1 \le\_{sub} c\_2 \right)$$

The smaller sort needs to subsume all the classes in the larger sort. In particular {*c*1} ≤*sub* {*c*2} iff (*c*1, *c*2) ∈ *sub*.

Now we can define a predicate has-sort that checks whether, in the context of some order-sorted signature (*sub*,*tcs*), a type fulfills a given sort constraint:

*S* ≤*sub S* has-sort (*sub*, *tcs*) (Tv *a S*) *S tcs* κ = Some *dm* ∀ *c*∈*S*. ∃ *Ss*. *dm c* = Some *Ss* ∧ list-all2 (has-sort (*sub*, *tcs*)) *Ts Ss* has-sort (*sub*, *tcs*) (Ty κ *Ts*) *S*

The rule for type variables uses the subsort relation and is obvious. A type (*T*1, . . ., *T*n) κ has sort {*c*1, ...} if for every *c*i there is a signature κ :: (*S* 1, . . ., *S* n) *c*i and has-sort (*sub*, *tcs*) *T*j *S*j for *j* = *1* , . . ., *n*.

We *normalize* a sort by removing "superfluous" class constraints, i.e. retaining only those classes that are not subsumed by other classes. This gives us unique representatives for sorts which we call *normalized*:

normalize-sort *sub S* = {*c* ∈ *S* | ¬ (∃ *c* ∈*S*. (*c* , *c*) ∈ *sub* ∧ (*c*, *c* ) ∈/ *sub*)} normalized-sort *sub S* = (normalize-sort *sub S* = *S*)

We work with normalized sorts because it simplifies the derivation of efficient executable code later on.

Now we can define wellformedness of an *osig*:

wf-osig (*sub*, *tcs*)=(wf-subclass *sub* ∧ wf-tcsigs *sub tcs*)

A sublass relation is wellformed if it is a partial order where reflexivity is restricted to its Field. Wellformedness of type constructor signatures (wf-tcsigs) is more complex. We describe it in terms of *TCS* derived from *tcs* (see above). The conditions are the following:

	- ∀ (κ, *Ss*1, *c*1)∈*TCS*. ∀ *c*2. (*c*1, *c*2) ∈ *sub* −→

These conditions are used in a number of places to show that the type system is well behaved. For example, has-sort is upward closed:

wf-osig (*sub*, *tcs*) ∧ has-sort (*sub*, *tcs*) *T S* ∧ *S* ≤*sub S* −→ has-sort (*sub*, *tcs*) *T S*

# **6 Signatures**

A *signature* consist of a map from constant names to their (most general) types, a map from type constructor names to their arities, and an order-sorted signature:

**type synonym** *signature* = (*name typ*) × (*name nat*) × *osig*

The three projection functions are called const-type, type-arity and osig. We now define a number of wellformedness checks w.r.t. a signature Σ.  Combining wellformedness and τ yields welltypedness of a term:

wt-term Σ *t* = (wf-term Σ *t* ∧ (∃ *T*. τ *t* : *T*))

Wellformedness of a signature Σ = (*ctf* , *arf* , *oss*) where *oss* = (*sub*, *tcs*) is defined as follows:

```
wf-sig Σ =
((∀ T∈ran ctf . wf-type Σ T) ∧ wf-osig oss ∧ dom tcs = dom arf ∧
(∀ κ dm. tcs κ = Some dm −→ (∀ Ss∈ran dm. arf κ = Some |Ss|)))
```
In words: all types in *ctf* are wellformed, *oss* is wellformed, the type constructors in *tcs* are exactly those that have an arity in *arf*, for every type constructor signature (κ, *Ss*, ) in *tcs*, κ has arity |*Ss*|.

# **7 Logic**

Isabelle's metalogic M is an extension of the logic described by Paulson [30]. It is a fragment of intuitionistic higher-order logic. The basic types and connectives of M are the following:

The type subscripts of and ≡ are dropped in the text if they can be inferred.

Readers familiar with Isabelle syntax must keep in mind that for readability we use the symbols -, =⇒ and ≡ for the *encodings* of the respective symbols in Isabelle's metalogic. We avoid the corresponding metalogical constants completely in favour of HOL's ∀ , −→, = and inference rule notation.

The provability judgment of M is of the form Θ,Γ *t* where Θ is a theory, Γ (the hypotheses) is a set of terms of type prop and *t* a term of type prop.

A *theory* is a pair of a signature and a set of axioms:

**type synonym** *theory* = *signature* × *term set*

The projection functions are sig and axioms. We extend the notion of wellformedness from signatures to theories:

wf-theory (Σ, *axs*) = (wf-sig Σ ∧ (∀ *p*∈*axs*. wt-term Σ *p* ∧ τ *p* : prop) ∧ is-std-sig Σ ∧ eq-axs ⊆ *axs*)

The first two conjuncts need no explanation. Predicate is-std-sig (not shown) requires the signature to have certain minimal content: the basic types (→, prop) and constants (≡, -, =⇒) of M and the additional types and constants for type class reasoning from Section 7.3. Our theories also need to contain a minimal set of axioms. The set eq-axs is an axiomatic basis for equality reasoning and will be explained in Section 7.2.

We will now discuss the inference system in three steps: the basic inference rules, equality and type class reasoning.

#### **7.1 Basic Inference Rules**

The *axiom rule* states that wellformed type-instances of axioms are provable:

wf-theory Θ *t* ∈ axioms Θ wf-inst Θ Θ,Γ \$\$ *t*

where :: *var* ⇒ *sort* ⇒ *typ* is a type substitution and \$\$ denotes its application (see Section 4).  This condition is not superfluous because otherwise has-sort *oss* (Tv *v S*) *S* and wf-type Σ (Tv *v S*) only hold if *S* is wellformed w.r.t Σ.

Note that there are no extra rules for general instantiation of type or term variables. Type variables can only be instantiated in the axioms. Term instantiation can be performed using the forall introduction and elimination rules.

The *assumption rule* allows us to prove terms already in the hypotheses:

$$\frac{\text{wf-term } (\text{sig } \Theta) \ t \qquad \vdash\_{\tau} t : \text{prop} \qquad t \in \varGamma}{\Theta, \varGamma \vdash t}$$

Both and =⇒ are characterized by introduction and elimination rules:

wf-theory Θ Θ,Γ *t* (*x* , *T*) ∈/ FV Γ wf-type (sig Θ) *T* Θ,Γ T (Abs-fv *xTt*) Θ,Γ T (Abs *T t*) τ *u* : *T* wf-term (sig Θ) *u* Θ,Γ subst-bv *u t* wf-theory Θ Θ,Γ *u* wf-term (sig Θ) *t* τ *t* : prop Θ,Γ − {*t*} *t* =⇒ *u* Θ,Γ1 *t* =⇒ *u* Θ,Γ2 *t* Θ,Γ1 ∪ Γ2 *u*

where FV Γ = ( *t*∈Γ fv *t*).

#### **7.2 Equality**

Most rules about equality are not part of the inference system but are axioms (the set eq-axs mentioned above). Consequences are obtained via the axiom rule.

The first three axioms express that ≡ is reflexive, symmetric and transitive:

$$x \equiv x \qquad x \equiv y \implies y \equiv x \qquad x \equiv y \implies y \equiv z \implies x \equiv z$$

The next two axioms express that terms of type prop (*A* and *B*) are equal iff they are logically equivalent:

$$A \equiv B \implies A \implies B \qquad (A \implies B) \implies (B \implies A) \implies A \equiv B$$

The last equality axioms are congruence rules for application and abstraction:

$$f \equiv g \implies x \equiv y \Longrightarrow (f \cdot x) \equiv (g \cdot y)$$

$$\bigwedge \text{ (Abs } T \text{ (} (f \cdot \mathcal{B} \nu \, 0) \equiv (g \cdot \mathcal{B} \nu \, 0))) \Longrightarrow \text{Abs } T \text{ (} f \cdot \mathcal{B} \nu \, 0) \equiv \text{Abs } T \text{ (} g \cdot \mathcal{B} \nu \, 0)$$

Paulson [30] gives a slightly different congruence rule for abstraction, which allows to abstract over an arbitrary, free *x* in *f* ,*g*. We are able to derive this rule in our inference system.

Finally there are the lambda calculus rules. There is no need for α conversion because α-equivalent terms are already identical thanks to the De Brujin indices for bound variables. For β and η conversion the following rules are added. In contrast to the rest of this subsection, these are not expressed as axioms.

$$\begin{array}{c c c c} & \mathsf{wf\text{-}theory} & \Theta\\ \mathsf{wt\text{-}term (sig } \Theta) \ (\mathsf{Abs} \ T \ t) & \mathsf{wf\text{-}term (sig } \Theta) \ u & \mathsf{\vdash\_{\tau} u \ :\ T}{}(\beta) \\ \hline & \Theta, \Gamma \vdash (\mathsf{Abs} \ T \ t \cdot u) \equiv \mathsf{subst} \ \mathsf{st} \ \mathsf{b} \ u \ t \\ \hline & \mathsf{wf\text{-}theory } \Theta & \mathsf{wf\text{-}term (sig } \Theta) \ t & \mathsf{\vdash\_{\tau} t \ :\ T \to T' }(\eta) \\ \hline & \Theta, \Gamma \vdash \mathsf{Abs} \ T \ (t \cdot \mathcal{B} \mathsf{v} \ 0) \equiv t \end{array}$$

Rule (β) uses the substitution function subst-bv as explained in Section 4 (and defined in the Appendix).

Rule (η) requires a few words of explanation. We do not explicitly require that *t* does not contain Bv *0*. This is already a consequence of the precondition that τ *t* : *T* → *T* : it implies that *t* is closed. For that reason it is perfectly unproblematic to remove the abstraction above *t*.

#### **7.3 Type Class Reasoning**

Wenzel [38] encoded class constraints of the form "type *T* has class *c*" in the term language as follows. There is a unary type constructor named *"itself"* and *T* itself abbreviates Ty *"itself"* [*T*]. The notation *TYPET* itself is short for Ct *"type"* (*T* itself ) where *"type"* is the name of a new uninterpreted constant. You should view *TYPET* itself as the term-level representation of type *T*.

Next we represent the predicate "is of class *c*" on the term level. For this we define some fixed injective mapping const-of-class from class to constant names. For each new class *c* a new constant const-of-class *c* of type *T* itself → prop is added. The term Ct (const-of-class *c*) (*T* itself → prop) *· TYPET* itself represents the statement "type *T* has class *c*". This is the inference rule deriving such propositions:

wf-theory Θ const-type (sig Θ) (const-of-class *C* ) = Some ( *a* itself → prop) wf-type (sig Θ) *T* has-sort (osig (sig Θ)) *T* {*C* } Θ,Γ Ct (const-of-class *C* ) (*T* itself → prop) *· TYPET* itself

This is how the has-sort inference system is integrated into the logic.

This concludes the presentation of M. We have shown some minimal sanity properties, incl. that all provable terms are of type prop and wellformed:

**Theorem 1.** Θ,Γ *t* −→ τ *t* : prop ∧ wf-term (sig Θ) *t*

The attentive reader will have noticed that we do not require unused hypotheses in Γ to be wellformed and of type prop. Similarly, we only require wf-theory Θ in rules that need it to preserve wellformedness of the terms and types involved. To restrict to wellformed theories and hypotheses we define a top-level provability judgment that requires wellformedness:

Θ,Γ *t* = (wf-theory Θ ∧ (∀ *h*∈Γ . wf-term (sig Θ) *h* ∧ τ *h* : prop) ∧ Θ,Γ *t*)

# **8 Proof Terms and Checker**

Berghofer and Nipkow [4] added proof terms to Isabelle. We present an executable checker for these proof terms that is proved sound w.r.t. the above formalization of the metalogic. Berghofer and Nipkow also developed a proof checker but it was unverified and checked the generated proof terms by feeding them back through Isabelle's unverified inference kernel.

It is crucial to realize that all we need to know about the proof term checker is the soundness theorem below. The internals are, from a soundness perspective, irrelevant, which is why we can get away with sketching them informally. This is in contrast to the logic itself, which acts like a specification, which is why we presented it in detail.

This is our data type of proof terms:

```
datatype proofterm = PAxm term (((var × sort) × typ) list) | PBound nat
 | Abst typ proofterm | AbsP term proofterm | Appt proofterm term
 | AppP proofterm proofterm | OfClass typ name | Hyp term
```
These proof terms are not designed to record proofs in our inference system, but to mirror the proof terms generated by Isabelle. Nevertheless, the constructors of our proof terms correspond roughly to the rules of the inference system. PAxm contains an axiom and a type substitution. This substitution is encoded as an association list instead of a function. AbsP and Abst correspond to introduction of =⇒ and -, AppP and Appt correspond to the respective eliminations. Hyp and PBound relate to the assumption rule, where Hyp refers to a free assumption while PBound contains a De Brujin index referring to an assumption added during the proof by an AbsP constructor. OfClass denotes a proof that a type belongs to a given type class.

Isabelle looks at terms modulo αβη-equivalence and therefore does not save β or η steps, while they are explicit steps in our inference system. Therefore we have no constructors corresponding to the (β) and (η) rules. The remaining equality axioms are naturally handled by the PAxm constructor.

In the rest of the section we discuss how to derive an executable proof checker. Executability means that the checker is defined as a set of recursive functions that Isabelle's code generator can translate into one of a number of target languages, in particular its implementation language SML [5,9,8].

Because of the approximate correspondence between proof term constructors and inference rules, implementing the proof checker largely amounts to providing executable versions of each inference rule, as in LCF: each rule becomes a function that checks the side conditions, and if they are true, computes the conclusion from the premises given as arguments. The overall checker is a function

# replay :: *theory* ⇒ *proofterm* ⇒ *term option*

In particular we need to make the inductive wellformedness checks for sorts, types and terms, signatures and theories executable. Mostly, this amounts to providing recursive versions of inductive definitions and proving them equivalent.

We now discuss some of the more difficult implementation steps. To model Isabelle's view of terms modulo αβη-equivalence, we βη normalize our terms (αequivalence is for free thanks to De Brujin notation) during the reconstruction of the proof. A lengthy proof shows that this preserves provability (we do not go into the details):

wf-theory Θ ∧ finite Γ ∧ (∀ *A*∈Γ . wt-term (sig Θ) *A* ∧ τ *A* : prop) ∧ Θ,Γ *t* ∧ beta-eta-norm *t* = Some *u* −→ Θ,Γ *u*

Isabelle's code generator needs some help handling the maps used in the (ordersorted) signatures. We provide a refinement of maps to association lists. Another problematic point is the definition of the type instance relation (-), which contains an (unbounded) existential quantifier. To make this executable, we provide an implementation which tries to compute a suitable type substitution. In another step, we refine the type substitution to an association list as well.

In the end we obtain a proof checker

# check-proof Θ *P p* = (wf-theory Θ ∧ replay Θ *P* = Some *p*)

that checks theory Θ and checks if proof *P* proves the given proposition *p*. The latter check is important because the Isabelle theorems that we check contain both a proof and a proposition that the theorem claims to prove. Function checkproof checks this claim. As one of our main results, we can prove the correctness of our checker:

# **Theorem 2.** check-proof Θ *P p* −→ Θ,set (hyps *P*) *p*

The proof itself is conceptually simple and proceeds by induction over the structure of proof terms. For each proof constructor we need to show that the corresponding inference rule leads to the same conclusion as its functional version used by replay. Most of the proof effort goes into a large library of results about terms, types, signatures, substitutions, wellformedness etc. required for the proof, most importantly the fact that βη normalization preserve provability.

# **9 Size and Structure of the Formalization**

All material presented so far has been formalized in Isabelle/HOL. The definition of the inference system (incl. types, terms etc.) resides in a separate theory *Core* that depends only on the basic library of Isabelle/HOL. It takes about 300 LOC and is fairly high level and readable – we presented most of it. This is at least an order or magnitude smaller than Isabelle's inference kernel (which is not clearly delineated) – of course the latter is optimized for performance. Its abstract type of theorems alone takes about 2,500 LOC, not counting any infrastructure of terms, types, unification etc.

The whole formalization consists of 10,000 LOC. The main components are:

# **10 Integration with Isabelle**

As explained above, Isabelle generates SML code for the proof checker. This code has its own definitions of types, terms etc. and needs to be interfaced with the corresponding data structures in Isabelle. This step requires 150 lines of handwritten SML code (*glue code*) that translates Isabelle's data structures into the corresponding data structures in the generated proof checker such that we can feed them into check-proof. We cannot verify this code and therefore aim to keep it as small and simple as possible. This is the reason for the previously mentioned *intentional implementation bias* we introduced in our formalization. We describe now how the various data types are translated. We call a translation trivial if it merely replaces one constructor by another, possibly forgetting some information.

The translation of types and terms is trivial as their structure is almost identical in the two settings. For Isabelle code experts it should be mentioned that the two term constructors Free and Var in Isabelle (which both represent free variables but Var can be instantiated by unification) are combined in type *var* of the formalization which we left unspecified but which in fact looks like this: **datatype** *var* = *Free name* | *Var indexname*. This is purely to trivialize the glue code, in our formalization *var* is totally opaque.

Proof term translation is trivial except for two special cases. Previously proved lemmas become axioms in the translation (see also below) and so-called "oracles" (typically the result of unfinished proofs, i.e. "sorry" on the user level) are rejected (but none of the theories we checked contain oracles). Also remember that the translation of proofs is not safety critical because all that matters is that in the end we obtain a correct proof of the claimed proposition.

We also provide functions to translate relevant content from the background theory: axioms and (order-sorted) signatures. This mostly amounts to extracting association lists from efficient internal data structures. Translating the axioms also involves translating some alternative internal representation of type class constraints into their standard form presented in Sect. 7.3.

The checker is integrated into Isabelle by calling it every time a new named theorem has been proved. The set of theorems proved so far is added to the axiomatic basis for this check. Cyclic dependencies between lemmas are ruled out by this ordering because every theorem is checked before being added to the axiomatic basis. However, an explicit cyclicity check is not part of the formalization (yet), which speaks only about checking single proofs.

#### **11 Running the Proof Checker**

We run this modified Isabelle with our proof checker on multiple theories in various object logics contained in the Isabelle distribution. A rough overview of the scope of the covered material for some logics and the required running times can be found in the following table. The running times are the total times for running Isabelle, not just the proof checking, but the latter takes 90% of the time. All tests were performed on a Intel Core i7-9750H CPU running at 2.60GHz and 32GB of RAM.

We can check the material in several smaller object logics in their entirety. One of the larger such logics is first-order logic (FOL). These logics do not develop any applications but FOL comes with proof automation and theories testing that automation, in particular Pelletier's collection of problems that were considered challenges in their day [32]. Because the proofs are found automatically, the resulting proof terms will typically be quite complex and good test material for a proof checker.

The logic ZF (Zermelo-Fraenkel set theory) builds on FOL but contains real applications and is an order of magnitude larger than FOL. We are able to check all material formalized in ZF in the Isabelle distribution.

Isabelle's most frequently used and largest object logic is HOL. We managed to check about 12% of the Main library. This includes the basic logic and the libraries of sets, functions, orderings, lattices and groups. The formalizations are non-trivial and make heavy use of Isabelle's type classes.

Why can we check about five times as many lines of code in ZF compared to HOL? Profiling revealed that the proof checker spends a lot of time in functions that access the signature, especially the wellformedness checks. The primary reasons: inefficient data structures (e.g. association lists) and thus the running time depends heavily on size of signature and increases with every new constant, type and class. To make matters worse, there is no sharing of any kind in terms/types and their wellformedness checks. Because ZF is free of polymorphism and type classes, these wellformedness checks are much simpler.

## **12 Trust Assumptions**

We need to trust the following components outside of the formalization:

Because users currently cannot examine Isabelle's internal data structures that we start from, they have to trust Isabelle's front end that parses and transforms some textual input file into internal data structures. One could add a (possibly verified) presentation layer that outputs those internal representations into a readable format that can be inspected, while avoiding the traps Adams [3] is concerned with.

# **13 Future Work**

Our primary focus will be on scaling up the proof checker to not just deal with all of HOL but with real applications (including itself!). There is a host of avenues for exploration. Just to name a few promising directions: more efficient data structures than association lists (e.g. via existing frameworks [19,20]); caching of wellformedness checks for types and terms; exploiting sharing within terms and types (tricky because our intentionally simple glue code creates copies); working with the compressed proof terms [5] that Isabelle creates by default instead of uncompressing them as we do now.

We will also upgrade the formalization of our checker from individual theorems sets of theorems, explicitly checking cyclic dependencies (which are currently prevented by the glue code, see Sect. 10).

A presentation layer as discussed in Sect. 12 would not just allow the inspection of the internal representation of the theories but could also be extended to the proofs themselves, thus permitting checkers to be interfaced with Isabelle on a textual level instead of internal data structures.

It would also be nice to have a model-theoretic semantics for M. We believe that the work by Kunˇcar and Popescu [15,16,17,18] could be adapted from HOL to M. This would in particular yield semantically justified cyclicity checks for constant and type definitions which we currently treat as axioms because a purely syntactic justification is unclear.

#### **Acknowledgements**

We thank Kevin Kappelmann, Magnus Myreen, Larry Paulson, Andrei Popescu, Makarius Wenzel and the anonymous reviewers for their comments.

## **A Appendix**

```
subst-bv u t = subst-bv2 t0u
```