GRUNGE: A Grand Unified ATP Challenge

TL;DR

This paper introduces GRUNGE, a comprehensive benchmark of theorem proving problems translated into various logical formalisms, enabling performance comparison of different automated theorem provers and fostering integrated learning approaches.

Contribution

It presents a large, unified set of theorem proving problems across multiple logical formalisms, facilitating systematic evaluation and combined use of ATP systems.

Findings

Enables comparison of ATP systems across different logics

Provides a large, diverse benchmark for theorem proving

Supports multi-formalism learning and system integration

Abstract

This paper describes a large set of related theorem proving problems obtained by translating theorems from the HOL4 standard library into multiple logical formalisms. The formalisms are in higher-order logic (with and without type variables) and first-order logic (possibly with multiple types, and possibly with type variables). The resultant problem sets allow us to run automated theorem provers that support different logical formats on corresponding problems, and compare their performances. This also results in a new "grand unified" large theory benchmark that emulates the ITP/ATP hammer setting, where systems and metasystems can use multiple ATP formalisms in complementary ways, and jointly learn from the accumulated knowledge.

Tables

Table 1. Table 1: Number of HOL4 formulae in each category.

	First-order		Higher-order		Combined
Uni-sorted	1632	(FOF)	0		1632
Monomorphic	2232	(TF0)	3683	(TH0)	5915
Polymorphic	1536	(TF1)	6650	(TH1)	8186
Combined	5400		10333		15733

Table 2. Table 2: Number of theorems proved, out of 12140. Each ATP is evaluated on all its supported TPTP formats.

System	TH1-I	TH0-I	TH0-II	TF1-I	TF0-I	TF0-II	FOF-I	FOF-II	Union
agsyHOL 1.0 [32]		1374	1187						1605
Beagle 0.9.47 [3]					2008	2047	2449	2498	3183
cocATP 0.2.0		899	599						1000
CSE_E 1.0 [51]							4251	3102	4480
CVC4 1.6 [2]					4851	3991	5030	3746	5709
E 2.2 [41]					4277	3622	4618	3844	5118
HOLyHammer 0.21 [27]	5059								5059
iProver 2.8 [29]							2778	2894	3355
iProverModulo 2.5-0.1 [11]					2435	1639	1433	1263	2852
LEO-II 1.7.0 [4]		2579	1923				2119	1968	3702
Leo-III 1.3 [44, 43]	6668	5018	3485	3458	4032	3421	3986	3185	7090
Metis 2.4 [24]							2353	474	2356
Princess 170717 [39, 40]					3646	2138	3162	2086	4096
Prover9 1109a [33]							2894	1742	3128
Satallax 3.3 [10]		2207	1292						2494
SPASS 3.9 [50]							2850	3349	3821
Vampire 4.3 [30]					4837	4693	4008	4928	5929
ZenonModulo [15]				1071	1038	1041	1026	1198	1751
Zipperposition 1.4 [13]		2252	2161	3771	3099	2576	2531	1795	4251
Union	6824	5209	3771	4663	5732	5074	5909	5249	7412

Equations

$$\forall k.\mathsf{linear}(\lambda x.k\times x)$$

$$\forall kx.\mathbf{f}kx=k\times x$$

$$\forall k.\mathsf{linear}(\mathbf{f}k)$$

$$\forall x.x=\mathsf{COND}(x=0)0x$$

$$\forall x.\mathbf{f}x\iff (x=0)$$

$$\forall x.x=\mathsf{COND}(\mathbf{f}x)0x$$

$$\forall fg(\forall x.\mathsf{ap}fx=\mathsf{ap}gx)\Rightarrow f=g$$

$$\mathsf{SUC}0=1\wedge \exists y.\mathsf{MAP}\mathsf{SUC}y\ne y$$

$$\mathsf{SU}{\mathsf{C}}_{1}x=\mathsf{ap}\mathsf{SU}{\mathsf{C}}_{0}x,\dots$$

$${\mathsf{SUC}}_1{0}_0=1_0\wedge \exists y.{\mathsf{MAP}}_2{\mathsf{SUC}}_{0}y\ne y$$

$$\forall xy:o.(\mathsf{p}(x)\iff \mathsf{p}(y))\Rightarrow (x=y)$$

$$\mathsf{p}(\mathsf{true}),\neg \mathsf{p}(\mathsf{false}),\forall x:o.x=\mathsf{true}\vee x=\mathsf{false}$$

$$\mathsf{ap}$$

$$\forall x:\mu .\mathsf{s}(\hat{\nu },{\mathsf{i}}_{\nu }({\mathsf{j}}_{\nu }(\mathsf{s}(\hat{\nu },x))))=\mathsf{s}(\hat{\nu },x)$$

$$\forall x:\tilde{\nu }.{\mathsf{j}}_{\nu }(\mathsf{s}(\hat{\nu },{\mathsf{i}}_{\nu }(x)))=x$$

