Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!samsung!usc!ucla-cs!moises
From: moises@maui.cs.ucla.edu (Moises Goldszmidt)
Newsgroups: comp.theory
Subject: Re: Horn clauses
Message-ID: <30630@shemp.CS.UCLA.EDU>
Date: 9 Jan 90 19:34:25 GMT
References: <4500@daimi.dk> <1799@uwm.edu> <813@ra.cs.Virginia.EDU>
Sender: news@CS.UCLA.EDU
Reply-To: moises@cs.ucla.edu (Moises Goldszmidt)
Organization: UCLA Computer Science Department
Lines: 15

In article <813@ra.cs.Virginia.EDU> mac@ra.cs.Virginia.EDU (M. Alex Colvin) writes:
>>How difficult is resolution of propositional Horn clauses,
>>i.e. consider a prolog program without variables ...
>
>isn't this the same as SAT (Boolean satisfiability), the canonical
>NP-complete problem?


Propositional Horn formulae is a very special case. Look into
the article 
"Linear Time Algorithms for Testing the Satisfiabilty of 
Propositional Horn Formulae" by W. Dowling and J. Gallier
in Journal of Logic Programming 1984:3:267-284.

moises.-