Rev: 01968

RR9

RIA
laboria

laboratoire de recherche
en informatique
et automatique

A Mechanization
of Type Theory

Gerard P. Huet

Institut de Recherche
d'Informatique
et d'Automatique

Domaine de Voluceau
Rocquencourt
78150 - Le Chesnay
Tél. 954.90.20

Rapport de Recherche n° 9

février 1973
A MECHANIZATION OF TYPE THEORY

Gérard P. HUET

Présenté par Maurice Nivat

ABSTRACT

A refutational system of logic for a language of order ω is presented. This language is a slight modification of Church's λ-calculus with types. The system is complete, in the sense that a refutation of a set of sentences exists if and only if this set does not possess a general Henkin model. The main rule of inference is a generalization of Robinson's resolution to type theory, which allows us to get rid of the substitution rule.

DESCRIPTIVE TERMS :

- Automatic theorem proving

- Mathematical logic

- Proof procedures

- Resolution principle

- Higher order logic

- Type theory

- Lambda calculus

- Unification algorithms

--- § ---
UNE MECANISATION DE LA THEORIE DES TYPES

RÉSUMÉ

CE PAPIER PRESENTE UN SYSTEME REFUTATIONNEL POUR UNE
LOGIQUE D'ORDRE $\omega$.

Le langage utilisé est une légère modification du
$\lambda$-calcul typé de Church. Ce système est complet au sens de
Henkin, c'est-à-dire qu'un ensemble de propositions peut être
réfuté si et seulement s'il ne possède pas de modèle de Henkin.
La principale règle de déduction est une généralisation à la
théorie des types de la règle de résolution de Robinson, ce qui
nous permet de nous passer de règle explicite de substitution.
ACKNOWLEDGMENTS

This paper presents results contained in the author's Ph.D.
thesis at Case Western Reserve University, under the direction of
Pr G. W. ERNST. This research was supported by the National Science
Foundation under Grant n° GJ - 1135.
# INTRODUCTION

During the last decade, a lot of effort in automatic theorem proving has been devoted to mechanizing first-order logic. The main achievement has been the definition by J. A. Robinson (1965) of a now well-known refutational first-order system. Its unique rule of inference, called resolution, is an elegant way of combining the substitution and cut rules. The other familiar rules of inference are implicitly taken care of by Skolemization and the set representation (clauses) of the conjunctive normal form of the set of sentences one wants to refute. More precisely, resolution permits us to select just the substitutions which are necessary for the cut of two literals. Moreover, if this cut is possible at all, only one such substitution is sufficient, called the most general unifier of the two literals. This existence of a most general unifier between two terms in first-order logic is fundamental to the resolution method.

Many a theorem proving program was written based on the resolution rule, embodying various heuristics to speed up the search for a refutation. However, results obtained so far are still too limited to permit any really useful application. To remedy this situation, some workers in the field, notably Robinson (1969) have argued for the exploration of more powerful systems of logic such as Church's $\lambda$-calculus.

# HIGHER ORDER UNIFICATION

The situation in higher order logic is quite different from first order. Most general unifiers do not exist any more (Gould 1966). Consider for instance the two terms :
$$t_1 = f(x)$$
and $$t_2 = A$$

Where $f$ is a (second-order) variable, $x$ is a variable and $A$ a constant. The following substitutions are two independent unifiers of $t_1$ and $t_2$:

$$\sigma_1 = \{f \leftarrow \lambda u \cdot A\}$$
$$\sigma_2 = \{f \leftarrow \lambda u \cdot u, x \leftarrow A\}$$

We may even need to consider an infinity of unifiers. Let us say that substitution $\sigma$ is less general than substitution $\rho$ if there exists $\eta$ such that:

$$\sigma = \eta \circ \rho$$

We shall denote this relation (which is reflexive and transitive) by : $\sigma \prec \rho$. Now we call complete generator of unifiers for terms $t_1$ and $t_2$ (CGU in short) any set $\Sigma$ of substitutions such that:

$$\begin{cases} 1^{\circ} \forall \sigma \in \Sigma : \sigma \text{ unifies } t_1 & \text{and } t_2. \\ 2^{\circ} \forall \sigma \text{ unifier of } e_1 & \text{and } e_2 : \exists \rho \in \Sigma \text{ such that } \sigma \prec \rho. \end{cases}$$

Gould (1966) has shown that certain pairs of terms $t_1$, $t_2$ do not possess a finite CGU. Consider for instance:

$$\begin{cases} t_1 = f(x, A) \\ t_2 = f(x, B) \end{cases}$$

where $x$ is a (variable) function and $f$ is a (variable) functional. Now let $\Sigma = \{\sigma_i | i \ge 0\}$, with:

$$\begin{align*} \sigma_0 &= \{f \leftarrow \lambda u \cdot h(u)\} \\ \sigma_n &= \{f \leftarrow \lambda u \cdot g_n(u, u(h_1(u, v)), \dots, u(h_n(u, v))), \\ & \phantom{=} x \leftarrow \lambda u \cdot z, y \leftarrow \lambda u \cdot z\} \quad (n > 0) \end{align*}$$
The proof can be sketched as follows :

