                         WoD 2004 Preliminary Version

Bounded Model Generation for Isabelle/HOL

Tjark Weber^{1,2}

Institut für Informatik, Technische Universität München Boltzmannstr. 3, D-85748 Garching b. München, Germany

Abstract A translation from higher-order logic (on top of the simply typed λ-calculus) to propositional logic is presented, such that the resulting propositional formula is satisfiable iff the HOL formula has a model of a given finite size. A standard SAT solver can then be used to search for a satisfying assignment, and such an assignment can be transformed back into a model for the HOL formula. The algorithm has been implemented in the interactive theorem prover Isabelle/HOL, where it is used to automatically generate countermodels for non-theorems.

Key words: Higher-Order Logic, Finite Model Generation, Interactive Theorem Proving

1 Introduction

Interactive theorem provers have been enhanced with numerous automatic proof procedures for different application domains. However, when an automatic proof attempt fails, the user usually gets little information about the reasons. It may be that an additional lemma needs to be proved, that an induction hypothesis needs to be generalized, or that the formula one is trying to prove is not valid. In such cases an automatic tool that can refute non-theorems would be useful.

This paper presents a translation from higher-order logic to propositional logic (quantifier-free Boolean formulae) such that the propositional formula is satisfiable if and only if the HOL formula has a model of a given finite size, i.e. involving no more than a given number of elements. A standard SAT solver can then be used to search for a satisfying assignment, and if such an assignment is found, it can easily be transformed back into a model for the HOL formula.

1 This work was supported by the PhD program Logic in Computer Science of the German Research Foundation.

2 Email: webertj@in.tum.de

This is a preliminary version. The final version will be published in Electronic Notes in Theoretical Computer Science

                       URL: www.elsevier.nl/locate/entcs

Weber

An algorithm that uses this translation to generate (counter-)models for HOL formulae has been implemented in the interactive theorem prover Isabelle/HOL [15]. This algorithm is not a (semi-)decision procedure: if a formula does not have a model of a given size, it may still have larger or infinite models. The algorithm’s applicability is also limited by its complexity, which is non-elementary for higher-order logic. Nevertheless, formulae that occur in practice often have small models, and the usefulness of an approach similar to the one described in this paper has been confirmed in [10].

Section 2 introduces the syntax and semantics of the logic considered in this paper, a version of higher-order logic on top of the simply typed λ-calculus. The model generation algorithm, and in particular the translation into propositional logic are described in Section 3. We conclude with some final remarks in Section 4.

2 The HOL Logic

Our translation can handle a large fragment of the logic that is underlying the HOL [9] and Isabelle/HOL theorem provers. The logic is originally based on Church’s simple theory of types [3]. In this section we present the syntax and set-theoretic semantics of the relevant fragment. A complete account of the HOL logic, including a proof system, can be found in [8].

We distinguish types and terms, intended to denote certain sets and elements of sets respectively. Types σ are given by the following grammar, where α ranges over a countably infinite set T V of type variables:

σ ::= o | α | σ → σ.

Type variables stand for arbitrary non-empty sets. The type o denotes a distinguished two-element set {⊤, ⊥}. If σ_{1} and σ_{2} are types, then σ_{1} → σ_{2} is the function type with domain σ_{1} and range σ_{2}. It denotes the set of all total functions from the set denoted by its domain to the set denoted by its range. As usual, → associates to the right, i.e. σ_{1} → σ_{2} → σ_{3} is short for σ_{1} → (σ_{2} → σ_{3}).

We assume a countably infinite set V of variables. A term t_{σ} of type σ is either an (explicitly typed) variable, logical constant, application, or λabstraction. Hence terms are given by the following grammar:

t_{σ} ::= x_{σ} | c_{σ} | (t_{σ′→σ} t_{σ′})_{σ} | (λx_{σ_{1}}. t_{σ_{2}})_{σ_{1}→σ_{2}},

