kimskak@daimi.dk (Kim Skak Larsen) (01/05/90)
How difficult is resolution of propositional Horn clauses,
i.e. consider a prolog program without variables that looks
something like
a :- b,c.
b :- c.
c.
and not like
a(X,Y) :- b(X),c(X,Y).
etc...
What is the complexity of answering queries such as
a?
I heard a rumour about a result by Mike Paterson of O(n^2).
Any references?markh@csd4.csd.uwm.edu (Mark William Hopkins) (01/06/90)
In article <4500@daimi.dk> kimskak@daimi.dk (Kim Skak Larsen) writes: > >How difficult is resolution of propositional Horn clauses, >i.e. consider a prolog program without variables that looks >something like > a :- b,c. > b :- c. > c. > ... >What is the complexity of answering queries such as > > a? Your example: a :- b, c. b :- c. c. :- a. is actually a disguised version of this: * Given the grammar: * Start symbol: *start * Nonterminals: a, b, c * Terminals: *c * Productions: * *start -> a * a -> b c * b -> c * c -> *c * * Prove that the corresponding language is non-empty. I think the corresponding general problem is NP-complete.
mac@ra.cs.Virginia.EDU (M. Alex Colvin) (01/09/90)
>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?
moises@maui.cs.ucla.edu (Moises Goldszmidt) (01/10/90)
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.-