Path: utzoo!utgpu!jarvis.csri.toronto.edu!rutgers!cs.utexas.edu!uunet!yale!Duchier-Denys
From: Duchier-Denys@cs.yale.edu (Denys Duchier)
Newsgroups: comp.ai
Subject: Re: Request for opinions on AI textbook
Message-ID: <65402@yale-celray.yale.UUCP>
Date: 4 Jul 89 23:26:42 GMT
References: <295@kubix.UUCP>
Sender: root@yale.UUCP
Reply-To: Duchier-Denys@cs.yale.edu (Denys Duchier)
Organization: Computer Science, Yale University, New Haven, CT 06520-2158
Lines: 15
In-reply-to: flach@kubix.UUCP (Peter Flach)

In article <295@kubix.UUCP>, flach@kubix (Peter Flach) writes:
> To me, the book seems quite good, although I came across some strange
> mistakes such as 'The Horn clause calculus is equivalent to the full
> first-order predicate calculus for proofs by refutation' (p.206).

In what sense is it a mistake? Resolution is refutation-complete and a
set of clauses can be transformed into an equivalent set of
horn-clauses by inventing new predicates to name the negation of
existing predicates. For instance (NOT (P a)) can be replaced by (Q a)
provided you add the horn clauses:

		(OR (NOT (P x)) (Q x))
		(OR (NOT (Q x)) (P x))

--Denys