11. Search

Following Miller [10] and Berger, we have implemented a proof search algorithm for minimal logic. To enforce termination, every assumption can only be used a fixed number of times.

We begin with a short description of the theory involved.

Q always denotes a ∀∃∀-prefix, say ∀∃∀, with distinct variables. We call the signature variables, the flexible variables and the forbidden variables of Q, and write Q_∃ for the existential part ∃ of Q.

Q-terms are inductively defined by the following clauses.

• If u is a universally quantified variable in Q or a constant, and are Q-terms, then u is a Q-term.
• For any flexible variable y and distinct forbidden variables from Q, y is a Q-term.
• If r is a Q∀z-term, then λzr is a Q-term.

Explicitely, r is a Q-term iff all its free variables are in Q, and for every subterm y of r with y free in r and flexible in Q, the are distinct variables either λ-bound in r (such that y is in the scope of this λ) or else forbidden in Q.

Q-goals and Q-clauses are simultaneously defined by

• If are Q-terms, then P is a Q-goal as well as a Q-clause.
• If D is a Q-clause and G is a Q-goal, then D → G is a Q-goal.
• If G is a Q-goal and D is a Q-clause, then G → D is a Q-clause.
• If G is a Q∀x-goal, then ∀xG is a Q-goal.
• If D[y:=Y ] is a ∀∃,Y ∀-clause, then ∀yD is a ∀∃∀-clause.

Explicitely, a formula A is a Q-goal iff all its free variables are in Q, and for every subterm y of A with y either existentially bound in A (with y in the scope) or else free in A and flexible in Q, the are distinct variables either λ- or universally bound in A (such that y is in the scope) or else free in A and forbidden in Q.

A Q-sequent has the form 𝒫⇒ G, where 𝒫 is a list of Q-clauses and G is a Q-goal.

A Q-substitution is a substitution of Q-terms.

A unification problem 𝒰 consists of a ∀∃∀-prefix Q and a conjunction C of equations between Q-terms of the same type, i.e. ∧ ∧ _i=1ⁿr_i = s_i. We may assume that each such equation is of the form λr = λs with the same (which may be empty) and r,s of ground type.

A solution to such a unification problem 𝒰 is a Q-substitution ϕ such that for every i, r_iϕ = s_iϕ holds (i.e. r_iϕ and s_iϕ have the same normal form). We sometimes write C as = , and (for obvious reasons) call it a list of unification pairs.

We work with lists of sequents instead of single sequents; they all are Q-sequents for the same prefix Q. One then searches for a Q-substitution ϕ and proofs of the ϕ-substituted sequents. intro-search takes the first sequent and extends Q by all universally quantified variables x₁…. It then calls select, which selects (using or) a fitting clause. If one is found, a new prefix Q′ (raising the new flexible variables) is formed, and the n (≥ 0) new goals with their clauses (and also all remaining sequents) are substituted with star∘ ρ, where star is the “raising” substitution and ρ is the mgu. For this constellation intro-search is called again. In case of success, one obtains a Q′-substitution ϕ′ and proofs of the star∘ ρ ∘ ϕ′ -substituted new sequents. Let ϕ := (ρ ∘ ϕ′)↾Q_∃, and take the first n proofs of these to build a proof of the ϕ-substituted (first) sequent originally considered by intro-search.

Compared with Miller [10], we make use of several simplifications, optimizations and extensions, in particular the following.

• Instead of arbitrarily mixed prefixes we only use those of the form ∀∃∀. Nipkow in [11] already had presented a version of Miller’s pattern unification algorithm for such prefixes, and Miller in [10, Section 9.2] notes that in such a situation any two unifiers can be transformed into each other by a variable renaming substitution. Here we restrict ourselves to ∀∃∀-prefixes throughout, i.e. in the proof search algorithm as well.
• The order of events in the pattern unification algorithm is changed slightly, by postponing the raising step until it is really needed. This avoids unnecessary creation of new higher type variables. – Already Miller noted in [10, p.515] that such optimizations are possible.
• The extensions concern the (strong) existential quantifier, which has been left out in Miller’s treatment, and also conjunction. The latter can be avoided in principle, but of course is a useful thing to have.

(search m (name1 m1) ...) expects for m a default value for multiplicity (i.e. how often assumptions are to be used), for name1 …

• numbers of hypotheses from the present context or
• names for theorems or global assumptions,

and for m1 ...multiplicities (positive integers for global assumptions or theorems). A search is started for a proof of the goal formula from the given hypotheses with the given multiplicities and in addition from the other hypotheses (but not any other global assumptions or theorems) with m or mult-default. To exclude a hypothesis from being tried, list it with multiplicity 0.