=Paper=
{{Paper
|id=Vol-2752/paper11
|storemode=property
|title=Boolean Reasoning in a Higher-Order Superposition Prover
|pdfUrl=https://ceur-ws.org/Vol-2752/paper11.pdf
|volume=Vol-2752
|authors=Petar VukmiroviΔ,Visa Nummelin
|dblpUrl=https://dblp.org/rec/conf/cade/VukmirovicN20
}}
==Boolean Reasoning in a Higher-Order Superposition Prover==
https://ceur-ws.org/Vol-2752/paper11.pdf
Boolean Reasoning in a Higher-Order Superposition
Prover
Petar VukmiroviΔa , Visa Nummelina
a
Vrije Universiteit Amsterdam, De Boelelaan 1105, 1081 HV Amsterdam, The Netherlands
Abstract
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 first-
order 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.
Keywords
higher-order logic, theorem proving, superposition
1. Introduction
In the last decades, automatic theorem provers have been used successfully as backends to
βhammersβ in proof assistants [1, 2] and to software verifiers [3]. Most advanced provers, such as
CVC4 [4], E [5], and Vampire [6], are based on first-order logic, whereas most frontends that use
them are based on versions of higher-order logic. Thus, there is a large gap in expressiveness
between front- and backends. This gap is bridged using well-known translations from higher-
order to first-order logic [7, 8]. However, translations are usually less efficient than native
support [9, 10, 11]. The distinguishing features of higher-order logic used by proof assistants
that the translation must eliminate include π-binders, function extensionality β the property that
functions are equal if they agree on every argument, described by the axiom @pπ₯, π¦ : π Γ πq.
p@pπ§ : π q. π₯ π§ Β« π¦ π§q Γ± π₯ Β« π¦, and formulas occurring as arguments of function symbols [8].
A group of authors including VukmiroviΔ [10] recently designed a complete calculus for
extensional Boolean-free higher-order logic. This calculus is an extension of superposition,
the calculus used in most successful provers such as E or Vampire. The extension removes the
need to translate the first two above mentioned features of higher-order logic. Kotelnikov et al.
[12, 13] extended the language of first-order logic to support the third feature of higher-order
logic that requires translation. They described two approaches: one based on calculus-level
treatment of Booleans and the other, which requires no changes to the calculus, based on
preprocessing.
PAAR 2020: Seventh Workshop on Practical Aspects of Automated Reasoning, June 29β30, 2020, Paris, France (virtual)
p.vukmirovic@vu.nl (P. VukmiroviΔ); visa.nummelin@vu.nl (V. Nummelin)
{ https://petarvukmirovic.github.io/home/ (P. VukmiroviΔ)
0000-0001-7049-6847 (P. VukmiroviΔ); 0000-0003-0078-790X (V. Nummelin)
Β© 2020 Copyright for this paper by its authors.
Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
148
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
To fully bridge the gap between higher-order and first-order tools, we combine the two
approaches: we use the efficient higher-order superposition calculus and extend it with inference
rules that reason with Boolean terms. In early work, Kotelnikov et al. [12] have described a
FOOL paramodulation rule that, under some order requirements, removes the need for the axiom
describing the Boolean domain β @pπ : πq. π Β« J _ π Β« K. In this approach, it is assumed that
a problem with formulas occurring as arguments of symbols is translated to first-order logic.
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. [10] is support
for (function) extensionality. Moving to higher-order logic with Booleans also means that we
need to consider Boolean extensionality: @pπ : πqpπ : πq. pπ Γ΄ πq Γ± π Β« π. We extend the rules
of Bentkamp et al. that treat function extensionality to support Boolean extensionality as well.
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 [14] and Satallax [15], such as elimination of Leibniz
equality, primitive instantiation and treatment of choice operator [16]. We have also designed
new rules that use higher-order unification to resolve Boolean formulas that are hoisted to literal
level, delay clausification of non-atomic literals, reason about formulas under π-binders, and
many others. Even though the rules we use are inspired by the ones of refutationally complete
higher-order provers, we do not guarantee completeness of our extension of π-superposition.
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. [13], we implemented the preprocessing approach that does not require
introduction of Boolean axioms. We also discuss some examples, coming from TPTP [17], that
illustrate advantages and disadvantages of our approach (Section 5).
Our approach is implemented in the Zipperposition theorem prover [18, 19]. Zipperposition
is an easily extensible open source prover that Bentkamp et al. used to implement their higher-
order superposition calculus. We further extend their implementation.
We performed an extensive evaluation of our approach (Section 6). In addition to evaluating
different 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 differences
between our approach and the approaches we base on, as well as related approaches (Section 7).
2. Background
We base our work on Bentkamp et al.βs [10] extensional polymorphic clausal higher-order logic.
We extend the syntax of this logic by adding logical connectives to the language of terms. The
semantic of the logic is extended by interpreting Boolean type π as a two-element domain. This
amounts to extending Bentkamp et alβs fragment of higher-order logic to full-higher order logic
149
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
(HOL). Our notation, definitions and the following text are largely based 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 pπ1 , . . . , ππ 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π π‘1 q Β¨ Β¨ Β¨ π‘π 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 [20]. Following our previous work [21], we define nonstandard notion
of subterms and positions inductively as a graceful extension of the first-order counterparts: a
term π is a subterm of itself at position π. If π is a subterm of π‘π at position π then π is a subterm
of π π‘π at position π.π, where π is a head. If π is a subterm of π‘ at position π then π is a subterm
of ππ₯. π‘ at position 1.π. We use π |π to denote subterm of π at position π.
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 πΆ.
150
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
3. The Native Approach
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 [22] and adopt the notation used by Schulz [23].
3.1. Support for Booleans in Zipperposition
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 [18].
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 [5], we modified Zipperposition to represent all literals
equationally: a non-equational literal π is stored as π Β« J, whereas β£π is stored as π ff J.
Equations of the form π Β« K and π ff K are transformed into π ff J and π Β« J, respectively.
3.2. Core Rules
Kotelnikov et al. [12], to the best of our knowledge, pioneered the approach of extending a
first-order superposition prover to support nested Booleans. They call effects of including the
axiom @pπ : πq. π Β« J _ π Β« K a βrecipe for disasterβ. To combat the explosive behavior of
the axiom, they imposed the following two requirements to the simplification order Δ
(which
is a parameter to the superposition calculus): J Δ
K and J and K are two smallest ground
terms with respect to Δ
. If these two requirements are met, there is no self-paramodulation
of the clause and only paramodulation possible is from literal π Β« J of the mentioned axiom
into a Boolean subterm of another clause. Finally, Kotelnikov et al. replace the axiom with the
inference rule FOOL Paramodulation (FP):
πΆrπ s
FP
πΆrJs _ π Β« K
where π is a nested non-variable Boolean subterm of clause πΆ, different from J and K. In
addition, they translate the initial problem containing nested Booleans to first-order logic
without interpreted Booleans; this translation introduces proxy symbols for J and K, and proxy
type for π.
1
https://github.com/sneeuwballen/zipperposition
151
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
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:
πΆrπ s πΆrπ s
Cases CasesSimp
πΆrKs _ π Β« J πΆrKs _ π Β« J πΆrJs _ π ff J
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):
πΆ
EC
π·1 Β¨ Β¨ Β¨ π·π
.
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 [24] aggressively simplifies the
input problem using well-known Boolean equivalences before clausifying it. For example, the
formula p ^ J will be replaced by p. To simplify nested Booleans we implemented the rule
πΆrπ πs
BoolSimp
πΆrππs
where π ΓΓ π P πΈ runs over fixed set of rewrite rules πΈ, and π is any substitution. In the
current implementation of Zipperposition, πΈ consists of the rules described by Nonnengart
152
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
and Weidenbach [24, Section 3]. This set contains the rules describing how each logical symbol
behaves when either of its argument is J or K: for example, it includes J Γ± π ΓΓ π and
π Γ± J ΓΓ J. Leo-III implements a similar rule, called simp [25, Section 4.2.1.].
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 πΆrπ πs
BoolDemod
π ff J πΆrKs
3.3. Higher-Order Considerations
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 [25, 16].
Fortunately, we can approximate the formulas using a complete set of logical symbols (e.g., β£,
@, and ^). Since such an approximation is not only necessary for completeness of some calculi,
but very useful in practice, we implemented the primitive instantiation (PI) rule:
.
πΆ _ ππ₯π . π π π Β« π‘
. PI
pπΆ _ ππ₯π . π π π Β« π‘qtπ ΓΓ π u
where π is a free variable of the type π1 Γ Β¨ Β¨ Β¨ Γ ππ Γ π. Choosing a different π 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 [21]: we say that the term ππ₯π . f pπ¦1 π₯π q Β¨ Β¨ Β¨ pπ¦π π₯π q is an
imitation of constant f : π1 Γ Β¨ Β¨ Β¨ Γ ππ Γ π for some variable π§ of type π1 Γ Β¨ Β¨ Β¨ Γ ππ Γ π .
Variables π¦ π are fresh free variables, where each π¦π has the type π1 Γ Β¨ Β¨ Β¨ Γ ππ Γ ππ ; variable
π₯π is of type ππ .
Rule PI was already implemented by Simon Cruanes in Zipperposition, before we started our
modifications. The rule has different 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 suffices 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
153
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
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.
Efficiently treating axiom of choice is notoriously difficult for higher-order provers. Andrews
formulates this axiom as @pπ : πΌ Γ πq. pDpπ₯ : πΌq. π π₯q Γ± π pπ πq, where π : Ξ πΌ. pπΌ Γ πq Γ πΌ
denotes the choice operator [16]. After clausification, this axiom becomes π π₯ ff J _ π pπ πq Β« J.
Since term π π₯ matches any Boolean term in the proof state, this axiom is very explosive.
Therefore, Leo-III [14] deals with the choice operator on the calculus level. Namely, whenever a
clause πΆ β π π₯ ff J _ π pf πq Β« J is chosen for processing, πΆ is removed from the proof state
and f is added to set of choice functions CF (which initially contains just π). Later, elements
of CF will be used to heuristically instantiate the axiom of choice. We reused the method of
recognizing choice functions, but generalized the rule for creating the instance of the axiom
(assuming π P CF ):
πΆrπ π‘s
Choice
π₯ 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. [26] modify first-order
unification to return unification constraints consisting of pairs of terms of functional type,
whereas Steen relies on the unification rules of Leo-IIIβs calculus [25, Section 4.3.3.] to deal with
extensionality. Bentkamp et al [10] altered core generating inference rules of the superposition
calculus to support extensionality. Instead of requiring that terms involved in the inference
are unifiable, it is required that they can be decomposed into disagreement pairs such that at
least one of the disagreement pairs is of functional type. Disagreement pairs of terms π and
π‘ of the same type are defined inductively using function dp: dppπ , π‘q β H if π and π‘ are equal;
dppπ π π , π π‘π q β Ε€
tpπ π π , π π‘π qu if π and π are different heads; dppππ₯. π , ππ¦. π‘q β tpππ₯. π , ππ¦. π‘qu;
dppπ π π , π π‘π q β ππβ1 dppπ π , π‘π q. Then the extensionality rules are stated as follows:
.
π Β«π‘_πΆ π’rπ 1 s Β« π£ _ π·
. ExtSup
pπ 1 ff π 11 _ Β¨ Β¨ Β¨ _ π π ff π 1π _ π’rπ‘s Β« π£ _ πΆ _ π·qπ
π ff π 1 _ πΆ
ExtER
pπ 1 ff π 11 _ Β¨ Β¨ Β¨ _ π π ff π 1π Β¨ Β¨ Β¨ _ πΆqπ
π Β« π‘ _ π 1 Β« π’ _ πΆ
ExtEF
pπ 1 ff π 11 _ Β¨ Β¨ Β¨ _ π π ff π 1π _ π‘ ff π’ _ π 1 Β« π’ _ πΆqπ
Rules ExtSup, ExtER, and ExtEF are extensional versions of superposition, equality resolution
and equality factoring [23]. The union of these three rules is denoted by Ext. In each rule, π
is a most general unifier of the types of π and π 1 , and dppπ π, π 1 πq β tpπ 1 , π 11 q, . . . , pπ π , π 1π qu. All
154
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
side conditions for extensional rules are the same as for the standard rules, except that condition
that π and π 1 are unifiable is replaced by the condition that at least one π π is of functional type
and that π Δ
0. This rule is easily extended to support Boolean extensionality by requiring that
at least one π π is of functional or type π, and adding the condition βdppπ, πq β tpπ, πqu if π and
π are different formulasβ to the definition of dp.
Consider the clause f pβ£p _ β£qq ff f pβ£pp ^ qqq. This problem is obviously unsatisfiable,
since arguments of f on different 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, effectively 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 [10])
to both sides of a (dis)equation to reduce it to a first-order literal; Boolean extensionality is
usually better supported by applying EC on the top-level Boolean term. Thus, for the following
discussion we can assume π and π 1 are not π-abstractions or formulas. Then, ExtSup is applicable
if π and π 1 have the same head, and a functional or Boolean subterm. To efficiently retrieve such
terms, we added an index that maps symbols to positions in clauses where they appear as a
head of a term that has a functional or Boolean subterm. This index will be empty for first-order
problems, incurring no overhead if extensionality reasoning is not needed. Furthermore, we
do not apply Ext rules if all disagreement pairs have at least one side whose head is a variable;
those will be dealt with more efficiently using standard, non-extensional, versions of the rules.
We also eagerly resolve literals π π ff π 1π using at most one unifier returned by terminating,
pragmatic variant of unification algorithm by VukmiroviΔ et al. [21].
Expressiveness of higher-order logic allows users to define equality using a single axiom,
called Leibniz equality [16]: @pπ₯ : πΌqpπ¦ : πΌq. p@pπ : πΌ Γ πq. π π₯ Γ± π π¦q Γ± π₯ Β« π¦. Leibniz
equality often appears in TPTP problems. Since modern provers have the native support for
equality, it is usually beneficial to recognize and replace occurrences of 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 π
π π 1π Β« J _ Β¨ Β¨ Β¨ _ π π ππ Β« J _ π π‘π ff J _ Β¨ Β¨ Β¨ _ π π‘π ff J _ πΆ
ElimPredVar
pπ π 1π Β« J _ Β¨ Β¨ Β¨ _ π π ππ Β« J _ πΆqπ
where π is a free variable, π does not occur in any π ππ or π‘ππ , or in πΆ, and π is defined as
tπ ΓΓ ππ₯π . ππβ1 p ππβ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 ^π¦ Β« b2 q_pπ₯ Β« c1 ^π¦ Β« c2 qu. After
applying π to πΆ and subsequent π½-reduction, negative literal π b1 b2 ff J will reduce to pb1 Β«
b1 ^ b2 Β« b2 q _ pb1 Β« c1 ^ b2 Β« c2 q 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.
155
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
The previous rule removes all variables occurring in disequations in one attempt. We imple-
mented two rules that behave more lazily, inspired by the ones present in Leo-III and Satallax:
π π π Β« J _ π π‘π ff J _ πΆ π π π ff J _ π π‘π Β« J _ πΆ
ElimLeibniz` ElimLeibnizΒ΄
pπ π Β« π‘π _ πΆqπ pπ π Β« π‘π _ πΆqπ 1
where π is a free variable, π does not occur in π‘π , π β tπ ΓΓ ππ₯π . π₯π Β« π‘π u and π 1 β tπ ΓΓ
ππ₯π . β£pπ₯π Β« π‘π qu. This rule differs 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ππ₯π¦. π₯ Β« b1 u to obtain the clause πΆ 1 β a1 Β« b1 _ a1 ff c1 .
3.4. Additional Rules
Zipperpositionβs unification algorithm [21] uses flattened representation of terms with logical
operators ^ and _ for heads to unify terms that are not unifiable modulo πΌπ½π-equivalence,
but are unifiable modulo associativity and commutativity of ^ and _. Let Λ denote either ^
or _. When the unification algorithm is given two terms Λ π π and Λ π‘π , where neither of π π nor
π‘π contain duplicates, it performs the following steps: First, it removes all terms that appear
in both π π and π‘π from the two argument tuples. Next, the remaining terms are sorted first by
their head term and then by their weight. Finally, the
` sorted lists are unified pairwise. As anΛ
example, consider the problem of unifying the pair ^ pp aq pq pf aqq, ^ pq pf aqq pπ pf pf aqqq
where π is a free variable. If the arguments of ^ are simply sorted as described above, we
would unsuccessfully try to unify p a with q pf aq. However, by removing term q pf aq from the
argument lists, we will be left with the problem pp a, π pf pf aqqq which has a unifier.
The winner of THF division of CASC-27 [27], Satallax [15], has one crucial advantage over
Zipperposition: it is based on higher-order tableaux, and as such it does not require formulas
to be converted to clauses. The advantage of tableaux is that once it instantiates a variable with
a term, this instantiation naturally propagates through the whole formula. In Zipperposition,
which is based on higher-order superposition, the original formula is clausified and instantiating
a variable in a clause πΆ does not automatically instantiate it in all clauses that are results of
clausification of the same formula as πΆ. To mitigate this issue, we have created extensions of
equality resolution and equality factoring that take Boolean extensionality into account:
π Β« π 1 _ πΆ π π π Β« J _ π 1 ff J _ πΆ
BoolER BoolEF`Β΄
πΆπ pπ π π Β« β£π 1 _ πΆqπ
π π π ff J _ π 1 Β« J _ πΆ π π π ff J _ π 1 ff J _ πΆ
BoolEF´` BoolEF´´
pπ π π Β« β£π 1 _ πΆqπ pπ π π Β« π 1 _ πΆqπ
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
156
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
`Β΄ 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 suffices 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 effects of eager clausification is to delay it as long
as possible. Following the approach by Ganzinger and Stuber [28], we represent every input
formula π as a unit clause π Β« J and use the following lazy clausification (LC) rules:
pπ ^ πq Β« J _ πΆ pπ _ πq Β« J _ πΆ pπ Γ± πq Β« J _ πΆ
LC^ LC_ LCΓ±
π Β«J_πΆ πΒ«J_πΆ π Β«J_πΒ«J_πΆ π ff J _ π Β« J _ πΆ
pβ£π q Β« J _ πΆ p@π₯. π q Β« J _ πΆ pDπ₯. π q Β« J _ πΆ
LCβ£ LC@ LCD
π ff J _ πΆ π tπ₯ ΓΓ π¦u _ πΆ π tπ₯ ΓΓ skxπΌyπ¦ π u _ πΆ
π Β«π_πΆ
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 [28]. In LCΒ« we require both π and π to be formulas and at least one of
them not to be J. In LC@ , π¦ is a fresh variable, and in LCD , sk is a fresh symbol and πΌ and π¦ π
are all the type and term variables occurring freely in Dπ₯. π .
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 different 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 π 1 tπ₯ ΓΓ pskxπΌπ yπ¦ π qπu. Renaming and name reusing techniques are inspired by
the VCNF algorithm described by Reger et al. [29].
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
157
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
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
Interpretπ
p@π₯π . π q ff J _ πΆrππ₯π . Js p@π₯π . β£π q ff J _ πΆrππ₯π . Ks
4. Alternative Approaches
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.
4.1. Axiomatization
A simple axiomatization of the theory of Booleans is given by Bentkamp et al. [10]. Following
their approach, we introduce the proxy type bool , which corresponds to π, to the signature.
We define proxy symbols t, f, not, and, or, impl, equiv, forall, exists, choice, and eq which correspond
to the homologous logical constants from Section 2. In their type declarations π is replaced by
bool .
To make this paper self-contained we include the axioms from Bentkamp et al. [10]. Definitions
of symbols are computational in nature: symbols are characterized by their behavior on t and
f. This also reduces interferences between different axioms. Axioms are listed as follows:
t ff f or t π₯ Β« t equiv π₯ π¦ Β« and pimpl π₯ π¦q pimpl π¦ π₯q
π₯Β«t_π₯Β«f or f π₯ Β« π₯ forallxπΌypππ₯. tq Β« t
not t Β« f impl t π₯ Β« π₯ π¦ Β« pππ₯. tq _ forallxπΌy π¦ Β« f
not f Β« t impl f π₯ Β« t existsxπΌy π¦ Β«
and t π₯ Β« π₯ π₯ ff π¦ _ eqxπΌy π₯ π¦ Β« t not pforallxπΌy pππ₯. not pπ¦ π₯qqq
and f π₯ Β« f π₯ Β« π¦ _ eqxπΌy π₯ π¦ Β« f π¦ π₯ Β« f _ π¦ pchoicexπΌyπ¦q Β« t
4.2. Preprocessing Booleans
Kotelnikov et al. extended VCNF, Vampireβs algorithm for clausification, to support nested
Booleans [13]. VukmiroviΔ et al. extended the clausification algorithm of Ehoh, the lambda-free
higher-order version of E, to support nested Booleans inspired by VCNF extension [11, Section
8]. Zipperposition and Ehoh share the same clausification algorithm, enabling us to reuse the
extension with one notable difference: unlike in Ehoh, not all nested Booleans different from
variables, J and K will be removed. Namely, Booleans that are below π-abstraction and contain
π-bound variables will not be preprocessed. They cannot be easily hoisted to the level of an atom
in which they appear, since this process might leak any variables bound in the context in which
the nested Boolean appears. Similar preprocessing techniques are used in other higher-order
provers [30].
158
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
5. Examples
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 [10] which applies fresh variable
π€ to both sides of the equation, yielding clause πΆ β sk1 psk2 π¦q π€ Β« π¦ π€. Most superposition-
or paramodulation-based higher-order theorem provers (such as Leo-III, Vampire and Zip-
perposition) will split this clause into two clauses πΆ1 β sk1 psk2 π¦q π€ ff J _ π¦ π€ Β« J and
πΆ2 β sk1 psk2 π¦q π€ Β« J _ π¦ π€ ff J. This clausification step makes the problem considerably
harder. Namely, the clause πΆ instantiated with the substitution tπ¦ ΓΓ ππ₯. β£psk1 π₯ π₯q, π€ ΓΓ
sk2 pππ₯. β£psk1 π₯ π₯qqu yields the empty clause. However, if the original clause is split into two
as described above, Zipperposition will rely on PI rule to instantiate π¦ with imitation of β£ and
on equality factoring to further instantiate this approximation. These desired inferences need
to be applied on both new clauses and represent only a fraction of inferences that can be done
with πΆ1 and πΆ2 , reducing the chance of successful proof attempt. Rule BoolER imitates the
behavior of tableaux prover: it essentially rewrites the clause πΆ into β£psk1 psk2 π¦q π€q ff π¦ π€
which makes finding the necessary substitution easy and does not require a clausification step.
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 effect
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.
159
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
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 effects. 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.
6. Evaluation
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 [31] servers with Intel Xeon E5-2609 0
CPUs clocked at 2.40 GHz. The evaluation is separated in two parts that answer different
questions: How useful are the new rules? How does our approach compare with state-of-the-art
higher-order provers?
6.1. Evaluation of the Rules
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. [21]. It enables
BoolSimp rule, EC rule, PI rule in Pragmatic mode with π β 2, ElimLeibniz and ElimPredVar
rules, BoolER rule, and BoolEF rules. To evaluate the usefulness of all rules we described above,
we enable, disable or change the parameters of a single rule, while keeping all other parameters
of π intact. In figures that contain sufficiently different configurations, cells are of the form πpπq
where π is the total number of proved problems by a particular configuration and π is the number
of unique problems that a given configuration solved, compared to the other configurations in the
same figure. Intersections of rows and columns denote corresponding combination of parameters.
Result for the base configuration is written in cursive; the best result is written in bold.
First, we tested different 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 different 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.
160
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
a lo li
b 1646 1648 1640
bc 1644 1645 1644
Figure 1: Effect of the Cases(Simp) rule on success rate
Β΄PI bπ bπ b^ b_ bΒ« bβ£ b@D
πβ1 1648 1628 1637 1634 1630 1641 1637
πβ2 1636 1646 1629 1636 1631 1627 1638 1634
πβ8 1643 1625 1633 1631 1623 1637 1635
Figure 2: Effect of PI rule on success rate
Β΄EL `EL Β΄BEF `BEF
Β΄EPV 1584 (0) 1644 (0) Β΄BER 1644 (2) 1643 (0)
`EPV 1612 (0) 1646 (0) `BER 1645 (0) 1646 (0)
Figure 3: Effect of Leibniz equality elimination Figure 4: Effect of BoolER and BoolEF
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 different values of π. The
results show that different values for π have a modest effect 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 different modes somewhat differ.
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 effects 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 difference. 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
161
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
CVC4 Leo-III Satallax Vampire Zipperposition
pure 1806 (5) 1627 (0) 2067 (0) 1924 (7) 1980 ( 0)
coop β 2085 (3) 2214 (9) β 2190 (17)
Figure 5: Comparison with other higher-order provers
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.
6.2. Comparison with Other Higher-Order Provers
We compared Zipperposition with all higher-order theorem provers that took part in THF
division of CASC-27[27]: CVC4 1.8 prerelease [4], Leo-III 1.4 [14], Satallax 3.4 [15], and Vampire-
THF 4.4 [6]. In this part of the evaluation, Zipperposition is ran in portfolio mode that runs
configurations in different time slices. We set the CPU time limit to 180 s, the time allotted to
each prover at 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 [32] as backends, while
Satallax uses Ehoh [11] as backend. Zipperposition can use Ehoh as backend as well. To test
effectiveness of each calculus, we run the cooperative provers in two versions: pure, which
disables backends, and coop which uses all supported backends.
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. Leo-
III 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.
7. Discussion and Related Work
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 effort
has gone into making the translations of higher-order logic as efficient as possible. Descriptions
of hammers like HOLyHammer [1] and Sledgehammer [2] for Isabelle contain details of these
translations. Software verifiers Boogie [33] and Why3 [34] use similar translations.
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 [10, 11, 9]. Those two provers are built from the ground up as
higher-order provers β treatment of exclusively higher-order issues such as extensionality or
choice is built into them usually using explosive rules. Those explosive rules might contribute
162
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
to their suboptimal performance on mostly first-order Sledgehammer problems.
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 [35], in which
both authors of this paper participate, resulted in adding support for π-free higher-order logic
with Booleans to E [11] and veriT [9], and adding support for Boolean-free higher-order logic
to Zipperposition. Authors of many state-of-the-art first-order provers have implemented some
form of support for higher-order reasoning. This is true both for SMT solvers, witnessed by
the recent extension of CVC4 and veriT [9], and for superposition provers, witnessed by the
extension of Vampire [36]. All of those approaches were arguably more focused on functional
aspects of higher-order logic, such as π-binders and function extensionality, than on Boolean
aspects such as Boolean subterms and Boolean extensionality. A notable exception is work by
Kotelnikov et al. that introduced support for Boolean subterms to first-order Vampire [12, 13].
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 [10]. We conjecture that it is this
efficient reasoning base on which the approach is based that contributes to its competitive
performance.
8. Conclusion
We presented a pragmatic approach to support Booleans in a modern automatic prover for
clausal higher-order logic. Our approach combines previous research efforts that extended
first-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. [10], we do not give any completeness guarantees for
our extension. We plan to develop a refutationally complete calculus that supports Booleans
around core rules such as Cases and LC in future work.
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).
163
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
References
[1] C. Kaliszyk, J. Urban, Hol(y)hammer: Online ATP service for HOL light, Mathematics in
Computer Science 9 (2015) 5β22.
[2] L. C. Paulson, J. C. Blanchette, Three years of experience with Sledgehammer, a practical
link between automatic and interactive theorem provers, in: G. Sutcliffe, S. Schulz,
E. Ternovska (Eds.), IWIL-2010, volume 2 of EPiC, EasyChair, 2012, pp. 1β11.
[3] J. FilliΓ’tre, A. Paskevich, Why3 - where programs meet provers, in: M. Felleisen,
P. Gardner (Eds.), Programming Languages and Systems - 22nd European Symposium on
Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and
Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, volume
7792 of LNCS, Springer, 2013, pp. 125β128.
[4] C. W. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds,
C. Tinelli, CVC4, in: G. Gopalakrishnan, S. Qadeer (Eds.), CAV 2011, volume 6806 of LNCS,
Springer, 2011, pp. 171β177.
[5] S. Schulz, S. Cruanes, P. Vukmirovic, Faster, higher, stronger: E 2.3, in: P. Fontaine (Ed.),
CADE 2019, volume 11716 of LNCS, Springer, 2019, pp. 495β507.
[6] L. KovΓ‘cs, A. Voronkov, First-order theorem proving and vampire, in: N. Sharygina,
H. Veith (Eds.), CAV 2013, volume 8044 of LNCS, Springer, 2013, pp. 1β35.
[7] J. Robinson, A note on mechanizing higher order logic, in: B. Meltzer, D. Michie (Eds.),
Machine Intelligence, volume 5, Edinburgh University Press, 1970, pp. 121β135.
[8] J. Meng, L. C. Paulson, Translating higher-order clauses to first-order clauses, J. Autom.
Reasoning 40 (2008) 35β60.
[9] H. Barbosa, A. Reynolds, D. E. Ouraoui, C. Tinelli, C. W. Barrett, Extending SMT solvers
to higher-order logic, in: P. Fontaine (Ed.), CADE 2019, volume 11716 of LNCS, Springer,
2019, pp. 35β54.
[10] A. Bentkamp, J. Blanchette, S. Tourret, P. VukmiroviΔ, U. Waldmann, Superposition with
lambdas, 2020. Submitted to a journal, http://matryoshka.gforge.inria.fr/pubs/lamsup_
report.pdf.
[11] P. Vukmirovic, J. C. Blanchette, S. Cruanes, S. Schulz, Extending a brainiac prover to
lambda-free higher-order logic, 2020. Submitted to a journal, http://matryoshka.gforge.
inria.fr/pubs/ehoh_article.pdf.
[12] E. Kotelnikov, L. KovΓ‘cs, A. Voronkov, A first class boolean sort in first-order theorem
proving and TPTP, CoRR abs/1505.01682 (2015). arXiv:1505.01682.
[13] E. Kotelnikov, L. KovΓ‘cs, M. Suda, A. Voronkov, A clausal normal form translation for
FOOL, in: C. BenzmΓΌller, G. Sutcliffe, R. Rojas (Eds.), GCAI 2016, volume 41 of EPiC Series
in Computing, EasyChair, 2016, pp. 53β71.
[14] A. Steen, C. BenzmΓΌller, The higher-order prover Leo-III, in: D. Galmiche, S. Schulz,
R. Sebastiani (Eds.), IJCAR 2018, volume 10900 of LNCS, Springer, 2018, pp. 108β116.
[15] C. E. Brown, Satallax: An automatic higher-order prover, in: B. Gramlich, D. Miller,
U. Sattler (Eds.), IJCAR 2012, volume 7364 of LNCS, Springer, 2012, pp. 111β117.
[16] P. B. Andrews, Classical type theory, in: J. A. Robinson, A. Voronkov (Eds.), Handbook of
Automated Reasoning, volume II, Elsevier and MIT Press, 2001, pp. 965β1007.
[17] G. Sutcliffe, The TPTP problem library and associated infrastructure - from CNF to TH0,
164
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
TPTP v6.4.0, J. Autom. Reasoning 59 (2017) 483β502.
[18] S. Cruanes, Extending Superposition with Integer Arithmetic, Structural Induction, and
Beyond, Ph.D. thesis, Γcole polytechnique, 2015.
[19] S. Cruanes, Superposition with structural induction, in: C. Dixon, M. Finger (Eds.), FroCoS
2017, volume 10483 of LNCS, Springer, 2017, pp. 172β188.
[20] I. Cervesato, F. Pfenning, A linear spine calculus, J. Log. Comput. 13 (2003) 639β688.
[21] P. Vukmirovic, A. Bentkamp, V. Nummelin, Efficient full higher-order unification, in: Z. M.
Ariola (Ed.), FSCD 2020, volume 167 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fΓΌr
Informatik, 2020, pp. 5:1β5:17.
[22] L. Bachmair, H. Ganzinger, Rewrite-based equational theorem proving with selection and
simplification, J. Log. Comput. 4 (1994) 217β247.
[23] S. Schulz, E - a brainiac theorem prover, AI Commun. 15 (2002) 111β126.
[24] A. Nonnengart, C. Weidenbach, Computing small clause normal forms, in: J. A. Robinson,
A. Voronkov (Eds.), Handbook of Automated Reasoning (in 2 volumes), Elsevier and MIT
Press, 2001, pp. 335β367.
[25] A. Steen, Extensional paramodulation for higher-order logic and its effective
implementation Leo-III, Ph.D. thesis, Free University of Berlin, Dahlem, Germany, 2018.
[26] A. Bhayat, G. Reger, A combinator-based superposition calculus for higher-order logic, in:
N. Peltier, V. Sofronie-Stokkermans (Eds.), IJCAR 2020, volume 12166 of Lecture Notes in
Computer Science, Springer, 2020, pp. 278β296.
[27] G. Sutcliffe, The CADE-27 automated theorem proving system competition - CASC-27, AI
Commun. 32 (2019) 373β389.
[28] H. Ganzinger, J. Stuber, Superposition with equivalence reasoning and delayed clause
normal form transformation, Inf. Comput. 199 (2005) 3β23.
[29] G. Reger, M. Suda, A. Voronkov, New techniques in clausal form generation, in:
C. BenzmΓΌller, G. Sutcliffe, R. Rojas (Eds.), GCAI 2016, volume 41 of EPiC Series in
Computing, EasyChair, 2016, pp. 11β23.
[30] M. Wisniewski, A. Steen, K. Kern, C. BenzmΓΌller, Effective normalization techniques for
HOL, in: N. Olivetti, A. Tiwari (Eds.), IJCAR 2016, volume 9706 of LNCS, Springer, 2016,
pp. 362β370.
[31] A. Stump, G. Sutcliffe, C. Tinelli, StarExec: A cross-community infrastructure for logic
solving, in: S. Demri, D. Kapur, C. Weidenbach (Eds.), IJCAR 2014, volume 8562 of LNCS,
Springer, 2014, pp. 367β373.
[32] K. Korovin, iprover - an instantiation-based theorem prover for first-order logic (system
description), in: A. Armando, P. Baumgartner, G. Dowek (Eds.), IJCAR 2008, volume 5195
of LNCS, Springer, 2008, pp. 292β298.
[33] K. R. M. Leino, P. RΓΌmmer, A polymorphic intermediate verification language: Design and
logical encoding, in: J. Esparza, R. Majumdar (Eds.), TACAS 2010, volume 6015 of LNCS,
Springer, 2010, pp. 312β327.
[34] F. Bobot, J.-C. FilliΓ’tre, C. MarchΓ©, A. Paskevich, Why3: Shepherd Your Herd of Provers,
in: Boogie 2011: First International Workshop on Intermediate Verification Languages,
Wroclaw, Poland, 2011, pp. 53β64.
[35] J. Blanchette, P. Fontaine, S. Schulz, S. Tourret, U. Waldmann, Stronger higher-order
automation: A report on the ongoing matryoshka project, in: M. Suda, S. Winkler (Eds.),
165
Petar VukmiroviΔ et al. CEUR Workshop Proceedings 148β166
EPTCS 311: Proceedings of the Second International Workshop on Automated Reasoning:
Challenges, Applications, Directions, Exemplary Achievements - Natal, Brazil, August 26,
2019, Electronic Proceedings in Theoretical Computer Science, EPTCS, EPTCS, 2019, pp.
11β18.
[36] A. Bhayat, G. Reger, Restricted combinatory unification, in: P. Fontaine (Ed.), CADE 2019,
volume 11716 of LNCS, Springer, 2019, pp. 74β93.
166