1. $\Sigma$ is a CGU for $t_1$ and $t_2$

2. $\sigma_i < \sigma_{i+1} \quad \forall i > 0$

3. not $\sigma_{i+1} < \sigma_i \quad \forall i > 0$

4. not ($\sigma_0 < \sigma_i$ or $\sigma_i < \sigma_0$) $\forall i > 0$

5. suppose $\Sigma'$ is a finite CGU for $t_1$ and $t_2$. By 1. this implies that there exists $\Sigma'' \subset \Sigma$ finite CGU for $t_1$ and $t_2$. This contradicts obviously 3. and 4. (Consider $\sigma_{k+1}$, with $k = \max\{i | \sigma_i \in \Sigma''\}$). Thus, although any finite subset of $\Sigma$ can be generated by only two elements (using 2.), we cannot find a finite set of generators for the unifiers of $t_1$ and $t_2$.

It seems therefore that an extension of resolution to type theory would require generating a possibly infinite number of resolvents at every application of the resolution rule. One solution to this problem would be to order these resolvents (for instance according to some complexity of the unifier selected) and to "dove-tail" the generation of resolvents with the refutation search algorithm. This method has been proposed and proved complete by Pietrzykowski and Jensen (1972).

However the inefficiency of such dove-tailing processes is well known and its practical implementation seems difficult. We shall present here a method which, although it ultimately leads to a double enumeration too, delays the generation of unifiers as much as possible and thus minimizes the number of irrelevant choices.
CONSTRAINTS

The idea is to represent the set of unifiers of two literals L₁ and L₂ as a condition tagging the resolvent obtained by cutting L₁ and L₂ in their respective clauses. Such a condition is expressed as a set of "constraints" of the form {t₁, t₂} where t₁ and t₂ are subterms of L₁ and L₂. More generally, a constraint will be a set of terms which we want to unify. A clause tagged by a set of constraints will be represented as

$$L_1, L_2, \dots, L_n/C_1, C_2, \dots, C_p$$

where the Lᵢ's are the literals of the clause and the Cⱼ's are constraints. Such a "constrained clause" (CC in short) represents the set of all clauses σ∘L₁, σ∘L₂, ..., σ∘Lₙ such that σ unifies simultaneously every constraint Cᵢ; i.e., if Cᵢ = {e₁, e₂, ..., eₚ} then σ∘e₁ = σ∘e₂ = ... = σ∘eₚ (1 ≤ i ≤ p).

In many cases we will be able to decide if a constraint is not unifiable at all, in which case the corresponding CC is not generated. We may also know a most general unifier σ for the constraint, in which case σ is applied to the corresponding resolvent, tagged with the union of the constraints in the CCs resolved upon. Otherwise we generate the CC obtained by tagging the resolvent with the union of the parents' constraints plus the new one. In the last two cases we check that the set of constraints is not obviously inconsistent. Let us now give an example.
We suppose that we have two basic types : o for truth values and i for individuals. We shall use the following atoms, indicated with their type :

w, A i

v, y, B, C (i → i)

x, z, u ((i → i) → i)

f (((i → i) → i) → i)

P, R (i → o)

Q (i, (i → i) → o)

By convention, all lower case letters denote variables, all capitals denote constants. Of course ($α_1, α_2, ..., α_n → β$) denotes the type of functions of n arguments of types $α_1, ..., α_n$ and with range of type $β$. We consider the set $S$ of clauses :

$$1. P(f(x)), Q(z(C), C), R(f(z))$$

$$2. \neg P(A)$$

$$3. \neg Q(y(A), y)$$

$$4. \neg R(B(w))$$

We shall prove by constrained resolution that this set is unsatisfiable (the precise statement of the rule of constrained resolution will be given below).

First we resolve the P's in 1° and 2°. We are trying to unify $P(f(x))$ and $P(A)$, and this implies the unification of $f(x)$ and $A$. These terms do not possess a most general unifier, so we generate a constraint {$f(x), A$} which is tagged to the resolvent :

$$5. Q(z(C), C), R(f(z)) / \{f(x), A\}.$$
Now we resolve the Q's in 5° and 3°, which implies the simultaneous unification of :

firstly $y(A)$ and $z(C)$

and secondly $y$ and $C$. Fortunately in the second pair $\{y \leftarrow C\}$ is a most general unifier. This unifier transforms the first condition into the unification of $C(A)$ and $z(C)$. Here too there is no MGU, so we generate the resolvent :

$$6^{\circ} R(f(z)) / \{f(x), A\}, \{C(A), z(C)\}.$$

Finally we get the empty clause, resolving 6° and 4°, and generating one more constraint $\{B(w), f(z)\}$ :

$$7^{\circ} \Phi / \{f(x), A\}, \{C(A), z(C)\}, \{B(w), f(z)\}.$$

