We present a pragmatic approach to extending a Boolean-free higher-order superposition calculus to support Boolean reasoning. Our approach extends inference rules that have been used only in a firstorder setting, uses some well-known rules previously implemented in higher-order provers, as well as new rules. We have implemented the approach in the Zipperposition theorem prover. The evaluation shows highly competitive performance of our approach and clear improvement over previous techniques.
To fully bridge the gap between higher-order and first-order tools, we combine the two
approaches: we use the eficient higher-order superposition calculus and extend it with inference
rules that reason with Boolean terms. In early work, Kotelnikov et al. [
The backbone of our approach is based on an extension of this rule to higher-order logic. Namely, we do not translate away any Boolean structure that is nested inside non-Boolean terms and allow our rule to hoist the nested Booleans to the literal level. Then, we clausify the resulting formula (i.e., a clause that contains formulas in literals) using a new rule.
An important feature that we inherit by building on top of Bentkamp et al. [
Rules that extend the two orthogonal approaches form the basis of our support for Boolean
reasoning (Section 3). In addition, we have implemented rules that are inspired by the ones
used in the higher-order provers Leo-III [
We compare our native approach with two alternatives based on preprocessing (Section 4).
First, we compare it to an axiomatization of the theory of Booleans. Second, inspired by work
of Kotelnikov et al. [
Our approach is implemented in the Zipperposition theorem prover [
We performed an extensive evaluation of our approach (Section 6). In addition to evaluating diferent configurations of our new rules, we have compared them to full higher-order provers CVC4, Leo-III, Satallax and Vampire. The results suggest that it is beneficial to natively support Boolean reasoning – the approach outperforms preprocessing-based approaches. Furthermore, it is very competitive with state-of-the-art higher order provers. We discuss the diferences between our approach and the approaches we base on, as well as related approaches (Section 7).
We base our work on Bentkamp et al.’s [
A signature is a quadruple pΣty, Vty, Σ, Vq where Σty is a set of type constructors, Vty is a set of type variables and Σ and V are sets of constants and term variables, respectively. We require nullary type constructors and , as well as binary constructor Ñ to be in Σty. A type , is either a type variable P Vty or of the form p 1, . . . q where is an -ary type constructor. We write for pq, Ñ for Ñ p, q, and we abbreviate tuples p1, . . . , q as for ě 0. Similarly, we drop parentheses to shorten 1 Ñ p¨ ¨ ¨ Ñ p ´1 Ñ q ¨ ¨ ¨ q into 1 Ñ ¨ ¨ ¨ Ñ . Each symbol in Σ is assigned a type declaration of the form Π . where all variables occurring in are among .
Function symbols a, b, f, g, . . . are elements of Σ; their type declarations are written as f : Π . . Term variables from the set V are written , , . . . and we denote their types as : . When the type is not important, we omit type declarations. We assume that symbols J, K, ␣, ^, _, ñ, ô with their standard meanings and type declarations are elements of Σ. Furthermore, we assume that polymorphic symbols @ and D with type declarations Π. p Ñ q Ñ and « : Π. Ñ Ñ are in Σ, with their standard meanings. All these symbols are called logical symbols. We write binary logical symbols in infix notation.
Terms are defined inductively as follows. Variables : are terms of type . If f : Π .
is in Σ and is a tuple of types, called type arguments, then fx y (written as f if “ 0, or if
type arguments can be inferred from the context) is a term of type t ÞÑ u, called constant.
If is a variable of type and is a term of type then . is a term of type Ñ . If and
are of type Ñ and , respectively, then is a term of type . We call terms of Boolean type
() formulas and denote them by , , ℎ, . . .; we use , , , . . . for variables whose result type
is and p, q, r for constants with the same result type. We shorten iterated lambda abstraction
1. . . . . to . , and iterated application p 1q ¨ ¨ ¨ to . We assume the standard
notion of free and bound variables, capture-avoiding substitutions , , , . . . , and -, -,
conversion. Unless stated otherwise, we view terms as -equivalence classes, with -long
-reduced form as the representative. Each term can be uniquely written as . where
is either variable or constant and , ě 0; we call the head of . We say that a term is
written in spine notation [
Given a formula we call its Boolean subterm | a top-level Boolean if for all proper prefixes of , the head of | is a logical constant. Otherwise, we call it a nested Boolean. For example, in the formula “ h a « g pp ñ qq _ ␣p, |1 and |2 are top-level Booleans, whereas |1.2.1 is a nested Boolean (as well as its subterms). Only top-level Booleans are allowed in first-order logic, whereas nested Booleans are characteristic for higher-order logic. A formula is called an atom if it is of the form , where is a non-logical head, or of the form « , where if or are of type , and one of them has a logical head, the other one must be J or K. A literal is an atom or its negation. A clause is a multiset of literals, interpreted and written (abusing _) disjunctively as 1 _ ¨ ¨ ¨ _ . We write ff for ␣p « q. We say a variable is free in a clause if it is not bound inside any subterm of a literal in .
Some support for Booleans was already present in Zipperposition before we started extending the
calculus of Bentkamp et al. In this section, we start by describing the internals of Zipperposition
responsible for reasoning with Booleans. We continue by describing 15 rules that we have
implemented. For ease of presentation we divide them in three categories. We assume some
familiarity with the superposition calculus [
Zipperposition is an open source1 prover written in OCaml. From its inception, it was designed
as a prover that supports easy extension of its base superposition calculus to various theories,
including arithmetic, induction and limited support for higher-order logic [
Zipperposition internally stores applications in flattened, spine notation. It also exploits associativity of ^ and _ to flatten nested applications of these symbols. Thus, the terms p ^ pq ^ rq and pp ^ qq ^ r are represented as ^ p q r. The prover’s support for -terms is used to represent quantified nested Booleans: formulas @. and D. are represented as @ p. q and D p. q. After clausification of the input problem, no nested Booleans will be modified or renamed using fresh predicate symbols.
The version of Zipperposition preceding our modifications distinguished between equational
and non-equational literals. Following E [
Kotelnikov et al. [
r s rJs _ « K
FP
We created two rules that are syntactically similar to FP but are adapted for higher-order logic with one key distinction – we do not perform any translation: The double line in the definition of CasesSimp denotes that the premise is replaced by conclusions; obviously, the prover that uses the rules should not include them both at the same time. In addition, since literals « K are represented as negative equations ff J, which cannot be used to paramodulate from, we change the first requirement on the order to K ą J.
These two rules hoist Boolean subterms to the literal level; therefore, some results of Cases and CasesSimp will have literals of the form « J (or ff J) where is not an atom. This introduces the need for the rule called eager clausification ( EC):
1 ¨ ¨ ¨
EC We say that a clause is standard if all of its literals are of the form «. , where and are not Booleans or of the form «. J, where the head of is not a logical symbol and «. denotes « or ff. The rule EC is applicable if clause “ 1 _ ¨ ¨ ¨ _ is not standard. The resulting clauses represent the result of clausification of the formula @. 1 _ ¨ ¨ ¨ _ where are all free variables of .
An advantage of leaving nested Booleans unmodified is that the prover will be able to prove some problems containing them without using the prolific rules described above. For example, given two clauses f pp ñ p q « a and f pp a ñ p bq ff a, the empty clause can easily be derived without the above rules. A disadvantage of this approach is that the proving process will periodically be interrupted by expensive calls to the clausification algorithm.
Naive application of Cases and CasesSimp rules can result in many redundant clauses. Consider a clause “ p pp pp pp aqqq « J where p : Ñ , a : . Then, the clause “ a « J _ p K « J can be derived from in eight ways using the rules, depending on which nested Boolean subterm was chosen for the inference. In general, if a clause has a subterm occurrence of the form p a, where both p and a have result type , the clause a « J _ p K « J can be derived in 2´1 ways. To combat these issues we implemented pragmatic restrictions of the rule: only the leftmost outermost (or innermost) eligible subterm will be considered. With this modification can be derived in only one way. Furthermore, some intermediate conclusions of the rules will not be derived, pruning the search space.
The clausification algorithm by Nonnengart and Weidenbach [
Our decision to represent negative atoms as negative equations was motivated by the need to alter Zipperposition’s earlier behavior as little as possible. Namely, negative atoms were not used as literals that can be used to paramodulate from, and as such added to the laziness of the superposition calculus. However, it might be useful to consider unit clauses of the form ff J as « K to strengthen demodulation. To that end, we have introduced the following rule: ff J ff J
To achieve refutational completeness of higher-order resolution and similar calculi it is necessary
to instantiate variables with result type , predicate variables, with arbitrary formulas [
. p _ . « qt ÞÑ u
PI
where is a free variable of the type 1 Ñ ¨ ¨ ¨ Ñ Ñ . Choosing a diferent that
instantiates , we can balance between explosiveness of approximating a complete set of logical
symbols and incompleteness of pragmatic approaches. We borrow the notion of imitation
from higher-order unification jargon [
Rule PI was already implemented by Simon Cruanes in Zipperposition, before we started our modifications. The rule has diferent modes that generate sets of possible terms for : 1 Ñ ¨ ¨ ¨ Ñ Ñ : Full, Pragmatic, and Imit‹ where ‹ is an element of a set of logical constants “ t^, _, «x y, ␣, @, Du. Mode Full contains imitations (for ) of all elements of . Mode Pragmatic contains imitations of ␣, J and K; if there exist indices , such that ‰ and “ , it contains . « ; if there exist indices , such that ‰ , and “ “ , then it contains . ^ and . _ ; if for some , “ , then it contains . . Mode Imit‹ contains imitations of J, K and ‹ (except for Imit@D which contains imitations of both @ and D).
While experimenting with our implementation we have noticed some proof patterns that led us to come up with the following modifications. First, it often sufices to perform PI only on initial clauses – which is why we allow the rule to be applied only to the clauses created using at most generating inferences. Second, if the rule was used in the proof, its premise is usually only used as part of that inference – which is why we implemented a version of PI that removes the clause after all possible PI inferences have been performed. We observed that the mode Imit‹ is useful in practice since often only a single approximation of a logical symbol is necessary.
Eficiently treating axiom of choice is notoriously dificult for higher-order provers. Andrews
Ñ q. pDp : q. q ñ p q, where : Π. p
Ñ q Ñ
denotes the choice operator [
Therefore, Leo-III [
r s p q ff J _ p p p. p qqqq « J
Let be the conclusion of Choice. The fresh variable in acts as arbitrary context around , the chosen instantiation for from axiom of choice; the variable can later be replaced by imitation of logical symbols to create more complex instantiations of the choice axiom. To generate useful instances early, we create t ÞÑ . u and t ÞÑ . ␣u. Then, based on Zipperposition parameters, will either be deleted or kept. Note that will not subsume its instances, since the matching algorithm of Zipperposition is too weak for this.
Most provers natively support extensionality reasoning: Bhayat et al. [
“1 dpp, q. Then the extensionality rules are stated as follows: dpp , q “ tp , qu if and are diferent heads; dpp. , . q “ tp. , . qu; « _
r1s «. _ p1 ff 11 _ ¨ ¨ ¨ _ ff 1 _ rs «. _ _ q
ff 1 _ p1 ff 11 _ ¨ ¨ ¨ _ ff 1 ¨ ¨ ¨ _ q
« _ 1 « _ p1 ff 11 _ ¨ ¨ ¨ _ ff 1 _ ff _ 1 « _ q
Rules ExtSup, ExtER, and ExtEF are extensional versions of superposition, equality resolution
and equality factoring [
Consider the clause f p␣p _ ␣qq ff f p␣pp ^ qqq. This problem is obviously unsatisfiable, since arguments of f on diferent sides of the disequation are extensionally equal; however, without Ext rules Zipperposition will rely on Cases(Simp) and EC rules to derive the empty clause. Rule ExtER will generate “ ␣p _ ␣q ff ␣pp ^ qq. Then, will get clausified using EC, efectively reducing the problem to ␣p␣p _ ␣q ô ␣pp ^ qqq, which is first-order.
Zipperposition restricts ExtSup by requiring that and 1 are not of function or Boolean
types. If the terms are of function type, our experience is that better treatment of function
extensionality is to apply fresh free variables (or Skolem terms, depending on the sign [
Expressiveness of higher-order logic allows users to define equality using a single axiom,
called Leibniz equality [
Before we began our modifications, Zipperposition had a powerful rule that recognizes clauses that contain variations of Leibniz equality and instantiates them with native equality. This rule was designed by Simon Cruanes, and to the best of our knowledge, it has not been documented so far. With his permission we describe this rule as follows: 1 « J _ ¨ ¨ ¨ _ « J _ 1 ff J _ ¨ ¨ ¨ _ ff J _ p 1 « J _ ¨ ¨ ¨ _ « J _ q
where is a free variable, does not occur in any or , or in , and is defined as t ÞÑ . Ž“1pŹ“1 « qu.
To better understand how this rule removes variable-headed negative literals, consider the clause “ a1 a2 « J _ b1 b2 ff J _ c1 c2 ff J. Since all side conditions are fulfilled, the rule ElimPredVar will generate “ t ÞÑ . p « b1 ^ « b2q _ p « c1 ^ « c2qu. After applying to and subsequent -reduction, negative literal b1 b2 ff J will reduce to pb1 « b1 ^ b2 « b2q _ pb1 « c1 ^ b2 « c2q ff J, which is equivalent to K. Thus, we can remove this literal and all negative literals of the form ff J from and apply to the remaining ones.
The previous rule removes all variables occurring in disequations in one attempt. We implemented two rules that behave more lazily, inspired by the ones present in Leo-III and Satallax: « J _ ff J _ p « _ q
ElimLeibniz` ff J _ « J _ p « _ q 1
ElimLeibniz´ where is a free variable, does not occur in , “ t ÞÑ . « u and 1 “ t ÞÑ . ␣p « qu. This rule difers from ElimPredVar in three ways. First, it acts on occurrences of variables in both positive and negative literals. Second, due to its simplicity, it usually does not require EC as the following step. Third, it imposes much weaker conditions on . However, removing all negative variables in one step might improve performance. Coming back to example of the clause “ a1 a2 « J _ b1 b2 ff J _ c1 c2 ff J, we can apply ElimLeibniz` using the substitution “ t. « b1u to obtain the clause 1 “ a1 « b1 _ a1 ff c1.
Zipperposition’s unification algorithm [
The winner of THF division of CASC-27 [
ff J _ 1 « J _ p « ␣1 _ q
BoolEF´` « J _ 1 ff J _
p « ␣1 _ q ff J _ 1 ff J _ p « 1 _ q
BoolEF`´ BoolEF´´ All side conditions except for the ones concerning the unifiability of terms are as in the original equality resolution and equality factoring rules. In rule BoolER, unifies and ␣1. In the `´ and ´` versions of BoolEF, unifies and ␣1, and in the remaining version it unifies and 1. Intuitively, these rules bring Boolean (dis)equations in the appropriate form for application of the corresponding base rules. It sufices to consider literals of the form « 1 for BoolER since Zipperposition rewrites ô « J and ␣p ô q ff J to « (and does analogous rewriting into ff ).
Another approach to mitigate harmful efects of eager clausification is to delay it as long
as possible. Following the approach by Ganzinger and Stuber [
LC^
p _ q « J _ « J _ « J _
LC_
p ñ q « J _ ff J _ « J _
LCñ p␣ q « J _ ff J _
LC␣ t ÞÑ u _ « _
LCD
LC«
ff J _ « J _ « J _ ff J _
The rules described above are as given by Ganzinger and Stuber (adapted to our setting), with
the omission of rules for negative literals ( ff J), which are easy to derive and which can be
found in their work [
Naive application of the LC rules can result in exponential blowup in problem size. To avoid this, we rename formulas that have repeated occurrences. We keep the count of all non-atomic . formulas occurring as either side of a literal. Before applying the LC rule on a clause « J _ , we check whether the number of ’s occurrences exceeds the threshold . If it does, based on . the polarity of the literal « J, we add the clause p ff J _ « J (if the literal is positive) or p « J _ ff J (if the literal is negative), where are all free variables of and p is . . a fresh symbol. Then, we replace the clause « J _ by p « J _ .
Before the number of occurrences of is checked, we first check (using a fast, incomplete matching algorithm) if there is a formula , for which definition was already introduced, such that “ , for some substitution . This check can have three outcomes. First, if the definition q is already introduced for with the polarity matching that of «. J, then is replaced by pq q . Second, if the definition was introduced, but with diferent polarity, we create the clause defining with the missing polarity, and replace with pq q . Last, if the there is no renamed formula generalizing , then we perform the previously described check.
In addition to reusing names for formula definitions, we reuse the Skolem symbols introduced
by the LCD rule. When LCD is applied to “ D. 1 we check if there is a Skolem skx y
introduced for a formula “ D. 1, such that “ . If so, the symbol sk is reused and D. 1
is replaced by 1t ÞÑ pskx yq u. Renaming and name reusing techniques are inspired by
the VCNF algorithm described by Reger et al. [
Rules Cases and CasesSimp deal with Boolean terms, but we need to rely on extensionality reasoning to deal with -abstractions whose body has type . Using the observation that the formula @. implies that . is extensionally equal to . J (and similarly, if @. ␣ , then . « . Kq, we designed the following rule (where all free variables of are and variables occurring freely in ):
r . s p@. ␣ q ff J _ r . Ks
An alternative to heavy modifications of the prover needed to support the rules described above is to treat Booleans as yet another theory. Since the theory of Booleans is finitely axiomatizable, simply stating those axioms instead of creating special rules might seem appealing. Another approach is to preprocess nested Booleans by hoisting them to the top level.
A simple axiomatization of the theory of Booleans is given by Bentkamp et al. [
To make this paper self-contained we include the axioms from Bentkamp et al. [
forallx yp. tq « t « p. tq _ forallx y « f
existsx y « not pforallx y p. not p qqq « f _ pchoicex yq « t
Kotelnikov et al. extended VCNF, Vampire’s algorithm for clausification, to support nested
Booleans [
The TPTP library contains thousands of higher-order benchmarks, many of them hand-crafted to point out subtle interferences of functional and Boolean properties of higher order logic. In this section we discuss some problems from the TPTP library that illustrate the advantages and disadvantages of our approach.
In the last five instances of the CASC theorem proving competition, the core calculus of the best performing higher-order prover was tableaux – a striking contrast from first-order part of the competition dominated by superposition-based provers. TPTP problem SET557^1 (a statement of Cantor’s theorem) might shed some light on why tableaux-based provers excel on higher-order problems. This problem conjectures that there is no surjection from a set to its power set:
␣pDp : Ñ Ñ q. @p : Ñ q. Dp : q. « q
After negating the conjecture and clausification this problem becomes sk1 psk2 q « where sk1
and sk2 are Skolem symbols. Then, we can use ArgCong rule [
Combining rule (Bool)ER with lazy clausification is very fruitful as the problem SYO033^1 illustrates. This problem also contains the single conjecture
Dp : p Ñ q Ñ q. @p : Ñ q.p ô p@p : q. qq The problem is easily solved if we instantiate variable with the constant @. Moreover, the prover does not have to blindly guess this instantiation for , but can obtain it by unifying with @ (which is the -short form of @p : q. ). However, when the problem is clausified, all quantifiers are removed. Then, Zipperposition only finds the proof if appropriate instantiation mode of PI is used, and if both clauses resulting from clausifying the negated conjecture are appropriately instantiated. In contrast, lazy clausification will derive the clause psk q ff @ psk q from the negated conjecture in three steps. Then, equality resolution results in an empty clause, swiftly finishing the proof without any explosive inferences. This efect is even more pronounced on problems SYO287^5 and SYO288^5, in which critical proof step is instantiation of a variable with imitation of _ and ^. In configurations that do not use lazy clausification and BoolER, Zipperposition times out in any reasonable time limit; with those two options it solves mentioned problems in less than 100 ms.
In some cases, it is better to preprocess the problem. For example, TPTP problem SYO500^1.005 contains many nested Boolean terms:
f0 pf1 pf1 pf1 pf2 pf3 pf3 pf3 pf4 aqqqqqqq « f0 pf0 pf0 pf1 pf2 pf2 pf2 pf3 pf4 pf4 pf4 aqqqqqqqqqqq In this problem, all functions f are of type Ñ , and constant a is of type . FOOL unfolding of nested Boolean terms will result in exponential blowup in the problem size. However, superposition-based theorem provers are well-equipped for this issue: their CNF algorithms use smart simplifications and formula renaming to mitigate these efects. Moreover, when the problem is preprocessed, the prover is aware of the problem size before the proving process starts and can adjust its heuristics properly. E, Zipperposition and Vampire, instructed to perform FOOL unfolding, solve the problem swiftly, using their default modes. However, if problem is not preprocessed, Zipperposition struggles to prove it using Cases(Simp) and due to the large number of (redundant) clauses it creates, succeeds only if specific heuristic choices are made.
We performed extensive evaluation to determine usefulness of our approach. As our benchmark
set, we used all 2606 monomorphic theorems from the TPTP library, given in THF format.
All of the experiments were performed on StarExec [
For this part of the evaluation, we fixed a single well-performing Zipperposition configuration
called base (b). Since we are testing a single configuration, we used the CPU time limit of 15 s
– roughly the time a single configuration is given in a portfolio mode. Configuration b uses the
pragmatic variant pv21121 of the unification algorithm given by Vukmirović et al. [
First, we tested diferent parameters of Cases and CasesSimp rules. In Figure 1 we report the results. The columns correspond to three possible options to choose subterm on which the inference is performed: a stands for any eligible subterm, lo and li stands for leftmost outermost and leftmost innermost subterms, respectively. The rows correspond to two diferent rules: b is the base configuration, which uses CasesSimp, and bc swaps this rule for Cases. Although the margin is slim, the results show it is usually preferable to select leftmost-outermost subterm. b bc
a
Second, we evaluated all the modes of PI rule with 3 values for parameter : 1, 2, and 8 (Figure 2). The columns denote, from left to right: disabling the PI rule, Pragmatic mode, Full mode, and Imit‹ modes with appropriate logical symbols. The rows denote diferent values of . The results show that diferent values for have a modest efect on success rate. The raw data reveal that when we focus our attention to configurations with “ 2, mode Full can solve 10 problems no other mode (including disabling PI rule) can. Modes Imit^ and Pragmatic solve 2 problems, whereas Imit_ solves one problem uniquely. This result suggests that, even though this is not evident from Figure 2, sets of problems solved solved by diferent modes somewhat difer.
Figure 3 gives results of evaluating rules that treat Leibniz equality on the calculus level: EL stands for ElimLeibniz, whereas EPV denotes ElimPredVar; signs ´ and ` denote that rule is removed from or added to configuration b, respectively. Disabling both rules severely lowers the success rate. The results suggest that including ElimLeibniz is beneficial to performance.
Similarly, Figure 4 discusses merits of including (`) or excluding (´) BoolER (BER) and BoolEF (BEF) rules. Our expectations were that inclusion of those two rules would make bigger impact on success rate. It turned out that, in practice, most of the efects of these rules could be achieved using a combination of the PI rule and basic superposition calculus rules.
Combining these two rules with lazy clausification is more useful: when the rule EC is replaced by the rule LC, the success rate increases (compared to 1646 problems solved by ) to 1660 problems. We also discovered that reasoning with choice is useful: when rule Choice is enabled, the success rate increases to 1653. We determined that including or excluding the conclusion of Choice, after it is simplified, makes no diference. Counterintuitively, disabling BoolSimp rule results in 1640 problems, which is only 6 problems short of configuration . Disabling Ext and Interpret- rules results in solving 25 and 31 problems less, respectively. Raw data show pure coop
CVC4 that in total, using configurations from Figure 1 to Figure 4, 1682 problems can be solved.
Last, we compare our approach to alternatives. Axiomatizing Booleans brings Zipperposition down to a grinding halt: only 1106 problems can be solved using this mode. On the other hand, preprocessing is fairly competitive: it solves only 8 problems less than the configuration.
We compared Zipperposition with all higher-order theorem provers that took part in THF
division of CASC-27[
Leo-III and Satallax are cooperative theorem provers – they periodically invoke first-order
provers to finish the proof attempt. Leo-III uses CVC4, E and iProver [
In both pure and cooperative mode, Satallax comes out as the winner. Zipperposition comes in close second, showing that our approach is a promising basis for further extensions. LeoIII uses SMT solver CVC4, which features native support for Booleans, as a backend. It is possible that the use of CVC4 is one of the reasons for massive improvement in success rate of cooperative configuration of Leo-III, compared with the pure version. Therefore, we conjecture that including support for SMT backends in Zipperposition might be beneficial.
Our work is primarily motivated by the goal of closing the gap between higher-order “hammer”
or software verifier frontends and first-order backends. Considerable amount of research efort
has gone into making the translations of higher-order logic as eficient as possible. Descriptions
of hammers like HOLyHammer [
Established higher-order provers like Leo-III and Satallax perform very well on TPTP benchmarks;
however, recent evaluations show that on Sledgehammer problems they are outperformed by
translations to first-order logic [
In contrast, our approach is to start with a first-order prover and gradually extend it with
higher-order features. The work performed in the context of Matryoshka project [
The main merit of our approach is that it combines two successful complementary approaches
to support features of higher-order logic that have not been combined before in a modular
way. It is based on a higher-order superposition calculus that incurs around 1% of overhead
on first-order problems compared with classic superposition [
We presented a pragmatic approach to support Booleans in a modern automatic prover for clausal higher-order logic. Our approach combines previous research eforts that extended ifrst-order provers with complementary features of higher-order logic. It also proposes some solutions for the issues that emerge with this combination. The implementation shows clear improvement over previous techniques and competitive performance.
What our work misses is an overview of heuristics that can be used to curb the explosion
incurred by some of the rules described in this paper. In future work, we plan to address this
issue. Similarly, unlike Bentkamp et al. [
Acknowledgment We are grateful to the maintainers of StarExec for letting us use their service. We thank Alexander Bentkamp, Jasmin Blanchette and Simon Cruanes for many stimulating discussions and all the useful advice. Alexander Bentkamp suggested the rule BoolER. We are also thankful to Ahmed Bhayat, Predrag Janičić and the anonymous reviewers for suggesting many improvements to this paper. We thank Evgeny Kotelnikov for patiently explaining the details of FOOL, Alexander Steen for clarifying Leo-III’s treatment of Booleans, and Giles Reger and Martin Suda for explaining the renaming mechanism implemented in VCNF. Vukmirović’s research has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No. 713999, Matryoshka). Nummelin has received funding from the Netherlands Organization for Scientific Research (NWO) under the Vidi program (project No. 016.Vidi.189.037, Lean Forward).