$$\forall x_1:\widetilde{{\nu }_1}...x_n:\widetilde{{\nu }_n}.\mathsf{s}({\nu }_0,{\mathsf{i}}_{{\nu }_0}({\widetilde{c_n}}^{\nu }(x_1,...,x_n)))=\mathsf{s}({\nu }_0,\widehat{c_n}(\mathsf{s}({\nu }_1,{\mathsf{i}}_{{\nu }_1}(x_1)),...,\mathsf{s}({\nu }_n,{\mathsf{i}}_{{\nu }_n}(x_n)))$$

$$\forall \hat{x}.\mathsf{s}(\widehat{\mathsf{num}},\hat{\mathsf{I}}(\mathsf{s}(\widehat{\mathsf{num}},\hat{x})))=\mathsf{s}(\widehat{\mathsf{num}},\hat{x})$$

$$\forall \tilde{x}:\widetilde{\mathsf{num}}.{\mathsf{j}}_{\mathsf{num}}(\hat{\mathsf{I}}(\mathsf{s}(\widehat{\mathsf{num}},{\mathsf{i}}_{\mathsf{num}}(\tilde{x}))))=\tilde{x}$$

$$\exists \tilde{f}:fun\_num\_num.{\widetilde{\text{ap}}}^{\nu }(\tilde{f},{\tilde{0}}^{\mathsf{num}})={\tilde{0}}^{\mathsf{num}}$$

$$\exists \tilde{f}:\widetilde{\mathsf{num}}\to \widetilde{\mathsf{num}}.\tilde{f}{\tilde{0}}^{\mathsf{num}}={\tilde{0}}^{\mathsf{num}}$$

$$\forall Q\in \mathsf{bool}.\forall R\in \mathsf{bool}.(\mathsf{p}Q\leftrightarrow \mathsf{p}R)\to Q=R$$

$$\forall x:\alpha \to \beta .\forall x^{\prime }:\alpha .{\mathsf{LET}}^{\alpha ,\beta }x{x}^{\prime }=x{x}^{\prime }.$$

$$\forall AB:\delta .\forall f\in (\mathsf{arr}AB).\forall x\in A.\mathsf{ap}(\mathsf{ap}(\mathsf{LET}AB)f)x=\mathsf{ap}fx$$

$$\forall AB:\delta .\mathsf{LET}AB=\mathsf{lam}(\mathsf{arr}AB)(\lambda f:\iota .\mathsf{lam}A(\lambda x:\iota .\mathsf{ap}fx)).$$

$$\forall A\cdots \forall B\cdots \mathsf{LET}AB={\mathbf{f}}_{14}AB,$$

$$\forall A\cdots \forall B\cdots \forall f\in (\mathsf{arr}AB).\mathsf{ap}({\mathbf{f}}_{14}AB)f={\mathbf{f}}_{13}ABf$$

$$\forall A\cdots \forall B\cdots \forall f\in (\mathsf{arr}AB).\forall x\in A.\mathsf{ap}({\mathbf{f}}_{13}ABf)x=\mathbf{ap}fx.$$

Full text

1 Introduction

A hammer [7] for an interactive theorem prover (ITP) [22] typically translates an ITP goal into a formalism used by an automated theorem prover (ATP). Since the most successful ATPs have so far been for untyped first-order logic, the focus has been on first-order translations. There is also interest in ATPs working in richer formalisms, such as monomorphic and polymorphic, typed first-order, and higher-order logics. The TPTP formats for various formalisms have been adopted for this work, viz. FOF [46] TF0 [47], TF1 [8], TH0 [5], and TH1 [26]. An interesting related task is the creation of a (grand) unified large-theory benchmark that allows fair comparison of such ATP systems, their combination and integration with premise selectors and machine learners [1], across different formalisms. As a step towards creating such benchmarks we present two families of translations from the language of HOL4 [42] to the various TPTP formats. We have implemented these translations and plan to use them as the first “GRand UNified ATP challenGE” (GRUNGE) benchmarks, generalizing existing benchmarks such as the CakeML export [31] that was used in the large-theory benchmark (LTB) division of the CASC-J9 ATP competition [48].

The rest of the paper is structured as follows. Section 2 introduces notation and the HOL syntax. Section 3 introduces the problems – the HOL4 standard library. Section 4 introduces the first family of translations, and Section 5 introduces the second family of translations. Section 6 discusses and compares the translations on an example, and Section 7 evaluates the translations using existing ATPs. Section 8 describes the CASC-27 LTB division, which is based on these translations. Related work is discussed in Section 9.

2 Preliminaries

Since this work is based on the HOL4 standard library, it is necessary to start with brief comments about the syntax and notion of proof in HOL4. More detailed information is in [42, 19]. HOL4, like several other ITPs (e.g., Isabelle/HOL [36], HOL Light [20] or ProofPower [28]), is based on an extension of Church’s simple type theory [12] that includes prefix polymorphism and type definitions [19]. HOL4 includes a type $o$ of propositions, a type $\iota$ of individuals and a type $(\sigma\to\tau)$ of functions from a type $\sigma$ to a type $\tau$. Parentheses are omitted, with $\to$ associating to the right. In addition, there are type variables $\alpha$ and defined types. At each point in the development of the HOL4 library there is a finite set of (previously defined) constants $c$, and a a finite set of (previously defined) type constructors $\kappa$ giving a type $\kappa(\sigma_{1},\ldots,\sigma_{n})$ for types $\sigma_{1},\ldots,\sigma_{n}$. For simplicity we consider the signature to be fixed, to avoid the need to specify the types and terms relative to an evolving signature.

Terms are generated from constants $c$ and variables $x$ using application $(s\ t)$ and $\lambda$-abstractions $(\lambda x:\sigma.t)$ in the expected way, for terms $s$ and $t$. Parentheses are omitted, with application associating the left. Binders have scope as far to the right as possible, consistent with parentheses. Multiple binders over the same type can be written in a combined form, e.g., $\lambda xy:\sigma.t$ means $\lambda x:\sigma.\lambda y:\sigma.t$.

Constants may be polymorphic. There are two primitive polymorphic logical constants: $=^{\alpha}$ is polymorphic with type $\alpha\to\alpha\to o$ and $\varepsilon^{\alpha}$ is polymorphic with type $(\alpha\to o)\to\alpha$, where $\alpha$ is a type variable. When terms are defined, such constants are used with a fixed type for $\alpha$ written as a superscript. New polymorphic constants can be defined within a HOL4 theory.

Aside from $=^{\alpha}$ and $\varepsilon^{\alpha}$, implication $\Rightarrow$ of type $o\to o\to o$ is primitive. From these primitive logical constants it is possible to define $\land$, $\lor$ and $\neg$, as well as polymorphic operators $\forall^{\alpha}$ and $\exists^{\alpha}$. The usual notation is used for these logical connectives, so that the binder notation $\forall^{\sigma}(\lambda x:\sigma.t)$ is written as $\forall x:\sigma.t$, using the same binding conventions as for $\lambda$-abstractions. Similarly, $\exists^{\sigma}(\lambda x:\sigma.t)$ is written as $\exists x:\sigma.t$.

Terms of type $o$ are called propositions, and we use $\varphi$ and $\psi$ to range over propositions. A sequent is a pair $\Gamma\vdash\varphi$ where $\Gamma$ is a finite set of propositions and $\varphi$ is a proposition. There is a notion of HOL4 provability for sequents. While our translations map HOL4 sequents to TPTP formulae, it is not our intention to mirror HOL4 provability in the target format. The intention, roughly speaking, is to gain information about when a HOL4 theorem is a consequence of previous HOL4 theorems, in some logic weaker than HOL4.

From the simplest perspective, each translation translates HOL4 types and HOL4 terms (including propositions) to terms in the target format. A type, term or sequent with no type variables is called monomorphic. As an optimization, some of the translations translate some monomorphic HOL4 types to types in the target language. As a common notation throughout this paper, a HOL4 type $\sigma$ translated as a term is written as $\hat{\sigma}$, and $\sigma$ translated as a type is written as $\tilde{\sigma}$. Another optimization is to translate HOL4 propositions (and sequents) to the level of formulae in the target language.

3 Problem Set: The HOL4 Standard Library

Version Kananaskis-12 of the HOL4 standard library contains 15733 formulae: 8 axioms, 2294 definitions, and 13431 theorems. If most of the formulae were monomorphic and fell into a natural first-order fragment of HOL4, then there would be a natural translation into the FOF format. However, many formulae are either polymorphic or higher-order (or both), as Table 1 shows (note that the numbers are not cumulative, e.g., the 2232 monomorphic first-order formulae do not include the 1632 uni-sorted first-order formulae, which could also be processed by an ATP that can handle the monomorphic types). The problem set consists of 12140 theorems proven in the HOL4 standard library1111291 theorems were not included due to dependencies being erased during the build of the HOL4 library., in the context of a finite set of dependencies used in the HOL4 proof [16].

4 Syntactic Translations via First-Order Encodings

There already exist many families of translations for HOL to the TPTP format, usually developed for hammers [27, 35]. We have adopted and adapted them: (i) We have made the translations more local, by making them independent for each theorem, i.e., unaffected by other theorems. In particular, this means that when the same lambda function appears in two theorems, lambda-lifting will produce two new functions. (ii) We have made more problems provable (in principle) by introducing additional axioms and relying on an embedding of polymorphic types instead of relying on heuristic monomorphization. (iii) For the TF0 and TH0 formats, we have made use of their polysortedness by expressing the type of monomorphic constants directly using TF0 and TH0 types.

The translations are described in the order $\textsf{TH1}\rightarrow\textsf{TF1}\rightarrow\textsf{FOF}\rightarrow\textsf{TF0}\rightarrow\textsf{TH0}$, as translations to the later formats take advantage of translation techniques used for earlier formats.

4.1 Translating to TH1

TH1 is a language that is strictly more expressive than HOL4. Therefore HOL4 formulae can be represented in TH1 with minimal effort. This produces the TH1-I collection of ATP problems.

Alignment of Logical Constructions.

The TPTP format contains a set of defined constructs that have implicit definitions, and HOL4 objects are mapped to their TPTP counterparts in a natural way. The boolean type $o$ of HOL4 is mapped to the defined TPTP type $o. The arrow type operator is mapped to the TPTP arrow >. All other type operators are declared to take$n$types and give a type, using the TPTP “type of types”$tType. For example, the type operator $\mathit{list}$ has type $tType >$tType.

The TPTP logical connectives $\wedge$, $\vee$, $\Rightarrow$, $\neg$, $=$, $\forall$, $\exists$ are used at the top-level of the translated formula whenever possible, but the corresponding HOL4 constants are used when necessary. Equivalences relating HOL4 logical constants to TPTP connectives are included.

Explicit type arguments.

A HOL4 constant $c$ carries a type $\nu^{\prime}$. This type is an instance of type $\nu$ that was given to $c$ when $c$ was created. By matching $\nu$ with $\nu^{\prime}$, a type substitution $s$ can be inferred. Ordering the type variables in the domain of $s$, the implicit type arguments of $c$ are deduced. Making the quantification of type variables and the type arguments explicit is required in the TH1 format. The effect that this requirement has on a constant declaration and a formula is shown in Example 1.

Example 1

Explicit type arguments and type quantifications

[TABLE]

4.2 Translating to TF1

To produce the TF1-I collection of ATP problems, all the higher-order features of the HOL4 problems have to be eliminated. This is done in a sequence of steps.

Lambda-lifting and Boolean-lifting.

One of the higher-order features is the presence of lambda-abstraction. The translation first uses the extensionality property to add extra arguments to lambdas appearing on either side of an equality, and then beta-reduce the formula. Next lambda-lifting [14, 35] is used. Lambda-lifting creates a constant $\mathbf{f}$ for the leftmost outermost lambda-abstractions appearing at the term-level. This constant $\mathbf{f}$ replaces the lambda-abstraction in the formula. A definition is given for $\mathbf{f}$, which may involve some variable capture - see Example 2. This procedure is repeated until all the atoms are free of lambda-abstractions. The definitions are part of the background theory, and are considered to be axioms in the TF1 problem even if they were created from the conjecture.

Example 2

Lambda-lifting with variable capture

[TABLE]

A similar method can be applied to move some logical constants from the term-level to the formula-level - see Example 3 (this optimization is not applied in our second family of translations).

Example 3

Boolean-lifting

[TABLE]

To allow the ATPs to create their own encoded lambda-abstractions, axioms for the combinators $\mathsf{S}$, $\mathsf{K}$ and $\mathsf{I}$ are added to every problem. These axioms are omitted in the second family of translations. In the TH0-II versions of the problem, combinators are not needed since all simply typed $\lambda$-calculus terms are already representable. In the TF0-II and FOF-II versions only an axiom for $\mathsf{I}$ and a partially applied axiom for $\mathsf{K}$ are included. Combinator axioms enlarge the search space, which hinders the ATPs unnecessarily because they are not needed for proving most of the theorem.

Apply operator and arity equations.

As functions cannot be passed as arguments in first-order logic, an explicit apply operator $\mathsf{ap}$ is used to apply a function to an argument. This way all objects (constants and variables) have arity zero except for the apply operator which has arity two. The HOL4 functional extensionality axiom is added to all problems, as it expresses the main property of the apply operator:

[TABLE]

This axiom also demonstrates how the higher-order variables $f$ and $g$ become first-order variables after the introduction of $\mathsf{ap}$.

To limit the number of apply operators in a formula, versions of each constant are defined for all its possible arities, in terms of the zero-arity version. These constants are used in the translated formula - see Example 4.

Example 4

Using constants with their arity

[TABLE]

If the return type of a constant is a type variable then some of its instances can expect an arbitrarily large numbers of arguments. In the case where the number of arguments $n^{\prime}$ of an instance exceeds the number of arguments $n$ of the primitive constant, variants of this constant are not created for this arity. Instead, the apply operator is used to reduce the number of arguments to $n$. For example, the term $\mathsf{I}\ \mathsf{I}\ x$ is not translated to $\mathsf{I_{2}}\ \mathsf{I_{0}}\ x$ but instead to $\mathsf{ap}\ (\mathsf{I_{1}}\ \mathsf{I_{0}})\ x$.

TF1 types.

As a final step, type arguments and type quantifications are added as in Section 4.1 . Moreover, the boolean type of HOL4 is replaced by $o at the formula-level, and by$o$at the term-level (because$o is not allowed at the term-level in a first-order formula). This causes a mismatch between the type of the atom $o$ and the type of the logical connective $o. Therefore an additional operator$\mathsf{p}!:!o\rightarrow$o$is applied on top of every atom. The following properties of$\mathsf{p}$and$o$ are added to every translated problem (written here in the first-order style for function application):

[TABLE]

In a similar manner, the TPTP arrow type cannot be used whenever a function appears as an argument. Instead the type constructor $\mathsf{fun}$ is used, as illustrated by the following constant declaration:

[TABLE]

4.3 Translating to FOF

The translation to FOF, which produces the FOF-I collection of ATP problems, follows exactly the same path as the translation to TF1 except that the types are encoded as first-order terms. To represent the fact that a first-order term $t$ has type $\nu$, the tagging function $\mathsf{s}$, introduced by Hurd [23], is used: every term $t$ of type $\nu$ is replaced by $\mathsf{s}(\hat{\nu},t)$. Going from the type $\nu$ to the term $\hat{\nu}$ effectively transforms type variables into term variables, and type operators into first-order functions and constants. Type arguments are unnecessary as the tags contain enough information. In practice, the $\mathsf{s}$ tagging function prevents terms of different types from unifying, and allows instantiation of type variables - see Example 5.

Example 5

Type instantiation

[TABLE]

4.4 Translating to TF0

An easy way to translate HOL4 formulae to TF0, which produces the TF0-I collection of ATP problems, is to take the translation to FOF and inject it into TF0.

Trivial Injection from FOF to TF0.

The first step is to give types to all the constants and variables appearing the the FOF formula. A naive implementation would be to give the type $\iota^{n}\rightarrow\iota$ to symbols with arity $n$. However, since it is known that the first argument comes from the universe of non-empty types, and the second argument comes from the universe of untyped terms, an explicit distinction can be made. The type of $\mathsf{s}$ is defined to be $\delta\times\mu\rightarrow\iota$, with $\delta$ being the universe of non-empty types, $\mu$ being the universe of untyped terms, and $\iota$ being the universe of typed terms. After this translation a type operator (or type variable) with $m$ arguments has type $\delta^{m}\rightarrow\delta$, and a function (or term variable) with $n$ arguments has type $\iota^{n}\rightarrow\mu$. The type of $\mathsf{p}$ is \mathsf{p}:\iota\rightarrow{\tt\o}$. Declaring the type of all these objects achieves a trivial translation from FOF with tags to TF0.

Using Special Types.

To take full advantage of the polysortedness of TF0, a constant $\tilde{c_{n}}^{\nu}$ is declared for every constant $c_{n}$, with arity $n$ and monomorphic type $\nu$. The type of $\tilde{c_{n}}^{\nu}$ is declared to be $(\tilde{\nu_{1}}\times\ldots\times\tilde{\nu_{n}})\rightarrow\tilde{\nu_{0}}$, where $\tilde{\nu_{1}},\ldots,\tilde{\nu_{n}}$, and $\tilde{\nu_{0}}$ are basic types. A basic type constructs a single type from a monomorphic type, e.g., $\mathit{list\_real}$ for $\mathit{list[real]}$, $\mathit{fun\_o\_o}$ for $\mathit{fun(o,o)}$. The basic types are special types, and are declared using $tType. Thanks to these new constants monomorphic formulae can be expressed in a natural way, without type encodings in the formula. Nevertheless, an ATP should still be able to perform a type instantiation if necessary. That is why we relate the monomorphic representation with its tagged counterpart.

If a term has a basic type then it lives in the monomorphic world where as a term of type $\iota$ it belongs to the tagged world. All monomorphic terms (constructed from monomorphic variables and constants) can be expressed in the monomorphic world. To relate the two representations of the same HOL4 term an “injection” $\mathsf{i}_{\nu}$ and a “surjection” $\mathsf{j}_{\nu}$ are defined for each basic type $\tilde{\nu}$. The constants $\mathsf{i}_{\nu}:\tilde{\nu}\rightarrow\mu$ and $\mathsf{j}_{\nu}:\iota\rightarrow\tilde{\nu}$ must respect the following properties, which are included as axioms in the translated problems:

[TABLE]

Whenever $\tilde{c_{n}}^{\nu}$ is an instance of a polymorphic function $\hat{c_{n}}$, the following equation is included in the TF0 problem, which relates the two representatives:

[TABLE]

Example 6 shows how “injections”, “surjections”, and special types can be used to translate a theorem mixing polymorphic and monomorphic elements.

Example 6

Special types

The polymorphic function $I$ is applied to the monomorphic variable $x$. Using special types, type tags can be dropped for $x$.

[TABLE]

Effect on defined operators.

The $\mathsf{ap}$ operator is treated in the same way as every other constant. In particular, a different version of $\mathsf{ap}$ is created for each monomorphic type. The type of $\mathsf{p}$ becomes \tilde{o}\rightarrow\o$, and the projection$\mathsf{j}_{o}$ is used to transfer atoms from the tagged world to the monomorphic world.

If the presence of the $\mathsf{p}$ predicate and the inclusion of additional equations are ignored, our translation of a HOL4 first-order monomorphic formula using special types to TF0 is simply the identity transformation.

4.5 Translating to TH0

Translating from HOL4 to TH0, which produces the TH0-I collection of ATP problems, is achieved in a way similar to the translation to TF0. The HOL4 formulae are first translated to FOF and then trivially injected into TH0. Special types are used for basic types extracted from monomorphic types. The set of higher-order basic types is slightly different from the first-order one, where we recursively remove arrow types until a non-arrow constructor is found. In the higher-order setting a single monomorphic constant $\tilde{c}^{\nu}$ is used to replace all arity versions of $c$: $\forall f\ x.\ \tilde{\mathsf{ap}}^{\nu}\ f\ x=f\ x$. Another benefit of the expressivity of TH0 is that the basic type $\tilde{o}$ can be replaced by \o$, and the the predicate$\mathsf{p}$ can be omitted. The effect of the previous steps is illustrated in Example 7.

Example 7

Translations of $\exists f.\ f\ 0=0$

In this example $\tilde{\textsf{ap}}^{\nu}$ has type $(\mathsf{fun\_num\_num}\times\widetilde{\mathsf{num}})\to\widetilde{\mathsf{num}}$ where $\mathsf{fun\_num\_num}$ is the special type corresponding to $\mathsf{num}\to\mathsf{num}$.

[TABLE]

In order to have the same shallowness result for TH0 as for TF0, it would be necessary to replace monomorphic constants created by the lifting procedure by their lambda-abstractions. We chose to keep the definitions for the lifted constants, as they allow some term-level logical operators to be pushed to the formula level.

5 Semantic Translations via Set Theory Encodings

The second family of translations into TH0, TF0, and FOF is semantically motivated [38]: we make use of constructors known to be definable in set theory. Types and terms are translated to sets, where types must translate to non-empty sets. The translation may optionally use other special types for monomorphic types in the HOL4 source. In the TH0 case the builtin type $o can be used for the HOL4 type$o$. In the first-order cases HOL4 terms of type$o$are sometimes translated to terms, and sometimes to formulae, depending on how the HOL4 term is used. In the TF0 case a separate type${\tilde{o}}$of booleans is declared, which is used as the type of terms translated from HOL4 terms of type$o$. In the FOF case this approach is not possible, as all terms have the same type (intuitively representing sets). The other main difference between the translation to TH0 and the translations to the first-order languages is that the first-order translations make use of lambda lifting [14, 35]. As a result of the translations we obtain three new collections of ATP problems are produced: TH0-II, TF0-II and FOF-II.

5.1 Translating to TH0

The base type $o$ for propositions is written as $o in TH0, and$\iota$for individuals is written as$i. In addition a base type $\delta$ is declared. The translation treats elements of type $\iota$ as sets, and elements of type $\delta$ as non-empty sets. The basic constants used in the ATP problems are as follows:

• •

$\mathsf{bool}:\delta$ is used for a fixed two element set.

• •

$\mathsf{ind}:\delta$ is used for a fixed non-empty set corresponding to HOL4’s type of individuals.

• •

$\mathsf{arr}:\delta\to\delta\to\delta$ is used to construct the function space of two sets.

• •

$\mathsf{mem}:\iota\to\delta\to o$ corresponds to the membership relation on sets, where the second set is known to be non-empty. The term $\mathsf{mem}~{}s~{}t$ is written as $s\in t$, and the term $\forall x.x\in s\rightarrow t$ is written as $\forall x\in s.t$.

• •

$\mathsf{ap}:\iota\to\iota\to\iota$ corresponds to set theory level application (represented as a set).

• •

$\mathsf{lam}:\delta\to(\iota\to\iota)\to\iota$ is used to build set bounded $\lambda$-abstractions as sets.

• •

$\mathsf{p}:\iota\to o$ is a predicate that indicates whether or not an element of $\mathsf{bool}$ is true or not.

• •

$\mathsf{i}_{o}:o\to\iota$ is an injection of $o$ into $\iota$, essentially translating false to a set and true to a different set.

The basic axioms included in each ATP problem are:

${\mathbf{Inj}}_{o}$:

$\forall X:o.{\mathsf{i}}_{o}X\in\mathsf{bool}$.

${\mathbf{Iso}}^{1}_{o}$:

$\forall X:o.{\mathsf{p}}({\mathsf{i}}_{o}X)=X$.

${\mathbf{Iso}}^{2}_{o}$:

$\forall X\in\mathsf{bool}.{\mathsf{i}}_{o}({\mathsf{p}}X)=X$.

${\mathbf{ap_{tp}}}$:

$\forall AB:\delta.\forall f\in(\mathsf{arr}~{}A~{}B).\forall x\in A.(\mathsf{ap}~{}f~{}x)\in B$.

${\mathbf{lam_{tp}}}$:

$\forall AB:\delta.\forall F:\iota\to\iota.(\forall x\in A.F~{}x\in B)\rightarrow(\mathsf{lam}~{}A~{}F)\in(\mathsf{arr}~{}A~{}B)$.

${\mathbf{FunExt}}$:

$\forall AB:\delta.\forall f\in(\mathsf{arr}~{}A~{}B).\forall g\in(\mathsf{arr}~{}A~{}B).$

$(\forall x\in A.\mathsf{ap}~{}f~{}x=\mathsf{ap}~{}g~{}x)\rightarrow f=g.$

${\mathbf{beta}}$:

$\forall A:\delta.\forall F:\iota\to\iota.\forall x\in A.(\mathsf{ap}~{}(\mathsf{lam}~{}A~{}F)~{}x)=F~{}x$.

If $\iota$ is interpreted using a model of ZFC and $\delta$ using a copy of the non-empty sets in this model, then the constants above can be interpreted in an obvious way so as to make the basic axioms true.

Given this theory, a basic translation from HOL4 to TH0 is as follows. Each HOL4 type $\alpha$ (including type variables) is mapped to a term $\hat{\alpha}$ of type $\delta$. HOL4 type variables (constants) are mapped to TH0 variables (constants) of type $\delta$. For the remaining cases ${\mathsf{bool}}$, ${\mathsf{ind}}$, and $\mathsf{arr}$ are used. Each HOL4 term $s:\alpha$ is mapped to a TH0 term $\hat{s}$ of type $\iota$, for which the context $\hat{s}\in\hat{\alpha}$ is always known. The invariant can be maintained by including the hypothesis $\hat{x}\in\hat{\alpha}$ whenever $x$ is a variable or a constant. The $\mathsf{ap}$ and $\mathsf{lam}$ constants are used to handle HOL4 applications and $\lambda$-abstractions. The axioms ${\mathbf{ap_{tp}}}$ and ${\mathbf{lam_{tp}}}$ ensure the invariant is maintained. Finally HOL4 propositions (which may quantify over type variables) are translated to TH0 propositions in an obvious way, using $\mathsf{p}$ to go from $\iota$ to $o$, and $\mathsf{i}_{o}$ to go from $o$ to $\iota$, when necessary. As an added heuristic, the translation makes use of TH0 connectives and quantifiers as deeply as possible, delaying the use of $\mathsf{p}$ whenever possible.

Using Special Types.

As with the first family of translations, the second family optimizes by using special types for HOL4 types with no type variables, e.g., ${\mathtt{num}}$ and ${\mathtt{list}}~{}{\mathtt{num}}$. Unlike the first family, special types are not used for monomorphic function types. As a result it is not necessary to consider alternative $\mathsf{ap}$ operators. A basic monomorphic type is a monomorphic type that is not of the form $\alpha\to\beta$. If special types are used, then for each basic monomorphic type occurring in a proposition a corresponding TH0 type $\gamma$ is declared, mappings and axioms relating $\gamma$ to the type $\iota$ of sets are declared, and the type $\gamma$ is used to translate terms of the type and quantifiers over the type when possible. For example, if a basic monomorphic type $\nu$ (e.g., ${\mathtt{num}}$) occurs in a HOL4 proposition, then in addition to translating $\nu$ as a term $\hat{\nu}:\iota$ we also declare a TH0 type $\tilde{\nu}$, ${\mathsf{i}}_{\nu}:\tilde{\nu}\to\iota$ and ${\mathsf{j}}_{\nu}:\iota\to\tilde{\nu}$ along with axioms $\forall x:\tilde{\nu}.{\mathsf{j}}_{\nu}({\mathsf{i}}_{\nu}x)=x$ and $\forall x:\iota.x\in\hat{\nu}\rightarrow{\mathsf{i}}_{\nu}({\mathsf{j}}_{\nu}x)=x$.

One obvious basic monomorphic type is $o$. In the case of $o$ a new type is not declared, but instead the TH0 type $o is used. That is,$\tilde{o}$denotes$o. Note that $\mathsf{i}_{o}:\tilde{o}\to\iota$ is already declared. Additionally, $\mathsf{j}_{o}$ is used as shorthand for $\mathsf{p}$, which has the desired type $\iota\to\tilde{o}$.

Suppose a HOL4 constant $c$ has type $\alpha_{1}\to\ldots\to\alpha_{n}\to\beta$, where $\alpha_{1},\ldots,\alpha_{n},\beta$ are basic monomorphic types with corresponding TH0 types $\tilde{\alpha_{1}},\ldots,\tilde{\alpha_{n}},\tilde{\beta}$. Instead of translating a term $c\,t_{1}\cdots t_{n}$ as a term of type $\iota$, each $t_{i}$ is translated to a term $\hat{t_{i}}$ of type $\tilde{\alpha_{i}}$, and a first order constant $\tilde{c}:\tilde{\alpha_{1}}\to\cdots\to\tilde{\alpha_{n}}\to\tilde{\beta}$ is used to translate to the term $\tilde{c}\,\hat{t_{1}}\cdots\hat{t_{n}}$ of type $\tilde{\beta}$. In such a case an equation relating $\hat{c}$ to $\tilde{c}$ is also included. Since the translation may return a term of type $\iota$ or $\tilde{\alpha}$, where $\alpha$ is a basic monomorphic type, $\mathsf{i}_{\alpha}$ and $\mathsf{j}_{\alpha}$ are used to obtain a term of type $\tilde{\alpha}$ or $\iota$ when one is required. If a quantifier ranges over a monomorphic type $\alpha$, a quantifier over type $\tilde{\alpha}$ is used instead of using a quantifier over type $\iota$ and using $\in$ to guard the quantifier.

5.2 Translating to TF0

There are two main modifications to the translation to TH0 when targeting TF0. Firstly, propositions cannot be treated as special kinds of terms in TF0. In order to deal with this $o$ is treated like other special types by declaring a new type $\tilde{o}$ and functions ${\mathsf{i}}_{o}:\tilde{o}\to\iota$ and ${\mathsf{j}}_{o}:\iota\to\tilde{o}$ along with corresponding axioms as above. Note that unlike the TH0 case, ${\mathsf{j}}_{o}$ differs from ${\mathsf{p}}$. In TF0 ${\mathsf{p}}$ is a unary predicate on $\iota$, and ${\mathsf{j}}_{o}$ is a function from $\iota$ to $\tilde{o}$. In the TF0 versions of the axioms ${\mathbf{Iso}}^{1}_{o}$ and ${\mathbf{Iso}}^{2}_{o}$, ${\mathsf{p}}$ is replaced with ${\mathsf{j}}_{o}$. Secondly, the background theory cannot include the higher-order ${\mathsf{lam}}$ operator. Therefore the ${\mathsf{lam}}$ operator is omitted, and lambda lifting is used to translate (most) HOL4 $\lambda$-abstractions. The two higher-order axioms ${\mathbf{lam_{tp}}}$ and ${\mathbf{beta}}$ are also omitted.

In the TH0 case, the background axioms are enough to infer the following (internal) propositional extensionality principle

[TABLE]

from the corresponding extensionality principle $\forall QR:o.(Q\leftrightarrow R)\rightarrow Q=R$ valid in TH0. This is no longer the case in TF0, so propositional extensionality is added as an axiom.

There are two special cases where lambda lifting can be avoided: identity and constant functions. For this purpose a new unary function $\mathsf{I}$ on sets and a new binary function $\mathsf{K}$ on sets are added. Two new basic axioms are added to the ATP problem for these functions:

Id:

$\forall A:\delta.\forall X\in A.(\mathsf{ap}~{}(\mathsf{I}~{}A)~{}X)=X$.

Const:

$\forall A:\delta.\forall Y:\iota.\forall X\in A.(\mathsf{ap}~{}(\mathsf{K}~{}A~{}Y)~{}X)=Y$.

A HOL4 term $\lambda x:\alpha.x$ is translated as $\mathsf{I}~{}\hat{\alpha}$. For a HOL4 term $\lambda x:\alpha.t$, where $x$ is not free in $t$, $t$ is translated to a first-order term $\hat{t}$ of type $\iota$, and the $\lambda$-term is translated to $\mathsf{K}~{}\hat{\alpha}~{}\hat{t}$. If there is already a function defined for $\lambda x:\alpha.t$ (with the same variable names), then that function is reused. Otherwise, lambda lifting of $\lambda x:\alpha.t$ proceeds as follows. Let $\alpha_{1},\ldots,\alpha_{m}$ be type variables occurring in $\lambda x:\alpha.t$ and $y_{1}:\beta_{1},\ldots,y_{n}:\beta_{n}$ be the free variables occurring in $\lambda x:\alpha.t$. Assume $\hat{t}$ is a first-order term translation of $t$, with $\hat{x}$ of type $\iota$ corresponding to the variable $x$. (Note that this may have involved some lambda lifting.) Let $\mathbf{f}$ be a new $m+n$-ary function returning sets. If special types are not being used, then each argument of $\mathbf{f}$ is a set. If special types are used, then each argument is a set unless it corresponds to $y_{i}:\beta_{i}$, where $\beta_{i}$ is a monomorphic type in which case the argument has type $\tilde{\beta_{i}}$. The following axioms about $\mathbf{f}$ are added to the ATP problem:

$\mathbf{f}_{\mathbf{tp}}$:

$\forall A_{1}\cdots A_{n}:\delta.\forall Y_{1}\cdots Y_{m}:\iota.\cdots(\mathbf{f}~{}A_{1}\cdots~{}A_{n}~{}Y_{1}~{}\cdots~{}Y_{m})\in\hat{\alpha}$.

$\mathbf{f}_{\mathbf{beta}}$:

$\forall A_{1}\cdots A_{n}:\delta.\forall Y_{1}\cdots Y_{m}:\iota.\cdots\forall X\in\hat{\alpha}.\mathsf{ap}~{}(\mathbf{f}~{}A_{1}\cdots~{}A_{n}~{}Y_{1}~{}\cdots~{}Y_{m})~{}X=\hat{t}$.

In these axioms the preconditions that each $Y_{i}$ must be in $\hat{\beta_{i}}$ if $Y_{i}$ has type $\iota$ have been elided (otherwise special types are being used, $\beta_{i}$ is monomorphic, $Y_{i}$ has type $\tilde{\beta_{i}}$, and no guard is required).

5.3 Translating to FOF

In order to translate to FOF, all terms must be translated to the same type, effectively the type $\iota$. This requires omission of any special treatment of monomorphic types, and instead all HOL4 terms are translated to terms of type $\iota$. The type $\delta$ of non-empty sets is also omitted. Instead, $\iota$ is used wherever $\delta$ was used in the TF0 setting, and quantifiers that were over $\delta$ are guarded by a new non-emptiness predicate ${\mathsf{ne}}:\iota\to o$. Aside from these changes, the translation proceeds using lambda lifting as in the TF0 case.

6 Case Study

A very simple HOL4 theorem is $\forall f:\alpha\to\beta.\forall x:\alpha.{\mathsf{LET}}^{\alpha,\beta}~{}f~{}x=f~{}x$, where ${\mathsf{LET}}^{\alpha,\beta}$ is defined to be $\lambda f:\alpha\to\beta.\lambda x:\alpha.fx$. Informally the proof is clear: expand the definition of ${\mathsf{LET}}$ and perform two $\beta$-reductions. However, proving various translated versions of the problem range from trivial to challenging.

The first family of translations make use of a preprocessing step (Section 4.2) that changes the definition of ${\mathsf{LET}}$ from ${\mathsf{LET}}^{\alpha,\beta}=\lambda f:\alpha\to\beta.\lambda x:\alpha.fx$ to

[TABLE]

This step makes the definition of ${\mathsf{LET}}$ the same (up to $\alpha$-conversion) as the theorem. Even if further encodings are applied to obtain a first-order problem, the axiom will still be the same as the conjecture. Consequently all versions resulting from the first family of translations are trivially provable.

The TH0-II version has conjecture

[TABLE]

and the axiom (corresponding to the definition of ${\mathsf{LET}}$)

[TABLE]

The axiom defining ${\mathsf{LET}}$ combined with the basic axiom ${\mathbf{beta}}$ is enough to prove the theorem. However, the TH0-II version also includes all the other basic axioms along with internal versions of the logical constants for universal quantification and equality. The extra axioms make the problem hard for ATP systems, but if only the necessary axioms are provided the problem is easy. In TF0-II and FOF-II the conjecture is the same as in the TH0-II version, but the definition of ${\mathsf{LET}}$ is split into two functions declared when lambda lifting:

[TABLE]

[TABLE]

and

[TABLE]

All the first-order versions of this problem are easy for current ATP systems.

7 Results

Since the HOL4 library has a natural order of the problems, each translation can generate two versions of each problem. The bushy (small) version contains only the (translated) library facts that were needed for the HOL4 proof of the theorem. The chainy (large) version contains all the facts that precede the theorem in the library order, i.e., the real task faced by hammer systems. Chainy problems typically include thousands of axioms, requiring the use of premise selection algorithms [1] as a front-end in the ATP systems. Thus, in order to maintain the focus on ATP system performance, the results of running the ATP systems on the bushy problems are presented here.

Nineteen ATPs were run on the 12140 problems in each of the bushy problem sets, according to the ATPs’ support for the various TPTP formats. In each case we ran the ATP with a CPU time limit of 60s per problem. Table 2 summarizes the results. In union, more proofs were found in the first family of translations than in the second family, in all formats. However, some provers like Vampire 4.3 and SPASS 3.9 do better on FOF-II than on FOF-I. This indicates that these provers are probably better at reasoning with type guards than with type tags. Of the 12140 problems 7412 (61.1%) were solved by some ATP in one of the representations.

The TacticToe [17, 18] prover built into HOL4 has been tested as a baseline comparison, and it (re)proves 5327 of 8855 chainy versions of the problems (60.2%). TacticToe is a machine-learning guided prover that searches for a tactical proof by selecting suitable tactics and theorems learned from human-written tactical proofs. By design, this system works in the chainy setting. In total 8840 (72.8%) of the 12140 problems can be proved by either TacticToe or one of the ATPs using one of the translations.

8 GRUNGE as CASC LTB Division

The CADE ATP System Competition (CASC) [45] is the annual evaluation of fully automatic, classical logic Automated Theorem Proving (ATP) systems – the world championship for such systems. CASC is divided into divisions according to problem and system characteristics. Each competition division uses problems that have certain logical, language, and syntactic characteristics, so that the systems that compete in the division are, in principle, able to attempt all the problems in the division. For example, the First-Order Form (FOF) division uses problems in full first-order logic, with each problem having axioms and a conjecture to be proved.

While most of the CASC divisions present the problems to the ATP systems one at a time, with an individual CPU or wall clock time limit per problem, the Large Theory Batch (LTB) division presents the problems in batches, with an overall wall clock time limit on the batch. As the name also suggests, the problems in each batch come from a “large theory”, which typically has many functors and predicates, and many axioms of which only a few are required for the proof of a theorem. The problems in a batch typically have a common core set of axioms used by all problems, and each problem typically has additional axioms that are specific to the problem. The batch presentation allows the ATP systems to load and preprocess the common core set of axioms just once, and to share logical and control results between proof searches. Each batch is accompanied by a set of training problems and their solutions, taken from the same source as the competition problems. The training data can be used for ATP system tuning and learning during (typically at the start of) the competition.

In CASC-J9 [48] – the most recent edition of the competition – the LTB division used FOF problems exported from CakeML [31]. At the time there was growing interest in an LTB division for typed higher-order problems, and it became evident that a multi-format LTB division would add a valuable dimension to CASC. For the CASC-27 LTB division each problem was presented in multiple formats: TH1, TH0, TF1, TF0, and FOF. The work described in this paper provides the problems. Systems were able to attempt whichever versions they support, and a solution to any version constitutes a solution to the problem. For example, Leo-III is able to handle all the formats, while E can attempt only the

tffzero and FOF formats.

The batch presentation of problems in the LTB division provides interesting opportunities for ATP systems, including making multiple attempts on problems and learning search heuristics from proofs found. The multi-format LTB division extends these possibilities by allowing multiple attempts on problems by virtue of the multiple formats available, and learning from proofs found in one format to improve performance on problems in another format. The latter is especially interesting, with little known research in this direction.

9 Related Work

The HOL4 library already has translations for SMT solvers such as Yices [49], Z3 [9] and Beagle. A link to first-order ATPs is also available thanks to exports [16] of HOL4 theories to the HOL(y)Hammer framework [27]. Another notable project that facilitates the export of HOL4 theories is Open Theory [25]. The general approach for higher-order to first-order translations is laid out in Hurd [23]. An evaluation of the effect of different translations on ATP-provability was performed in [35]. A further study shows the potential improvements provided by the use of supercombinators [14]. In our work, the use of lambda-lifting (or combinators) is not necessary in TH0-II thanks to the use of the higher-order operator $\mathsf{lam}$. This is similar to using higher-order abstract syntax to model syntax with binders [37].

A method for encoding of polymorphic types as terms through type tags (as in our first translation) or type guards (as in our second translation) is described in [6]. Translations [21, 44] from a polymorphic logic to a monomorphic poly-sorted logic without encoding typically rely on heuristic instantiations of type variables. However, heuristics may miss useful instantiations, and make the translation less modular (i.e., context dependent). Our translations to TH0 and TF0 try to get the best of both worlds by using a type encoding for polymorphic types and special types for basic monomorphic types.

10 Conclusion

This work has defined, compared, and evaluated ATP performance on two families of translations of the HOL4 logic to a number of ATP formalisms, and described a new unified large-theory ATP benchmark (GRUNGE) based on them. The first family is designed to play to the strengths of the calculi of most ATP systems, while the second family is based on more straightforward semantics rooted in set theory. The case study shows how different the translated problems may be, even in a simple example. A number of methods and optimizations have been used, however it is clear that the translations can be further optimized and that different encodings favour different provers. Out of 12140 HOL4 theorems, the ATP systems can solve 7412 problems in one or more of the formats. The TacticToe system that works directly in the HOL4 formalism and uses HOL4 tactics could solve 5327 problems. Together the total number of problems solved is 8840. Leo-III was the strongest system in the higher-order representations. In the first-order representations the strongest systems were Zipperposition, CVC4, E and Vampire. A pre-release of the bushy versions of the problems was provided before CASC-27222http://www.tptp.org/CASC/27/TrainingData.HL4.tgz, to allow system developers to adapt and tune their systems before the competition.