Now, in order to validate our refutation, we must find a unifier satisfying simultaneously every constraint in 7°. However any unifier will do here, we do not need to generate a complete set of them. Actually, we just need to check for the existence of a unifier. Unfortunately there is no decision procedure for this task if we allow quantification over third order functionals, as shown in Huet (1973). All we can do here is to use a semi-decision algorithm of reasonable efficiency developed for this problem in Huet (1972). We shall not present this algorithm here, but merely indicate that for our example it would return an affirmative answer, with the unifier :

$$\begin{cases}
f \leftarrow \lambda u \cdot u(B) \\
z \leftarrow \lambda v \cdot v(A) \\
w \leftarrow A \\
x \leftarrow \lambda v \cdot A
\end{cases}$$
The reader will check that this substitution (together with $y \leftarrow C$) applied to S gives a contradictory set of ground clauses.

The general case is a little more complicated because, when resolving two CCs, each of which has a non-empty set of constraints, we have to merge these two sets.

Note also that when we apply a substitution to a CC we must apply it to its constraints as well, which may induce some possible simplifications, merging of constraints and rejections.

A more serious complication arises with the use of pre-dicate variables. A literal whose predicate is a variable may be transformed into several literals by substitution of a disjunction for the variable. For instance the clause $p(A), S(B)$ becomes

$q(A), r(A), S(B)$ after the substitution

$p \leftarrow \lambda u \cdot (q(u) \lor r(u))$ and passage to normal form. Similarly, the substitution of a corresponding conjunction will produce two clauses :

$q(A), S(B)$

and $r(A), S(B)$.

Also, substituting a quantified formula for $p$ would oblige us to Skolemize during the proof.

For these reasons we are obliged to introduce a second rule of inference, called splitting, which in effect simulates all possible ways of effecting these substitutions for predicate variables, using the mechanism of the constraints.
We shall now give the precise formulation of our rules of inference.

## REFUTATIONS

We shall not state formally the definitions of terms, literals, etc... The precise definitions are stated in Huet (1972, 1973). Let us just recall that our language is basically Church's $\lambda$ - calculus with types (Church 1940). Every term possesses a normal form :

$$ \lambda u_1 \dots u_n \cdot a(e_1, \dots, e_p) $$

where the $u_i$'s are variables, $a$ is an atom (called the head of the term) and the $e_j$'s are terms (see Andrews 1971). Functional extensionality is an option in the system. We shall distinguish three special constants $\neg \vee$ and $\pi$ of the appropriate types. They will denote respectively negation, disjunction and universal quantification. For the last one, we represent $\forall x \cdot a$ by $\pi(\lambda x \cdot a)$. Actually for each type $\alpha$ is a $\pi_\alpha$ of type $((\alpha \to o) \to o)$, denoting quantification over variables of type $\alpha$.

We suppose moreover that the set of sentences one wants to refute has been reduced to clause form. This means in particular that we have Skolemized as much as we could. Of course, it is forbidden to reduce propositions which are hidden inside the arguments of some literal. Our Skolemization consists in replacing (at the top level) :

- $\pi_\alpha(a)$ by $a(x)$ where $x$ is a new variable of type $\alpha$

- $\neg \pi_\alpha(a)$ by $\neg a(E_\alpha(a))$ where $E_\alpha$ is a special constant (called a parameter) of type $((\alpha \to o) \to \alpha)$.
After reduction, every clause will be represented as
a finite set of literals, each literal being of the form A or $\neg A$,
where A is a term $P(e_1, e_2, ..., e_n)$ and P is an atom different
from $\neg V$ and $\pi$.

Let us now give more precisely the definition of CC.

A *constraint* is any finite set {$e_1, e_2, ..., e_n$} of terms
of the same type. A substitution $\sigma$ is said to unify this constraint
if and only if $\sigma$ is a unifier for $e_1, e_2, ..., e_n$. It is said to uni-
fy a set of constraints {$C_1, C_2, ..., C_p$} if and only if it unifies
every $C_i$ ($1 \le i \le p$). A *constrained clause* $E/C$ consists of a clau-
se $E$ and of a finite set of constraints $C$. If $C = \emptyset$ we have an ini-
tial CC, if $E = \emptyset$ we have a terminal CC, $\Box = \emptyset/\emptyset$ is the empty CC.

In order to refute a set of sentences S, we first reduce
it to clause form as explained above, then we tag to every clause
the empty set of constraints $\emptyset$.

A refutation is any derivation from this set of initial
CCs, using the three rules of inference defined below and ending
with the empty CC. If such a refutation exists, we say that S is
refutable.

The first two rules of inference, constrained resolution
and splitting, apply to non-terminal CCs whereas the third one, uni-
fication, applies to terminal CCs. Constrained resolution is binary,
splitting and unification are unary rules.
## 1 - Constrained resolution

Let $E_1 = A_1/B_1$ and $E_2 = A_2/B_2$ be two non-terminal CCs. Let $\{x_1, x_2, ..., x_n\}$ be all the variables that appear free in both $E_1$ and $E_2$, and $\{w_1, w_2, ..., w_n\}$ be new variables of the same types which do not appear in either $E_1$ or $E_2$. We define the substitution :

