Relay-Version: version B 2.10 5/3/83; site utzoo.UUCP
Posting-Version: version B 2.10 beta 3/9/83; site cwruecmp.UUCP
Path: utzoo!linus!decvax!cwruecmp!decot
From: decot@cwruecmp.UUCP (Dave Decot)
Newsgroups: net.ai
Subject: Re: Unification Query
Message-ID: <730@cwruecmp.UUCP>
Date: Fri, 21-Oct-83 06:19:24 EDT
Article-I.D.: cwruecmp.730
Posted: Fri Oct 21 06:19:24 1983
Date-Received: Sat, 22-Oct-83 02:36:11 EDT
References: <6030@unc.UUCP>
Organization: CWRU Computer Engr. Cleveland, Ohio
Lines: 20

An "Efficient Unification Algorithm"?!?  This is amazing!  I'll have to go
read that article right away, because if the title is not misleading, and you
have accurately described what a unification algorithm is, P == NP!

The Satisfiability problem is solvable by any algorithm that does what you
require of your most general unification algorithm, so your problem is
NP-complete.  The set of terms to be unified contains only two terms, one is
simply "1" and the other is the expression to be satisfied.  Your problem is
in NP as long as the terms with substituted variables can be evaluated in
polynomial time.  At any rate, your problem is at least as "hard" as
Satisfiability.

Since your problem can be solved efficiently, it must be not only in NP, but
also in P (the set of problems solvable in time proportional to a polynomial
function of the length of its instances) by today's normal computers.

The most logical explanation is that the algorithm in that paper is not
a full implementation of your desired "most general" algorithm.
----------------------------------------
Dave Decot	..!decvax!cwruecmp!decot