Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

Unification Algorithm for Theorem Proving

IP.com Disclosure Number: IPCOM000074450D
Original Publication Date: 1971-Apr-01
Included in the Prior Art Database: 2005-Feb-23
Document File: 4 page(s) / 16K

Publishing Venue

IBM

Related People

Kellerman, E: AUTHOR

Abstract

This algorithm is applicable to theorem proving programs using variations of the resolution principle.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 50% of the total text.

Page 1 of 4

Unification Algorithm for Theorem Proving

This algorithm is applicable to theorem proving programs using variations of the resolution principle.

Before proceeding with a description of the algorithm, a definition of the terminology used will be helpful. The symbols u, v, w, x, y, z are variables and may be subscripted. The symbols f, g, h are function symbols and may be subscripted.

A function is a function symbol by itself (the constant functions), or a function symbol followed by one or more arguments enclosed in parentheses and separated by commas (if necessary). Once a function symbol is assigned to a function, it will always require the same number of arguments.

A variable is a term. A function whose arguments are terms is a term. The following are examples of terms: f (x,y,z)

f (x,g(x,u),y)

g (x,g(x,g(x,u))).

A substitution component is an expression of the form T/V where V is a variable and T is a term.

A substitution is a set of substitution components, none of the variables of which are the same.

If E is a term and t is a substitution, t=[T1/V1,...,Tn/Vn], then the instantiation of E by t (denoted by Et) is the operation of replacing every occurrence of the variable Vi in E by an occurrence of the term Ti. Example: E=f(x,g(x,y),z)

t-[ h(u)/x, y/z ]

and Et=f (h(u),g(h(u),z),z).

If A and B are terms, then a substitution t is said to unify A and B, if At=Bt, and if the generation of At and Bt requires only a finite number of replacements. Example: t= (x/u, f(x,y)/v ] unifies

A= f(x,f(x,y)) and

B= f(u,v)

since At=Bt= f(x,f(x,y)).

The present algorithm determines if two terms are unifiable, and if so, determines which substitution unifies the two terms.

In the following discussion, the terms to be unified will be referred to as A and B.
1. Scan A and B from left to right, associating with each symbol

encountered a depth constant whose value is determined as

follows:

1

Page 2 of 4

a) The initial value of the depth constant is 1.

b) Every time a left parenthesis is encountered, the value of

the depth constant is increased by 1.

c) Every time a right parenthesis is encountered, the value

of the depth constant is decreased by 1.

d) A comma has no effect on the depth constant.
2. Remove all parentheses and commas from A and B.
3. Scan the modified A and B from left to right, while checking

for the following conditions:

a) If the two positions being scanned have the same symbol,

then no action is required and the scan continues.

b) If the two positions being scanned have different symbols,

and neither of the symbols is a variable, then the two

terms are not unifiable. Stop.

c) If one of the two positions being scanned contains a

variable (call

it v), then a substitution component whose variable is

v is obtained. Assume that v comes from A and that the

value of

the depth constant associated with it is d. The term for

this substitution component is obtained from B, and

starts in the position

that was being compared with v. It includes...