$$ \theta = \{x_i \leftarrow w_i \mid 1 \le i \le n\} $$

Now we distinguish p positive literals in $A_1$, and q negative literals in $A_2$. That is, using $\cup$ to denote disjoint union :

$$ A_1 = \{M_1, M_2, ..., M_p\} \cup A_3 \quad p \ge 1 $$

$$ A_2 = \{\neg N_1, \neg N_2, ..., \neg N_q\} \cup A_4 \quad q \ge 1 $$

Now let

$$ B_3 = \{M_1, M_2, ..., M_p, \theta_0 N_1, \theta_0 N_2, ..., \theta_0 N_q\} $$

We say that the CC :

$$ E_3 = A_3 \cup \theta_0 A_4 / B_1 \cup \theta_0 B_2 \cup B_3 $$

follows by constrained resolution from CCs $E_1$ and $E_2$.

## 2 - Splitting

Let $E_1 = A/C$ be any non-terminal CC, such that A contains a literal L whose predicate is a variable ; i.e. $A = B \cup \{L\}$. We have the following cases :

1. If L is a positive literal :

$$ 1-1 \text{ Deduce } E_2 = B \cup \{q,r\} / C \cup \{\{L, q\}, \{\{L, r\}\}\} $$

where q and r are new variables of type o.

$$ 1-2 \text{ Deduce } E_2 = B \cup \{\neg q\} / C \cup \{\{L, \neg q\}\} $$

where q is a new variable of type o.
$$1-3 \text{ Deduce } E_2 = B \cup \{q(z)\} / C \cup \{{\tt L}, \pi_\alpha q\}$$

where z is a new variable of type α, q is a new variable of type (α → o).

2. If L is a negative literal; i.e. $L = \neg M$:

$$2-1 \text{ Deduce } E_2 = B \cup \{\neg q\} / C_1$$

$$\text{and } E_3 = B \cup \{\neg r\} / C_1$$

where $C_1 = C \cup \{{\tt M}, \neg q\}$, q and r are new variables of type o.

$$2-2 \text{ Deduce } E_2 = B \cup \{q\} / C \cup \{{\tt M}, \neg q\}$$

where q is a new variable of type o.

$$2-3 \text{ Deduce } E_2 = B \cup \{\neg q(E_\alpha(q))\} / C \cup \{{\tt M}, \pi_\alpha q\}$$

where q is a new variable of type (α → o).

Any of the above COs is said to be deducible from $E_1$ by splitting.

Rules 1-3 and 2-3 are not effective, because they depend on some arbitrary type α. They can be made effective in an obvious way by restricting α to some initial segment of types.

### 3 - Unification

Let $E = \emptyset / C$ be a terminal CC. If C is unifiable, we can deduce $\Box$ from E.

This rule too is not effective. We can make it so by putting a bound on the member of steps of our unification algorithm. For this reason our method may ultimately lead to a double enumeration.
## Soundness and completeness

### logic

It is well known that higher order is not complete, under the usual semantic characterization (Godel models). However, Henkin (1950) has shown that a different characterization yields completeness in w-order logic. The trick is to interpret predicate variables of type $(\alpha \to o)$ (for instance) over domains which may be proper subsets of $2^{\mathcal{A}}$, calling $\mathcal{B}_{\alpha}$ the domain of interpretation of objects of type $\alpha$. We only impose that these domains be closed under operations corresponding to the different constructs of the language (for instance complementation, projection, etc...). In the same way $\mathcal{B}(\alpha \to \beta)$ may be a proper subset of $\mathcal{B}_{\alpha} \to \mathcal{B}_{\beta}$.

This enlarged semantic characterization (general Henkin models) permits us to restrict validity to just those formulas which are derivable in the logic.

In the following, we shall therefore use satisfiable as an abbreviation for "has a general Henkin model".

**Definition**: A property $\Gamma$ of finite sets of propositions is called an analytic consistency property if and only if, for any finite set $S$ of propositions, we have $(\gamma_1)$ to $(\gamma_7)$ below.

$(\gamma_1)$ if $\Gamma(s)$, then there is no literal $a$ such that $a \in S$ and $\Gamma \in S$.

