Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!uunet!samsung!aplcen!haven!uvaarpa!ra!mac
From: mac@ra.cs.Virginia.EDU (M. Alex Colvin)
Newsgroups: comp.theory
Subject: Re: Horn clauses
Summary: satisfiability
Message-ID: <813@ra.cs.Virginia.EDU>
Date: 9 Jan 90 14:25:20 GMT
References: <4500@daimi.dk> <1799@uwm.edu>
Organization: U.Va. CS Department, Charlottesville, VA
Lines: 5

>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?