where x_{σ} ranges over variables, and c_{σ} is either ⟹ _{o→o→o} (implication) or =_{σ′→σ′→o} (equality on σ′), usually written in infix notation. Other logical constants, including ∨_{o→o→o}, ∧_{o→o→o}, ¬_{o→o}, and quantifiers of arbitrary order, can be defined as λ-terms [1]. Terms of type o are called formulae.

We now define the semantics of terms. Let t_{σ} be a term of type σ, and let tv(t_{σ}) ⊆ T V be the set of all type variables that occur in t_{σ}. tv can be defined inductively with the help of an auxiliary function tv′ that collects the type variables occuring in a type:

tv′(o) = ∅,
tv′(α) = {α},
tv′(σ_{1} → σ_{2}) = tv′(σ_{1}) ∪ tv′(σ_{2}),

and

tv(x_{σ}) = tv′(σ),
tv(c_{σ}) = tv′(σ),
tv((t_{σ′→σ} t′_{σ′})_{σ}) = tv(t_{σ′→σ}) ∪ tv(t′_{σ′}),
tv((λx_{σ_{1}}. t_{σ_{2}})_{σ_{1}→σ_{2}}) = tv′(σ_{1}) ∪ tv(t_{σ_{2}}).

Note that tv(t_{σ}) is not necessarily contained in tv′(σ). Types σ with tv′(σ) ≠ ∅ and terms t_{σ} with tv(t_{σ}) ≠ ∅ are called polymorphic.

Furthermore, let fv(t_{σ}) ⊆ V be the set of all free variables that occur in t_{σ}, defined as usual:

fv(x_{σ}) = {x_{σ}},
fv(c_{σ}) = ∅,
fv((t_{σ′→σ} t′_{σ′})_{σ}) = fv(t_{σ′→σ}) ∪ fv(t′_{σ′}),
fv((λx_{σ_{1}}. t_{σ_{2}})_{σ_{1}→σ_{2}}) = fv(t_{σ_{2}}) \ {x_{σ_{1}}}.

It is obvious that tv(t_{σ}) and fv(t_{σ}) are finite.

An environment D for t_{σ} is a function that assigns to each type variable α ∈ tv(t_{σ}) a non-empty set D(α). The semantics of types w.r.t. this environment is formally given by

[[o]]_{D} = {⊤, ⊥},
[[α]]_{D} = D(α),
[[σ_{1} → σ_{2}]]_{D} = [[σ_{2}]]_{D}^{[[σ_{1}]]^{D}}.

A variable assignment A for t_{σ} w.r.t. an environment D maps each variable x_{σ′} ∈ fv(t_{σ}) to an element A(x_{σ′}) of the set denoted by the type σ′. Given a variable assignment A, a variable x_{σ′} ∈ V, and an element d of the set denoted by σ′, let A[x_{σ′} ↦ d] be the assignment that maps x_{σ′} to d, and v ≠ x_{σ′} to A(v). Now the semantics of terms w.r.t. an environment D and an assignment A is given by

[[x_{σ}]]_{D}^{A} = A(x_{σ}),