$(\gamma_2)$ if $\Gamma(s \cup \{a\})$, then $\Gamma(s \cup \{a'\})$, where $a'$ is the $\lambda$ normal form of $a$.

$(\gamma_3)$ if $\Gamma(s \cup \{\lambda a\})$, then $\Gamma(s \cup \{a\})$.

$(\gamma_4)$ if $\Gamma(s \cup \{a \lor \beta\})$, then $\Gamma(s \cup \{a\})$ or $\Gamma(s \cup \{\beta\})$.
(γ₅) if Γ(s ∪ {¬(αβ)}), then Γ(s ∪ {α,¬β}).

(γ₆) if Γ(s ∪ {π<sub>α</sub>}), then for every term β of type α, Γ(s ∪ {π<sub>α</sub>, α(β)}).

(γ₇) if Γ(s ∪ {π<sub>α</sub>}), then Γ(s ∪ {¬α(X)}) for any constant or variable X of type α which does not occur free in α or s.

We are interested in analytic consistency properties because they provide a sufficient condition for satisfiability, as expressed by the following lemma from Andrews (1971).

**Lemma I.** If Γ is any analytic consistency property and s is a finite set of propositions such that Γ(s), then s is satisfiable.

For any set C of propositions, let C' be the set of sentences (closed propositions) obtained from C by replacing free variables by new constants in a one to one fashion. Obviously if C is unsatisfiable then C' is unsatisfiable too. Now we define the following property Γ of sets of propositions :

Γ(C) if and only if C' is not refutable.

**Lemma II.** Γ is an analytic consistency property. The proof of this lemma is given in Huet (1972). The idea is to prove each of (γ₁) to (γ₇) by proving the contrapositive statement about refutations. For instance, to prove (γ₁), let us assume that there exists a literal a such that a ∈ s and ¬a ∈ s. This implies that in the clause form of s' there are clauses {a'} and {¬a'}. Therefore from s' we can deduce CC φ/,{a',a'}}, from which we deduce □ by trivial unification. s' being refutable, we have not Γ(s) by definition of Γ. Taking the contrapositive statement we get (γ₁).
Now let $\mathfrak{S}$ be any unsatisfiable set of sentences. By lemma I and lemma II : not $\Gamma(\mathfrak{S})$ and by definition of $\Gamma \mathfrak{S}$ is refutable. This gives us the completeness of our system. The soundness is obtained by mapping refutations in our system into Andrews' $\mathfrak{R}$ system (Andrews 1971), known to be sound. Again a proof can be found in Huet (1972). Combining the two, we get the theorem :

**Theorem.** Let $\mathfrak{S}$ be any finite set of sentences. $\mathfrak{S}$ is unsatisfiable if and only if it is refutable.

**Remarks.** In our formal presentation of the rules of inference, we have supposed that we were not trying to unify at all when resolving, instead we just generated constraints. The processing of the literals candidates for unification and the checking for consistency of the constraints obtained is not necessary in theory, and it was more convenient to use this formalism for our proofs. However, as it was shown in our example above it is highly desirable in practice to do some amount of processing when applying constrained resolution. Of course this does not affect the soundness or completeness of the system. There is a trade-off here between many useless but fast derivations and few useless but slow ones, and it is difficult to estimate how much processing of constraints should be done until the system is implemented.

In the case where the set of initial clauses is first-order it is possible to process completely every constraint, and splitting is not applicable. Our system reduces exactly to resolution in this case.
It should be noted that we have not assumed extensio-
nality so far since Henkin models may not be extensional, as noted
by Andrews (1972). However we have in option a unification algorithm
which assumes the weak extensionality axiom :

$$
f = \lambda x \cdot f(x)
$$

We shall now present a few examples of refutations. We
have replaced the cumbersome existential parameters E(λx·α) by usual
Skolem functions X(y₁, ..., yₙ), the yᵢ's being the free variables of α.

EXAMPLES

Example 1

Cantor's theorem : $N^N$ is not denumerable.

Let i be the type "integer", n, f and h be variables,
with τ(n) = i, τ(f) = (i → i) and τ(h) = (i, i → i). We shall refute
the negation of Cantor's theorem : "it is possible to enumerate the
functions of integer to integer", i.e.

gh \Vf \Gn h(n) = f

After reduction to normal form we get, using N and H as
Skolem functions, τ(N) = ((i → i) → i), τ(H) = (i, i → i) :

1 HNf = f

We shall need the following property of equality :

2. $\neg f = g, fn = gn \ [\tau(g) = (i \to i)]$

and the existence of a successor function S satisfying :

3. $\neg n = Sn \quad [\tau(S) = (i \to i)]$
The refutation goes as follows :

$$
R(1,2) \quad 4 \quad \mathrm{H}(\mathrm{Nf},n) = \mathrm{fn}
$$

$$
R(4,3) \quad 5 \quad \Phi / \{fn, SH(Nf,n)\}
$$

$$
U(5) \quad 6 \quad \Box \text{ by substitution : } \{f \leftarrow \lambda u \cdot SH(u,u), n \leftarrow N(\lambda u \cdot SH(u,u))\}
$$

Note that the constraints coming from the first cons-
trained resolution can be completely processed, so that $C_4 = \emptyset$.
This short proof (3 steps) is due to a concise representation of the
problem. In particular, use of type i for integers gives us impli-
citly restricted quantification over integers without having to
carry additional literals.

Example 2

The pigeonhole principle : if we distribute n + 1 ob-
jects into n holes, there is at least one hole which contains more
than one object.

We choose type $\alpha$ for the set A of objects and type $\beta$
for the set B of holes. The hypothesis is :

$$
|B| < |A| < \omega
$$

1° $|B| < |A|$ : there exists a one-one mapping from B
to A, not onto.

2° $|A| < \omega$ : every one-one mapping from A to A is onto.

The conclusion is : there is no one-one mapping from
A to B.

Using the following atoms :

$$
\tau(F) = (\beta \rightarrow \alpha)
$$
$$ \tau(G) = (\alpha \rightarrow \beta) $$

$$ \tau(h) = (\alpha \rightarrow \alpha) $$

$$ \tau(u) = \tau(v) = \beta $$

$$ \tau(E) = \tau(x) = \tau(y) = \alpha $$

$$ \tau(X) = \tau(Y) = ((\alpha \rightarrow \alpha) \rightarrow \alpha) $$

$$ \tau(Z) = ((\alpha \rightarrow \alpha), \alpha \rightarrow \alpha) $$

we get, after reduction to normal form :

1. $\{ u = v, Fu \neq Fv \} \quad F$ is one-one $B \rightarrow A$
2. $Fu \neq E$ \quad not onto

3. $Xh \neq Yh, hZ(h,x) = x \quad$ every one-one $h \quad A \rightarrow A$
4. $hXh = hYh, hZ(h,x) = x \quad$ is onto

5. $x = y, Gx \neq Gy \quad G$ is one-one $A \rightarrow B$

We get the following refutation :

$$ \text{R(3,2)} \quad 6 \quad Xh \neq Yh/\{hZ(h,E), Fu'\} = C_6 $$

$$ \text{R(4,2)} \quad 7 \quad h\lambda h = hYh/C_6 $$

$$ \text{R(7,1)} \quad 8 \quad u = v/C_6 + \{hXh, Fu\} + \{hYh, Fv\} $$

$$ \text{R(8,5)} \quad 9 \quad x = y/C_6 + \{hXh, FGx\} + \{hYh, F Gy\} $$

$$ \text{R(9,6)} \quad 10 \quad \emptyset/\{hZ(h,E), Fu'\}, \{hXh, FGXh'\}, \{hYh, FGYh'\}, \{h'Z(h', E), Fu''\} $$

11. $\Box$ by substitution : $\{h \leftarrow \lambda x \cdot FGx, u' \leftarrow GZ(\lambda x \cdot FGx, E), h' \text{ same as } h, u'' \text{ same as } u'\}$.

When the theorem prover gets a refutation, it is tri-
vial to give the user a more natural proof in Andrews' system, chai-
ning back the substitutions.
We shall demonstrate this technique here; now $S(n)$ means substitution in clause n and $C(n,m)$ means cut of clause n and clause m. H is an abbreviation for $\lambda x.FGx$.

$$S(2) \qquad 6' \quad FGZ(H,E) \neq E$$

$$S(3) \qquad 7' \quad XH \neq YH, FGZ(H,E) = E$$

$$C(6',7') \qquad 8' \quad XH \neq YH$$

$$S(4) \qquad 9' \quad FGXH = FGYH, FGZ(H,E) = E$$

$$C(6',9') \qquad 10' \quad FGXH = FGYH$$

$$S(1) \qquad 11' \quad GXH = GYH, FGXH \neq FGYH$$

$$C(10',11') \qquad 12' \quad GXH = GYH$$

$$S(5) \qquad 13' \quad XH = YH, GXH \neq GYH$$

$$C(12',13') \qquad 14' \quad XH = YH$$

$$C(8',14') \qquad 15' \quad \Box$$

### Example 3

We shall now give a completely detailed refutation of a less trivial proposition. We are going to prove Knaster-Tarski's theorem : "Any function monotone over a complete lattice possesses a fixpoint". Let $(A, \leq)$ be the complete lattice considered.

We use the types : o for truth values

i for the elements of A.

We represent a subset of A by its characteristic function, of type $(i \to o)$. We use the following axioms :

$$(\forall xyz)[x \leq x \ \& \ ((x \leq y \ \& \ y \leq x) \supset x = y) \ \& \ ((x \leq y \ \& \ y \leq z) \supset x \leq z)] \\ [\leq \ \text{is a partial ordering}]$$

$$(\forall xh)[(hx \supset \cap h \leq x) \ \& \ ((\forall y)(hy \supset x \leq y) \supset x \leq \cap h)]$$

[every subset $h$ of A possesses a $glb \cap h$]
We want to prove :

$$ (\forall f)[(\forall xy)(x \le y \supset fx \le fy) \supset (\exists z)(fz = z)] $$

The types of our atoms are, respectively :

$x, y, z : i$

$h : (i \to o)$

$f : (i \to i)$

$=, \leq : (i, i \to o)$

$\cap : ((i \to o) \to i).$

We negate the theorem and put all the propositions in clause form. We use again the usual form of Skolem functions, replacing

$E_i(\lambda y \cdot hy \supset x \le y)$ by $Y(x,h)$ and

$E_{(i \to i)}(\lambda f \cdot ((\forall xy)(x \le y \supset fx \le fy) \supset (\exists z)(fz = z)))$ by $F$, where $Y$ and $F$ are new constants of types respectively $(i, (i \to o) \to i)$ and $(i \to i)$.

This gives us the following set of clauses :

$$ 1 \quad x \le x $$

$$ 2 \quad \neg x \le y, \neg y \le x, x = y $$

$$ 3 \quad \neg x \le y, \neg y \le z, x \le z $$

$$ 4 \quad \neg h x, \cap h \le x $$

$$ 5 \quad h Y(x, h), x \le \cap h $$

$$ 6 \quad \neg x \le Y(x, h), x \le \cap h $$

$$ 7 \quad \neg x \le y, Fx \le Fy $$

$$ 8 \quad \neg Fx = x $$
First we resolve 2 (on its last literal) and 8. As the constraint {x = y, Fx' = x'} possesses a most general unifier {x ← Fx', y ← x'} we just substitute without generating any constraint, to get :

$$R(2,8) \qquad 9 \quad \neg Fx \leq x, \neg x \leq Fx$$

Similarly, resolving 4 on its second literal with 9 on its second literal, we get :

$$R(4,9) \qquad 10 \quad \neg F \cap h \leq \cap h, \neg hF \cap h \\ \qquad \text{[The last literal is a shorthand for } \neg(h(F(\cap h))))\text{].}$$

Next, we resolve the second literal of 7 with the second of 10. Here we do not know a most general way of unifying the two literals, and a constraint is added to the resolvent :

$$R(7,10) \qquad 11 \quad \neg F \cap h \leq \cap h, \neg x \leq y/\{hF \cap h, Fx \leq Fy\} \\ \qquad \text{*(This constraint is obviously unifiable, for instance by } \{h \leftarrow \lambda u \cdot Fx \leq Fy\} \text{).}$$

Now we shall resolve both literals of 11 with the second literal of 6. We have to unify :

- firstly {F ∩ h, x, x'}

- secondly {∩h, y, ∩h'} and again we know a most general unifier :

$$\{x \leftarrow F \cap h, x' \leftarrow F \cap h, h' \leftarrow h, y \leftarrow \cap h\}$$

and therefore we get :

$$R(6,11) \qquad 12 \quad \neg F \cap h \leq Y(F \cap h,h)/\{hF \cap h, FF \cap h \leq F \cap h\}.$$

Notice that the substitution has been effected in the constraint from 11 as well as in the literals. We shall denote this new constraint by C.
The rest of the refutation is pretty straightforward,
no new constraints being generated :

$$
R(3, 12) \quad 13 \quad \neg F \cap h \le y, \neg y \le Y(F \cap h, h)/C
$$

$$
R(7, 13) \quad 14 \quad \bigcap h \le y, \bigwedge Fy \le Y(F \cap h, h)/C
$$

$$
R(4, 14) \quad 15 \quad \neg hy, \neg Fy \leq Y(F \cap h, h)/C
$$

$$
R(5, 11) \quad 16 \quad hY(F \cap h, h)/C
$$

This last CC is the analogue of 12, 5 and 6 having one
literal in common due to the initial reduction to clause form.

Next we resolve both literals of 15 with 16, obtaining
therefore a terminal CC :

R(16,15) 17 Ø/C' where C' consists of the following cons-
traints :

$$
\{hF \cap h, FF \cap h \leq F \cap h\},
$$

$$
\{h'F \cap h', FF \cap h' \leq F \cap h'\},
$$

$$
\{hy, Fy \leq Y(F \cap h, h), h'Y(F \cap h', h')\}.
$$

We then apply our unification process to C', which
terminates with the answer "yes", corresponding to the unifier :

$$
\sigma = \{h \leftarrow \lambda u \cdot Fu \leq u,
$$

$$
h' \leftarrow \lambda u \cdot Fu \leq u,
$$

$$
y \leftarrow Y(F \cap \lambda u \cdot Fu \le u, \lambda u \cdot Fu \le u).
$$

The refutation is now completed, and it is trivial to
go back in the proof, substituting σ and the substitutions derived
from it by composition with the unifiers already detected, to get
a ground refutation.
In particular, we shall substitute $\bigcap \lambda u \cdot Fu \le u$ for $x$ in 8, which gives us explicitly a fixpoint of $F$, namely $\bigcap (\{u|Fu \le u\})$, which is precisely its least fixpoint.

Notice that splitting was not necessary here again, and
that the refutation is pretty short and does not involve huge cons-
traints.

CONCLUSION

It is difficult to make any efficiency assertion from
searchless examples. However, one of the most important heuristic
rules to use in this system would be to throw out clauses with cons-
traints which are obviously not unifiable. In practice of course
most clauses will be recognized as such, thereby reducing sharply
the number of possible derivations.

Types in this logic play a multiple role. First, they
permit us to have $\lambda$ - calculus normal forms for every terms. Second,
they can be used to sort objects of different nature, and so we get
restricted quantification without adding cumbersome additional li-
terals. Finally, as a consequence they restrict the search for
unifiers.

This system uses the constraints mechanism to delay as
much as possible the process of unification. This has two advanta-
ges. First, the deeper we go in a refutation, the more information
we gather about the structure of the terms we need to substitute.
This reduces our search space for unifiers (intuitively, the more
pairs argument-value we know, the less functions exist whose graphs
contain these pairs).
Second, we just need to check for the existence of some unifier, we do not need most general ones. This permits us never to consider the unification of two terms whose heads are variables, such as :

$$f(A_1, A_2, \dots, A_n) \text{ and } g(B_1, B_2, \dots, B_p) \\ \text{or } f(A_1, A_2, \dots, A_n) \text{ and } f(C_1, C_2, \dots, C_n).$$

These cases are the most difficult ones to consider for most general unification, but they are trivial when we need only check for existence of unifiers (take any constant function). Actually we need to compose only two elementary unification processes (called imitation and projection), whereas to get most general unifiers Pietrzykowski and Jensen (1972) need four, the other two being the most prolific ones indeed. This is because when we consider a pair such as $f(A_1, A_2, \dots, A_n)$ and $F(B_1, B_2, \dots, B_p)$, we know something definite about the structure of the common instance (it must begin with an F) and so we have a "handle" on the unification process.

Automatic theorem proving is undoubtedly more difficult here than in first order logic. However our higher order language permits us to state many theorems in a more concise way, and refutations tend to be a lot shorter. For instance, in our examples, we used set variables in a very natural way (using their characteristic predicates). We could get all the properties of $\epsilon$ with application, of complementation with $\neg$ and of union with $\vee$. Also the abstraction mechanism of $\lambda$-calculus replaces in a nice way cumbersome comprehension axioms.
However we might still need use some axioms of descriptions, to assert the existence of certain functions :

$$ \exists i \forall p [(\exists! x p(x)) \supset p(i(p))] $$

When we need to substitute non-atomic propositions for predicate variables (via splitting), refutations tend to become messy and unnatural. The system should be improved on this point, maybe by replacing splitting by rules closer to natural deduction. This would also allow us to get rid of the initial reduction to clause form, which is not always desirable, and to use well-known techniques to decrease the complexity of refutations (Ernst 1971 b). Only then can we hope to deal with proofs by induction in a satisfactory way.

In conclusion, we have presented in this paper a system of logic which is a generalization to Church's type theory of Robinson's resolution. This system seems well suited to mechanizing proofs which require complex substitutions for function variables, as shown in a few hand-simulated examples. Substitutions of non-atomic propositions for predicate variables are not dealt with in a very satisfactory way yet, and some improvement is needed there. Our system without extensionality is equivalent to Andrews's system. However it is amenable to automatic treatment because the substitution rule has disappeared. Our system with extensionality ought to be equivalent to Pietrzykowski's system, and it is conjectured that it is more efficient. A partial implementation is in progress at I. R. I. A., mechanizing constrained resolution without splitting. The emphasis will be put on the heuristic rules to process constraints during the refutation.
B I B L I O G R A P H Y

Andrews P.B. (1971)

Resolution in type theory

Journal of Symbolic Logic 36,3 pp. 414-432.

Andrews P.B. (1972)

General models and extensionality

Journal of Symbolic Logic 37,2 pp. 395-397.

Church A. (1940)

A formulation of the simple theory of types.

Journal of Symbolic Logic 5,1 pp. 56-68.

Church A. (1941)

The calculi of lambda-conversion.

Annals of Mathematical Studies no.6.

Princeton University Press.

Curry H.B. and Feys R. (1958)

Combinatory Logic (Vol 1)

North Holland, Amsterdam.

Ernst G.W. (1971 a)

A matching procedure for type theory

Computing and Information Sciences,

Case Western Reserve University.

Ernst G.W. (1971 b)

The utility of independent subgoals in theorem proving.

Information and control 18,3 pp. 237-252.

Gould W.E. (1966)

A matching procedure for w-order logic.

Scientific Report No. 4, AFCRL 66-781

(Contract AF 19 (628)-3250) AD-646 560.

Henkin L. (1950)

Completeness in the theory of types.

Journal of Symbolic Logic 15,2 pp. 81-91.

Huet G.P. (1972)

Constrained resolution : A complete method for higher order logic.

Ph.D. Thesis, Case Western University,

Jennings Computing Center Report 1117.

Huet G.P. (1973)

The undecidability of unification in third order logic.

Information and Control, to appear.
Pietrzykowski T. (1971)

A complete mechanization of second order logic.

Report CSRR 2038, Department of Applied Analysis and Computer
Science, University of Waterloo.

Pietrzykowski T. and Jensen D. (1972)

A complete mechanization of ω-order type theory.

Report CSRR 2060, Department of Applied Analysis and Computer
Science, University of Waterloo.

Also Assoc. for Comp. Mach. National Conference (1972)

Vol 1, pp. 82-92.

Robinson J. A. (1965)

A machine-oriented logic based on the resolution principle.

Journal of Assoc. for Comp. Mach. 12, 1 pp. 23.41.

Robinson J. A. (1968)

New directions in theorem proving.

Proceedings of IFIP Congress Edinburgh August 1968

in Information processing 68, Vol. 1 pp. 63-67

North Holland, Amsterdam.

Robinson J. A. (1969)

Mechanizing higher order logic.

Machine Intelligence 4, pp. 151-170.

American Elsevier, New York.