Static analysis techniques have been studied for many years in the functional programming community, most prominently the use of inferred types to eliminate run-time checks. In analogy, if we regard checking whether an instance is useful for a proof as run-time checks and we can find types that eliminate irrelevant instances, we may also be able to prevent proof searches from checking those irrelevant instances, thereby improving the performance. This paper introduces a method that employs types as heuristics in proof search.
Introduction Instance-based theorem proving techniques have been implemented in many theorem provers: [1], [2], [3], [4], and [5], among others. Some of these provers have been shown to prove problems in some categories faster than or comparable to resolution-based theorem provers[6]. On the other hand, resolution-based theorem provers continue to lead on other problem categories. While instance-based theorem provers are believed to have a number of advantages, such as being capable of generating models for satisfiable problems and making use of the highly efficient SAT solvers, their run-time performance is suboptimal without guidance from instance generation heuristics such as resolution, semantics, etc..
Static analysis techniques in compilers, such as using types to eliminate runtime checks, have been studied for many years. In analogy, if we regard checking whether an instance is useful for a proof as run-time checks, then we may find types that prevent proof searches from checking some irrelevant instances, thereby improving the performance. In general, static analysis techniques generate heuristics from the input, in contrast to various static transformation techniques which preprocess the input. Following is a (incomplete) list of the techniques used in static analysis: Strategy Selection chooses a strategy that is believed to best suit the problem. Implementation: E[7], Vampire[8], and DCTP[5], among others. Restriction finds instances that may be pruned from the search space. Implementation: FM-Darwin[9], Paradox[10], and OSHL-S, among others. Ordering determines what kind of ordering can lead to contradiction faster.
Implementation: E(literal ordering), among others.
This paper introduces a method that employs inferred types from resolution as heuristics in first-order logic proof search. The general idea is deriving a type inference algorithm from a complete calculus, and using types to filter out a subset of instances that are not generated by the calculus by searching only welltyped instances. Properly designed types should bring some of the advantages from one method to another. 2
Notations
A vector is written as [a1, . . . , an], or vertically as in (
A Theory
An Example Example 1. S = {{P (X ), Q(f (X )}, {¬P (f (Y )), ¬Q(Y )}, {Q(a)}, {¬Q(f (f (a))}}. Since S is unsatisfiable, there exists a minimal (but not necessarily minimum) set S1 of ground instances of S that is unsatisfiable. By minimality of the instances in S1, for all ground literals N ∈ S S1, N ∈ S S1. For example, S1 = {{P (f (a)), Q(f (f (a))}, {¬P (f (a)), ¬Q(a)}, {Q(a)}, {¬Q(f (f (a)))}}. If we use a brute force method to find S1, then both X and Y are initiated to terms in x = {a, f (a), f (f (a)), . . .}. Our goal is to restrict the instantiation of variables to proper subsets of x given by a instantiation function I : Term → P (GrTerm). We establish a similar minimality requirement for I: for any literal N ∈ S and any ground instance N1 in I(N ), there exists L s.t. N1 ∈ I(L). Rewriting this requirement as an inequality of sets, we obtain: [ I(L) ⊃
[ I(L) L∈S S
L∈S S Informally speaking, all instances of literals in S should be resolvable. In the example, the only literal in S that is unifiable with P (X ) is ¬P (f (Y )). Therefore, any instance of P (X ) must have a complement, which must be an instance of ¬P (f (Y )). Hence I(¬P (f (Y ))) ⊃ I(P (X ))). If I(e) = {e[t/v]|ti ∈ I(vi), v = fv(e)}, then {f (t)|t ∈ I(Y )} ⊃ I(X ). We restrict the proof search by instantiating any variable v to elements of I(v), which we refer to as the semantics of the type of the variable v. 3.2
Algebra V In this section, we introduce an algebra V. The motivation of V is to enable simultaneously manipulating functions and sets, as in linear algebra. There are several groups of notations used in this paper. Algebra V: ρ, τ type; v variable; X term of the form [vi]in=1; A, A, B, F, G, H, T , T term. Mathematics: D domain; x, y set; f, g function; a, b, v vector; l, m, n, o, p natural number. Logic: u, v, X, Y variable; t term; e expression; L, N literal; C, D clause; S clause set; a, c, f function symbol.
Types are mainly used to define what terms are meaningful in V. To avoid the complexity of recursive domain equations, we define families of constructors indexed by natural numbers. The indices do not affect the mapping of the function that a term denotes, but the domain and range of that function. Definition 2. T : τ denotes that T is a term of type τ . τm,n = {m} → {n}. ∅n : {n} ∪n : {n} → {n} → {n} ∩n : {n} → {n} → {n} [] : {0}
p = m + n •m,n : {m} → {n} → {p} pi/n : {n} → {1}
v ⊃ f v(e) Λvn.e : {n} → {1}
v ⊃ f v(e) Λ−1vn.e : {1} → {n}
Sum ⊔m,n : τm,n → τm,n → τm,n FSum Inter ⊓m,n : τm,n → τm,n → τm,n FInter
p = m + n l,m,n : τl,m → τl,n → τl,p ◦m,n,p : τm,n → τn,p → τm,p Comp
v : {1}
T : ρ → τ T T ′ : τ T ′ : ρ
We use parentheses to delimit terms when ambiguous. We omit subscripts and superscripts indicating vector length and type indices when not ambiguous. There are two kinds of terms used in the paper: a term in the set Term and a term in V. We refer to the latter as a term of V to disambiguate only when necessary. T F unc is called a term function; RT F unc a reverse term function.
Let us now switch context to mathematical objects. As in domain theory, we say that a function f is continuous if x0 ⊂ x1 ⊂ . . . implies Si∞=0 f (xi) = f (Si∞=0 xi). Define ambn = [a1, . . . , am, b1, . . . , bn], x × y = {ambn|am ∈ x, bn ∈ y}, Qin=1 xi = x1 × (. . . × xn × {[]}), Si=1 xi = x1 ∪ . . . ∪ xn, Ti=1 xi = x1 ∩ n n . . . ∩ xn, and [xi]in=1 = [x1, . . . , xn]. For example, [a][f (a)] = [a, f (a)], {[a], [a′]} × {[f (a)]} = {[a, f (a)], [a′, f (a)]}. If we define Dn = {[xi]in=1|xi ∈ GrExpr}, then the domains Dτ are defined as follows, where [Dρ → Dτ ] is the set of functions from Dρ to Dτ .
D{n} = P(Dn) Dρ→τ = [Dρ → Dτ ]
interpretation is trivial if I(v) = ∅ for some variable v.
Given an interpretation I, the semantic function ()I∗ maps a term T : τ of V to an element of Dτ .
Definition 4. The semantic function ()I∗ is defined as follows. The semantics of function terms are given by partial evaluation.
(∅n)I∗ = ∅ (∪n)I∗(x)(y) = x ∪ y (∩n)I∗(x)(y) = x ∩ y
([])I∗ = {[]} (•m,n)I∗(x)(y) = x × y (pi/n)I∗(xn) = xi (Λv.e)I∗(x) = {e[t/v]|t ∈ x} (Λ−1v.e)I∗(x) = {t|e[t/v] ∈ x}
(λv.∅n)I∗(x) = ∅ (⊔m,n)I∗(f )(g)(x) = f (x) ∪ g(x) (⊓m,n)I∗(f )(g)(x) = f (x) ∩ g(x)
(λv.[])I∗(x) = {[]} ( l,m,n)I∗(f )(g)(x) = f (x) × g(x) (◦m,n,p)I∗(f )(g)(x) = f (g(x))
(v)I∗ = I(v) (F T )I∗ = (F )I∗((T )I∗) Notations such as ∅, ∪, ∩ are reused as both set-theoretical notations and terms of V. A term is variable-free if there is no subterm that is a variable. Since the denotations of variable-free terms are independent of I, we usually make I implicit when the term is variable-free. For example, (Λ[v1].f (v1))∗{[a]} = {[f (a)]}, (Λ−1[v1].f (v1))∗{[f (a)]} = {[a]}, (p1/2)∗{[a, f (a)]} = {[f (a)]}.
I |= T = T ′ if and only if (T )I∗ = (T ′)∗. T = T ′ if and only if it holds for all I I. A subset order is defined on set terms: I |= T ⊏ T ′ if and only if (T )I∗ ⊂ (T ′)∗. I The order is extended to functions I |= F ⊏ G if and only if for all terms T , I |= F T ⊏ GT . T ⊏ T ′ if and only if it holds for all I. The reverse is denoted by ⊐. F is continuous if and only if (F )I∗ is continuous for all I.
We write [Ti]in=1 = [T1, . . . , Tn] = T1 • . . . • Tn • [], [Fi]in=1 = [F1, . . . , Fn] = T1 . . . Tn λv.[]. We usually want to convert a vector to a term of the form [vi]in=1 and conversely, which we call algebraify and dealgebraify. If v is a vector of variables, then Av is a term v1 • . . . • vn • []; if X is a term of the form [vi]in=1, then A−1X = v. As a convention, we have X = Av and v = A−1X.
We make the following auxiliary definitions, where ve = fv(e), f is a function symbol of arity o, vf = [v1, . . . , vo], and Fn : {n} → {n} for some natural number n. Fn0 , ∪n∅n. Fnk+1 , FnFnk. f −1 , (Λ−1vf .f (v1, . . . , vo)). e , (Λve.e)Xe. I(e) , (Λve.e)∗I(ve). I(vn) , Qin=1 I(vi). For example, if f is binary, then f (X, Y ) = (Λ[X, Y ].f (X, Y ))[X, Y ], f −1 = Λ−1[X, Y ].f (X, Y ). We write binary functions as infix, for example, ⊔F G is written as F ⊔ G except for composition where we write ◦F G as F G.
It can be proved that (a) if F ⊐ G and F ⊐ H, then F ⊐ G⊔H; (b) F ⊔G ⊐ F and F ⊔ G ⊐ G; (c) (F ⊔ G)H = F H ⊔ GH; (d) F (G ⊔ H) = F G ⊔ F H; (e) [Fi]in=1T = [FiT ]in=1 (f) (λv.∅)F = λv.∅; (g) pi[Tk]k=1 = Ti, where i ∈ {1, . . . , n}. n 3.3
Constraints
substitutions Θ s.t. for every θ ∈ Θ,dom(θ) ⊃ f v(e). The instance set of e w.r.t. Θ is {xθ|θ ∈ Θ}. (b) An instantiation set of v induced by an interpretation I s.t. dom(I) ⊃ v is the set {[t/v]|t ∈ I(v)}. (c) An instantiation set is complete for a clause set S if the instances obtained from it are inconsistent. An interpretation is complete if the induced instantiation set is complete.
In this section we formalize the ideas discussed in Section 3.1 in terms of V . In the following discussion, S is a set of clauses s.t. ∅ ∈/ S and for any C, D ∈ S, f v(C) ∩ f v(D) = ∅.
Suppose that L, N ∈ S S and that σ is a well-formed mgu of L, N . We require that for every v ∈ f v(L), σ(v) 6= v, t = σ(v), v = fv(t) and for every u ∈ f v(L), σ(u) 6= u, t = σ(u), v = fv(t), v = vi,
I |= v ⊐ (Λv.t)X I |= v ⊐ pi(Λ−1v.t)u
I |= v ⊐ c
(
The apparent minimum solution to (
The algorithm for constraints generation (
common variables.
literal N in D such that N and L are unifiable by mgu σ, generate constraint
(
Denote the constraints generated by a clause set S by cons(S). If I makes a constraint true, then we say that I is a solution to the constraint. If any solution to constraints K is also a solution to constraints K′ and vice versa, then we say that K ≡ K′.
Next, we look at an example. Example 2. We choose g(X ) = f (a), g(Y ) = a and generate constraints for Example 1. Because P (X ) is unifiable with ¬P (f (Y )) with mgu [f (Y )/X ], the algorithm generates the following constraints I |= X ⊐ f (Y ), I |= Y ⊐ p1f −1X . Other constraints are generated similarly. We usually write the constraints in an equivalent but more compact form. I |= X ⊐ f (Y ) ∪ p1f −1(Y ) ∪ f (a), I |= Y ⊐ f (X ) ∪ p1f −1(X ) ∪ a. We also make I implicit when not ambiguous. Sometimes it is more compact to present a theory if we write inequality constraints in a vector normal form. For example, the constraints in Example 2 can be rewritten in the vector form:
I |= X ⊐ Λv.f (Y ) ⊔ p1Λ−1v.f (X )p2 ⊔ Λv.f (a) Λv.f (X ) ⊔ p2Λ−1v.f (Y )p1 ⊔ Λv.a
X , where X =
X
Y
(
I(v) = Si∞=0(Ai)∗∅. The rhs is a fixpoint of the function f (x) = (A)∗(x).
f v(D) = ∅, the binary resolvent D of two clauses C1 and C2 in S by some well-formed mgu, cons(S) ≡cons(S ∪ {D}).
f v(D) = ∅, any solution I to cons(S) is complete for S. 4
Context Free Type Generally speaking, I may have complicated structures. We need to find a finite representation for these sets that facilitates enumeration of terms, as one of the purposes of types is generating terms. By Theorem 1, A is a finite representation of the minimum solution of the constraint, but it is not very efficient as it includes 1 A long version of this paper can be found at http://cs.unc.edu/~xuh/oshls. RT F uncs which require pattern matching. Besides, it is also hard to generate terms in certain order, say, the size-lexicographic order. The approach introduced in this section converts the constraints into a grammar that produces a solution without RT F uncs.
Given a F P rod A = [Ai]in=1 in the normal form, for any component A of A, we denote the F Sum of T F unc or F SumU nit by A→, and the F Sum of other n terms (which contain RT F uncs) by A←, for example, A→ = Si=1(Λv.ti) and n A← = Si=1 pi(Λ−1v.ti)pi. Using this notation, an inequality can be written in the following form.
X ⊐ (A→ ⊔ A←)X
(
piΛ−1v.f (vi)Λv.a = λv.∅ .
We generalize the idea illustrated in Example 3. A←A→ can be expanded to an F P rod of F Sum of terms of the form pk(Λ−1v.t)(Λv.t′) or λv.∅. In general, not all terms of the form pk(Λ−1v.t)(Λv.t′) can be converted to a simpler, equal term. The inequalities shown as follows, where ll′ ∈ Pos, l ∈ Pos, can be used to simplify them to simpler terms.
pk(Λ−1v.t′′)pk′ σ = mgu(t′, t), σ(vk) = vk, pk(Λ−1v.t)(Λv.t′) ⊏
vk ∈ f v(t′′), t′′ = σ(vk′ ) ∈/ Var Λv.t′′ λv.∅ σ = mgu(t′, t), σ(vk) = t′′ t′, t not unifiable For example, if v = [X, Y ], then p1(Λ−1v.f (f (X)))(Λv.f (Y )) ⊏ p1(Λ−1v.f (X))p2, p1(Λ−1v.f (X))(Λv.f (f (Y ))) ⊏ Λv.f (Y ), p1(Λ−1v.f (f (X)))(Λv.a) ⊏ λv.∅. If two simplifications are applicable simultaneously, then we choose one arbitrarily. The reduced term can be rearranged into an equal normal form. If the original term is T, then we denote the normal form of the reduced term by s(T). s(T) ⊐ T for any T.
B0 = A Bk+1 = Bk ⊔ s(Bk←Bk→)
s.t. BN = BN+1.
Lemma 2. Si∞=0(BiN )∗∅ = Si∞=0((BN→)i)∗∅.
Theorem 4. (Soundness) If I(v) = Si∞=0((BN→)i)∗∅, then I |= X ⊐ AX. Unlike A, B→ does not contain RT F uncs. Constraint X ⊐ B→X can be
N N
straightforwardly converted to BNF productions by syntactically converting "∪"
to "|" and "⊐" to "→". The resulting grammar generates the solution I.
Example 4. Suppose (
Λv.X Λv.Y ⊔ Λv.a (b) p1Λ−1v.f (X )p2 ⊔ Λv.f (Y ) ⊔ Λv.f (a) ⊔ Λv.X p2Λ−1v.f (Y )p1 ⊔ Λv.f (X ) ⊔ Λv.a ⊔ Λv.Y
(a) X ⊐ f (Y ) ∪ f (a) ∪ X Y f (X ) ∪ a ∪ Y (c)
X → f (Y )|f (a)|X Y → f (X )|a|Y (d) 5
Related Work The (Inst-Gen) rule introduced in [11] uses unification as guide for instance generation. The algorithms presented in [12] also make use of unification to find blockages. [13] shows that using a proper semantics for OSHL is implicitly performing unification. One of the differences between our approach and others is that we infer types before proof search, which divides a theorem proving algorithm into the static analysis stage and the run-time stage. About clause linking, we have the following observation(probably others also have the same observation): in order for any instance Cσ of C to be useful, each literal Lσ in Cσ should be resolvable with some other literals. Given a set of clauses S, a clause C, and a literal L in C, we may decompose C on L w.r.t. S to a set of instances of C, {Cσi|i ∈ {1, 2, . . . , n}}, s.t. for any literal N in S, σi is an mgu of L and N for some i ∈ {1, 2, . . . , n} without affecting the completeness. Our approach generates criteria inspired by this observation. For a survey of instance-base methods, refer to [14].
Sort inference algorithms are implemented in some finite model finders such as Paradox[10] and FM-Darwin[9]. Sorted unification[15] uses sets of unary predicates as sorts. A key difference between our approach and multi-sorted logic is that the types are inferred from S, instead of being part of the logic itself. Therefore, we need to guarantee that the types inferred are backward compatible with the untyped version S. Theorems in this paper is essential for our approach but irrelevant to a multi-sorted logic without inferred sort. Our approach can be viewed as a type system[16] that is equipped with a type inference algorithm. The difference between our type system and those that are usually found in programming languages is that our type system is used to restrict instance generation while type systems in programming languages are usually used to eliminate expressions whose reduction leads to errors. In advanced compilers, some type systems are also used to guide optimization, in which sense it is similar to our type system. The presentation of this paper makes (very primitive) use of domains[17] and is loosely related to a type theory[18] in the sense that a type system is related to a type theory.
A closely related concept to grammar is tree grammar, where the rhs is composed of trees instead of sequences. The choice of grammar reflects the fact that terms can be internally represented by sequences instead of trees. 6
Discussion
It is possible to refine the constraints (
The granularity of types is the key to the efficacy of these types. CFT is useful for some problems as shown in Table 1.2 Finer granularity may be achieved by using enhanced grammars. These grammars are useful when a variable occurs twice in a literal, for example, P (f (X, X)). If we have a literal ¬P (Y ), then productions produced by CFT include Y → f (X, X) which does not reflect the correlation between the two occurrences of X. If we make use of an enhanced grammar to mark that X should always be instantiated to the same term, then we have better approximation to the minimum solution. A possible solution is adding correlation markers to correlated variables.
The constraints generated by CFT may have redundancy which affects the
time and space complexity of the term generator. We implemented the following
algorithms to reduce redundancy. Suppose that X ⊐ T, where X = [vk]k=1, T =
n
[Tk]kn=1, Ti = Ssm=1 Ti,s, i ∈ {1, 2, . . . , n}. In each iteration of Algorithm 2, if
Ti,o = vj and Tj,p = vi, then put vi, vj into an equivalence class; choose a
representative for each equivalence class; for every representative vi and vj 6= vi
in the equivalence class, set Ti to Ti ∪ Tj and Tj to vi and replace vj by vi in
T; and for every Ti s.t. Ti,o = vi for some o, remove vi from Ti. A variable is
nontrivial if the rhs of its production contains a term containing only variables
that are nontrivial. We slightly modify constraint (