[[ ⟹_{o→o→o}]]_{D}^{A} is the function that sends \{ \begin{matrix}⊤, ⊤ & to & ⊤ \\ ⊤, ⊥ & to & ⊥ \\ ⊥, ⊤ & to & ⊤ \\ ⊥, ⊥ & to & ⊤ \end{matrix} ,

[[ =_{σ′→σ′→o} ]]_{D}^{A} is the function that sends x, y ∈ [[σ′]]_{D}
to \{ \begin{matrix}⊤ & if x = y \\ ⊥ & otherwise \end{matrix} ,
[[(t_{σ′→σ} t′_{σ′})_{σ}]]_{D}^{A} = [[t_{σ′→σ}]]_{D}^{A}([[t′_{σ′}]]_{D}^{A}) (function application),
[[(λx_{σ_{1}}. t_{σ_{2}})_{σ_{1}→σ_{2}}]]_{D}^{A} is the function that sends each d ∈ [[σ_{1}]]_{D}
to [[t_{σ_{2}}]]_{D}^{A[x_{σ_{1}}↦d]}.

Hence the semantics of a term t_{σ} is an element of the set denoted by the type σ, i.e. [[t_{σ}]]_{D}^{A} ∈ [[σ]]_{D}.

3 Bounded Model Generation

The model generation for a HOL formula ϕ = t_{o} proceeds in several steps. We first fix the size of the model by choosing an environment D for ϕ that contains only finite sets. Note that environments are determined uniquely up to isomorphism by the size of the sets that they assign to type variables; the names of elements are irrelevant. With a fixed finite size for every set denoted by a type variable, every type then denotes a finite set: clearly |o| = 2, and |σ_{1} → σ_{2}| = |σ_{2}|^{|σ_{1}|}. Our task now is to find a variable assignment A with [[ϕ]]_{D}^{A} = ⊤. (To generate a countermodel, we can either consider ¬ϕ, or – equivalently – search for a variable assignment A with [[ϕ]]_{D}^{A} = ⊥.) At this point one can already view bounded model generation as a generalization of satisfiability checking, where the search tree is not necessarily binary, but still finite.

3.1 Translation into Propositional Logic

The input formula ϕ is translated into a propositional formula that is satisfiable if and only if such a variable assignment exists. Propositional formulae are given by the following grammar:

φ ::= True | False | p | ¬φ | φ ∨ φ | φ ∧ φ,

where p ranges over a countably infinite set of Boolean variables. The translation is by induction over terms. Although our aim is to translate a term of type o into a single propositional formula, a more complex intermediate data structure is needed to translate subterms (which may be of arbitrary type): we use trees whose leafs are labelled with propositional formulae. The construction of these trees is described in detail in the remainder of this section. A tree of height 1 and width m corresponds to a term whose type is a type variable (denoting a set of size m) or o (for m = 2), while an n-ary function or predicate is given by a tree of height n + 1. We will show how application and λ-abstraction can be “lifted” from the term level to this intermediate data structure.

To define the translation more precisely, several auxiliary functions are needed. The create function is invoked once for each free variable in ϕ, and returns a tree whose leafs are labelled with Boolean variables. (p) is a placeholder for a fresh Boolean variable, i.e. different occurrences of (p) are replaced by different Boolean variables. The height and width of the tree only depend on the type of the free variable in ϕ. Multiple occurrences of a free variable in ϕ are replaced by identical trees.

create(o) = [(p), (p)],
create(α) = [(p), …, (p)] of length |α|,
create(σ_{1} → σ_{2}) = [create(σ_{2}), …, create(σ_{2})] of length |σ_{1}|.

As can be seen from these rules, we use Boolean variables in a unary, rather than in a binary fashion. This means that we need n variables to represent an element of a type of size n, rather than ⌈log_{2} n⌉ variables. However, exactly one of these variables must later be set to True (which keeps the search space for the SAT solver small due to unit propagation [21]), and our encoding allows for a relatively simple translation of application. To ensure that exactly one of the Boolean variables p_{1}, …, p_{n} is set to True, a propositional formula

wf_{[p_{1},...,p_{n}]} = (⋁_{i=1}^{n} p_{i}) ∧ ⋀_{i,j=1}^{n} ; i≠j (¬p_{i} ∨ ¬p_{j})

is constructed for each tree of the form [p_{1}, …, p_{n}] that is returned by a call to create(o) or create(α). This formula is later conjoined with the result of the translation.

TT and FF are trees corresponding to ⊤ and ⊥, respectively.

TT = [True, False],
FF = [False, True].

The k-th unit vector of length n with entries True and False is given by uv_{k}^{n}, and likewise UV_{k}^{n} is the k-th unit vector of length n with entries TT and FF.

δ_{k}^{n} = \{ \begin{matrix}True & if n = k \\ False & otherwise \end{matrix} ,
uv_{k}^{n} = [δ_{1}^{k}, …, δ_{n}^{k}],
Δ_{k}^{n} = \{ \begin{matrix}TT & if n = k \\ FF & otherwise \end{matrix} ,
UV_{k}^{n} = [Δ_{1}^{k}, …, Δ_{n}^{k}].

These unit vectors are used to build trees whose leafs are labelled with propositional constants (True/False) only, representing specific (i.e. the first, second, …) elements of the domains under consideration. Also note that TT = uv_{1}^{2}, and FF = uv_{2}^{2}.

consts(σ) returns a list of length |σ|, containing one representing tree for every element in [[σ]]_{D}. pick([x_{1}, …, x_{n}]) – where each x_{i} is again a list – is an auxiliary function that returns a list containing all possible choices of one element from each list x_{i}. For the special case x_{1} = … = x_{n}, this corresponds to all functions from an n-element set to elements of x_{1}.

consts(o) = [TT, FF],
consts(α) = [uv_{1}^{|α|}, …, uv_{|α|}^{|α|}],
consts(σ_{1} → σ_{2}) = pick([\underbrace{consts(σ_{2}), …, consts(σ_{2})}_{|σ_{1}|}]).

The functions described so far are sufficient to define the translation for terms without application. The translation of application, however, requires further helper functions. all returns the conjunction of a list of propositional formulae. map(f, l) applies the unary function f to every element in a list l. Likewise, treemap(f, t) applies f to every leaf in a tree t. merge(g, t_{1}, t_{2}) merges two trees t_{1} and t_{2} by applying a binary function g to corresponding leafs in t_{1} and t_{2}. Both trees must have the same “structure”, i.e. differ at most in the formulae that they contain (but not in their height or width).

all([φ_{1}, …, φ_{n}]) = φ_{1} ∧ … ∧ φ_{n},
map(f, [φ_{1}, …, φ_{n}]) = [f(φ_{1}), …, f(φ_{n})],
treemap(f, [φ_{1}, …, φ_{n}]) = [f(φ_{1}), …, f(φ_{n})],
treemap(f, [t_{1}, …, t_{n}]) = [treemap(f, t_{1}), …, treemap(f, t_{n})],
merge(g, [φ_{1}^{1}, …, φ_{n}^{1}], [φ_{1}^{2}, …, φ_{n}^{2}]) = [g(φ_{1}^{1}, φ_{1}^{2}), …, g(φ_{n}^{1}, φ_{n}^{2})],
merge(g, [t_{1}^{1}, …, t_{n}^{1}], [t_{1}^{2}, …, t_{n}^{2}]) = [merge(g, t_{1}^{1}, t_{1}^{2}), …, merge(g, t_{n}^{1}, t_{n}^{2})].

enum(t), for t a tree representing an element of [[σ]]_{D}, computes a list of propositional formulae [φ_{1}, …, φ_{|σ|}] expressing that t represents the first, …, |σ|-th element of [[σ]]_{D}.

enum([φ_{1}, …, φ_{n}]) = [φ_{1}, …, φ_{n}],
enum([t_{1}, …, t_{n}]) = map(all, pick([enum(t_{1}), …, enum(t_{n})])).

Functions are represented by trees of height greater than 1. Intuitively, when a function is applied to the i-th element of its domain, the result is given by the i-th subtree of the tree representing the function. apply(t, [φ_{1}, …, φ_{n}]), where t is a tree representing a function, and φ_{i} is true iff the function’s argument is equal to the i-th element of the function’s domain, builds a tree whose leafs are labelled with propositional formulae that simulate the selection of the correct subtree of t.

apply([t_{1}], [φ_{1}]) = treemap((\underline{λ}φ. φ ∧ φ_{1}), t_{1}),
apply([t_{1}, t_{2}, …, t_{n}], [φ_{1}, φ_{2}, …, φ_{n}]) = merge((\underline{λ}φ φ′. φ ∨ φ′),

apply([t_{1}], [φ_{1}]), apply([t_{2}, …, t_{n}], [φ_{2}, …, φ_{n}])).

Above \underline{λ} is a meta-symbol used to denote a function (as opposed to the λ that is part of the term syntax), while ∨ and ∧ are constructors of propositional formulae.

We are now ready to define the translation T_{D} from terms to trees of propositional formulae. The translation is parameterized by a partial assignment B of trees to bound variables. Initially this partial assignment is empty, and it is extended whenever the translation descends into the body of a λ-abstraction. The translation is given by the following rules:

T_{D}^{B}(x_{σ}) = \{ \begin{matrix}B(x_{σ}) & if x_{σ} ∈ dom B \\ create(σ) & otherwise \end{matrix} ,
T_{D}^{B}( ⟹_{o→o→o}) = [[TT, FF], [TT, TT]],
T_{D}^{B}(=_{σ′→σ′→o}) = [UV_{1}^{|σ′|}, …, UV_{|σ′|}^{|σ′|}],
T_{D}^{B}((t_{σ′→σ} t′_{σ′})_{σ}) = apply(T_{D}^{B}(t_{σ′→σ}), enum(T_{D}^{B}(t′_{σ′}))),
T_{D}^{B}((λx_{σ_{1}}. t_{σ_{2}})_{σ_{1}→σ_{2}}) = [T_{D}^{B[x_{σ_{1}}↦d_{1}]}(t_{σ_{2}}), …, T_{D}^{B[x_{σ_{1}}↦d_{|σ_{1}|}]}(t_{σ_{2}})],
where [d_{1}, …, d_{|σ_{1}|}] = consts(σ_{1}).

Since ϕ is a term of type o, the result T_{D}^{∅}(ϕ) of the translation must be a tree of the form [T_{D}^{∅}(ϕ)^{⊤}, T_{D}^{∅}(ϕ)^{⊥}] for some propositional formulae T_{D}^{∅}(ϕ)^{⊤}, T_{D}^{∅}(ϕ)^{⊥}.

Proposition 3.1 Soundness, Completeness. Let ∗ ∈ {⊤, ⊥}, and let WF be the conjunction of all wf-formulae constructed during the translation. Then [[ϕ]]_{D}^{A} = ∗ for some variable assignment A if and only if WF ∧ T_{D}^{∅}(ϕ)^{∗} is satisfiable.

The theorem can be proved by generalization from formulae to terms of arbitrary type, followed by induction over the term. We omit the details.

3.2 Finding a Satisfying Assignment

Satisfiability can be tested with an off-the-shelf SAT solver. To this end translations into DIMACS SAT and DIMACS CNF format [6] have been implemented. The translation into SAT format is trivial, whereas CNF format (supported by zChaff [14], BerkMin [7] and other state-of-the-art solvers) requires the Boolean formula to be in conjunctive normal form. We translate into definitional CNF [19] to avoid an exponential blowup at this stage, introducing auxiliary Boolean variables where necessary. A more sophisticated CNF conversion might further enhance the performance of our approach [11].

Isabelle/HOL runs on a number of different platforms, and installation should be as simple as possible. Therefore we have also implemented a naive DPLL-based [5,21] SAT solver in Isabelle. This solver is not meant to replace the external solver for serious applications, but it has proved to be efficient enough for small examples. Hence it allows users to experiment with the countermodel generation without them having to worry about the installation of an additional tool.

If the SAT solver cannot find a satisfying assignment, the translation is repeated for a larger environment. The user can specify several termination conditions: a maximal size for sets in the environment, a limit on the number of Boolean variables to be used, a runtime limit. The order in which we enumerate environments guarantees that if the SAT solver is complete, a model will be found that is minimal w.r.t. the total size of its domains. Of course this is not necessarily true for incomplete (e.g. stochastic) SAT solvers.

3.3 Example Translation

Consider the formula ϕ = ((λx_{α}. x_{α})_{α→α} =_{(α→α)→(α→α)→o} y_{α→α})_{o}. Its only type variable is α, and its only free variable is y_{α→α}. In an environment D with |α| = 2 (and hence |α → α| = 2^{2} = 4), the subterms of ϕ are translated into the following trees:

T_{D}^{∅}((λx_{α}. x_{α})_{α→α}) = [[True, False], [False, True]],
T_{D}^{∅}(=_{(α→α)→(α→α)→o}) = [UV_{1}^{4}, UV_{2}^{4}, UV_{3}^{4}, UV_{4}^{4}],
T_{D}^{∅}(y_{α→α}) = [[y_{0}, y_{1}], [y_{2}, y_{3}]]

with four Boolean variables y_{0}, y_{1}, y_{2}, y_{3}. Additionally two wf-formulae are constructed, namely

wf_{[y_{0},y_{1}]} = (y_{0} ∨ y_{1}) ∧ (¬y_{0} ∨ ¬y_{1})

and

wf_{[y_{2},y_{3}]} = (y_{2} ∨ y_{3}) ∧ (¬y_{2} ∨ ¬y_{3}).

Using the translation rule for application, we then obtain (Boolean formulae equivalent to)

T_{D}^{∅}(ϕ)^{⊤} = y_{0} ∧ y_{3}

and

T_{D}^{∅}(ϕ)^{⊥} = (y_{0} ∧ y_{2}) ∨ (y_{1} ∧ y_{2}) ∨ (y_{1} ∧ y_{3}).

Hence a possible satisfying assignment for T_{D}^{∅}(ϕ)^{⊥}∧wf_{[y_{0},y_{1}]}∧wf_{[y_{2},y_{3}]} is given by {y_{0} ↦ True, y_{1} ↦ False, y_{2} ↦ True, y_{3} ↦ False}. Assuming [[α]]_{D} = {a_{0}, a_{1}}, this assignment corresponds to an interpretation of y_{α→α} as the function that maps both a_{0} and a_{1} to a_{0}.

3.4 Some Extensions: Sets, Hilbert’s Choice, and Datatypes

Several extensions to the logic described in Section 2 can straightforwardly be integrated into our framework. The type σ set of sets with elements from σ is isomorphic to σ → o. Set membership x ∈ P becomes predicate application P x, and set comprehension {x. P } can be translated simply as P.

Hilbert’s choice operator, ϵ, is a polymorphic constant of type (σ → o) → σ, satisfying the axiom

ϕ_{ϵ} : (∃x. P x) ⟹ P (ϵP).

Similarly, The, also a constant of type (σ → o) → σ, satisfies

ϕ_{The} : (The x. x = a) = a,

and arbitrary is a completely unspecified polymorphic constant. For the purpose of our translation T_{D}, we can treat these logical constants just like free variables, and introduce Boolean variables that determine their interpretation. For ϵ and The, we then translate the conjunction of the original formula ϕ with the relevant axiom (i.e. ϕ_{ϵ} ∧ ϕ or ϕ_{The} ∧ ϕ, respectively, or ϕ_{ϵ} ∧ ϕ_{The} ∧ ϕ if both ϵ and The occur in ϕ). Type variables in ϕ_{ϵ} (or ϕ_{The}) are instantiated to match the type of ϵ (or The) in ϕ.

Isabelle/HOL allows the definition of inductive datatypes [2]. In general, inductive datatypes with free constructors require an infinite model. We treat these datatypes by only considering a finite fragment (e.g. natural numbers up to an upper bound, or lists up to a certain length). A detailed description of the translation of inductive datatypes will be given elsewhere. We remark that if the inductive datatype occurs only positively in the input formula, then a model found for a fragment can always be extended to an infinite model for the full datatype.

However, many important datatypes are non-recursive, and for these, the situation is simpler. Examples are the type σ option, which augments a given type σ by a new element, product types σ_{1} × σ_{2}, and sum types σ_{1} + σ_{2}. The general syntax of a non-recursive datatype definition is given by

(α_{1}, …, α_{n})σ ::= C_{1} σ_{1}^{1} … σ_{m_{1}}^{1} | … | C_{k} σ_{1}^{k} … σ_{m_{k}}^{k},

where the C_{i} are the datatype’s constructors, the σ_{j}^{i} specify their argument types, and all σ_{j}^{i} only refer to previously defined types and type variables from α_{1}, …, α_{n}. Such a datatype can be interpreted in a finite model; its size is equal to S := ∑_{i=1}^{k} ∏_{j=1}^{m_{i}} |σ_{j}^{i}|. Hence an element of this datatype can be represented by a tree of height 1 and width S, and a datatype constructor C_{i} is a function of type σ_{1}^{i} → … → σ_{m_{i}}^{i} → (α_{1}, …, α_{n})σ, representable by a tree of height m_{i} + 1.

3.5 Some Optimizations

We briefly describe some optimizations in the implementation of the translation T_{D}. None of them affect soundness or completeness of the algorithm.

The Boolean formulae that are constructed during the translation process are simplified on the fly, using basic algebraic laws of ¬, ∨, ∧, True and False. Closed HOL formulae simply become True or False. The SAT solver is used only to search for an interpretation of free variables.

Variables of a type with size 1 can be represented by [True], using no Boolean variable at all (instead of one Boolean variable x together with a wf_{[x]}-formula x). While this has little effect at the SAT solver level due to unit propagation, it allows a more extensive simplification of the constructed Boolean formulae. Similarly variables of a type with size 2, including variables of type o, can be represented by a tree of the form [x, ¬x], rather than by a tree [x_{0}, x_{1}] and a wf_{[x_{0},x_{1}]}-formula (x_{0} ∨ x_{1}) ∧ (¬x_{0} ∨ ¬x_{1}).

More importantly, we avoid unfolding the definition of logical constants (i.e. True_{o}, False_{o}, ¬_{o→o}, ∧_{o→o→o}, ∨_{o→o→o}, ∀_{(σ→o)→o}, ∃_{(σ→o)→o}) as λ-terms as far as possible. Instead these constants are replaced directly by their counterparts in propositional logic. Since every type is finite, quantifiers of arbitrary order can be replaced by a finite conjunction or disjunction.

The latter leads to a more general optimization technique, applicable also to other functions and predicates (including e.g. equality): namely specialization of the rule for function application to particular functions. While any given function can be represented by a tree, it is often more efficient to implement a particular function’s action on its arguments, assuming these arguments are given as trees already, than to use the general translation rule and apply it to the tree representing the function. For =_{σ→σ→o} this avoids creating a tree whose size is proportional to |σ|^{2}, and instead uses a function that operates on trees representing elements of [[σ]]_{D}, their size proportional to |σ| (or possibly to log |σ|) only.

3.6 Examples

Table 1 shows some examples of formulae for which our algorithm can automatically find a countermodel. Type annotations are suppressed, and functions in the countermodel are given by their graphs. “∃!” denotes unique existence, defined as usual:

∃!x. P x ≡ ∃x. P x ∧ (∀y. P y ⟹ y = x).

The countermodels are rather small, and were all found within a few milliseconds. The main purpose of these examples is to illustrate the expressive

Property/Formula  Countermodel
”Every function that is onto is invertible.“ D(α) = {a_{0}, a_{1}}, D(β) = {b_{0}}
(∀y. ∃x. f x = y) ⟹ (∃g. ∀x. g (f x) = x) f = {(a_{0}, b_{0}), (a_{1}, b_{0})}
”There exists a unique choice function.“  D(α) = {a_{0}}, D(β) = {b_{0}, b_{1}}
(∀x. ∃y. P x y) ⟹ (∃!f. ∀x. P x (f x))  P = {(a_{0}, {(b_{0}, True), (b_{1}, True)})}
”The transitive closure of A ∩ B is equal to D(α) = {a_{0}, a_{1}}
the intersection of the transitive closures of A = {(a_{0}, a_{1}), (a_{1}, a_{0}), (a_{1}, a_{1})}
A and B.“  B = {(a_{0}, a_{0}), (a_{1}, a_{0}), (a_{1}, a_{1})}

Table 1 Examples

power of the underlying logic.

4 Conclusions and Future Work

We have presented a translation from higher-order logic to propositional formulae, such that the resulting propositional formula is satisfiable if and only if the HOL formula has a model of a given finite size. A working implementation of this translation, consisting of roughly 2,800 lines of code written in Standard ML [13], is available in the Isabelle/HOL theorem prover. A standard SAT solver can be used to search for a satisfying assignment for the propositional formula, and if such an assignment is found, it can be transformed into a model for the HOL formula. This allows for the automatic generation of finite countermodels for non-theorems in Isabelle/HOL. A similar translation has been discussed before [10]; the main contributions of this paper are its extension to higher-order logic and the seamless integration with a popular interactive theorem prover.

So far we have applied the technique only to relatively small examples. The applicability of the algorithm is limited by its non-elementary complexity. We believe that the algorithm can still be useful for practical purposes, since many formulae have small models. To substantiate this claim, and to further evaluate the performance of our approach, we plan to carry out some larger case studies, possibly from the area of cryptographic protocol verification [16,17].

We also plan to incorporate further optimizations [4,18], and to extend the translation to other Isabelle/HOL constructs: most notably the full language of HOL, including type operators [8], but also axiomatic type classes [20], inductively defined sets, and recursive functions.

An orthogonal approach that would be interesting to evaluate, both in terms of performance and feasibility, is the use of an external (first-order) model generator. The necessary translation from HOL to first-order logic could be based on recent work by Meng and Paulson [12].

Acknowledgments The author would like to thank Martin Strecker, Tobias Nipkow and the anonymous referees for their valuable comments.

References

[1] Peter B. Andrews. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, volume 27 of Applied Logic Series. Kluwer Academic Publishers, second edition, July 2002.

[2] Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL - lessons learned in formal-logic engineering. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, volume 1690 of Lecture Notes in Computer Science, pages 19–36. Springer, 1999.

[3] Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[4] Koen Claessen and Niklas Sörensson. New techniques that improve MACEstyle finite model finding. In CADE-19, Workshop W4, Model Computation – Principles, Algorithms, Applications, 2003.

[5] M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394–397, 1962.

[6] DIMACS satisfiability suggested format, 1993. Available from ftp://dimacs.rutgers.edu/pub/challenge/satisfiability/doc.

[7] E. Goldberg and Y. Novikov. BerkMin: A fast and robust SAT solver. In Design Automation and Test in Europe (DATE), pages 142–149, 2002.

[8] M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993.

[9] M. J. C. Gordon and A. M. Pitts. The HOL logic and system. In J. Bowen, editor, Towards Verified Systems, volume 2 of Real-Time Safety Critical Systems Series, pages 49–70. Elsevier, 1994.

[10] Daniel Jackson. Automating first-order relational logic. In Proc. ACM SIGSOFT Conf. Foundations of Software Engineering, pages 130–139, San Diego, November 2000.

[11] Paul Jackson and Daniel Sheridan. The optimality of a fast CNF conversion and its use with SAT. Technical Report APES-82-2004, APES Research Group, March 2004.

[12] Jia Meng and Lawrence C. Paulson. Experiments on supporting interactive proof using resolution. In David Basin and Michael Rusinowitch, editors, Automated Reasoning – Second International Joint Conference, IJCAR 2004, volume 3097 of Lecture Notes in Artificial Intelligence, pages 372–384. Springer, 2004.

[13] Robin Milner, Mads Tofte, Robert Harper, and David MacQueen. The Definition of Standard ML - Revised. MIT Press, May 1997.

[14] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proc. of the 38th Design Automation Conference, Las Vegas, June 2001.

[15] Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL – A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002.

[16] Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6:85–128, 1998.

[17] Graham Steel, Alan Bundy, and Ewen Denney. Finding counterexamples to inductive conjectures and discovering security protocol attacks. AISB Journal, 1(2), 2002.

[18] Tanel Tammet. Finite model building: improvements and comparisons. In CADE-19, Workshop W4, Model Computation – Principles, Algorithms, Applications, 2003.

[19] G. Tseitin. On the complexity of derivation in propositional calculus. In A. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, Part 2, pages 115–125, 1970.

[20] Markus Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy P. Felty, editors, Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, volume 1275 of Lecture Notes in Computer Science, pages 307–322. Springer, 1997.

[21] L. Zhang and S. Malik. The quest for efficient boolean satisfiability solvers. In Andrei Voronkov, editor, Proceedings of the 8th International Conference on Computer Aided Deduction (CADE 2002), volume 2392 of Lecture Notes in Computer Science. Springer, 2002.