Is Horn clause logic decidable?

[Daniel Schwartz]

Thanks to everyone for your replies.  This is very helpful, and appreciated.

Dan Schwartz

------------------------------------------------------------------------

Daniel Schwartz <schwartz at cs.fsu.edu> wrote:

> I have been told that Horn Clause Logic, considered as a subsystem of
> First-Order Logic, is undecidable.  More exactly, if S is a set of Horn
> clauses and P is an atom, then whether P is derivable from S is undecidable.
>
> However, I have never seen a proof of this and have been unable to find any
> discussion of it.
>
> Would anyone know whether this statemnt is true, and could you provide a
> refernce?
>
> Thanks and best regards,
>
> Dan Schwartz
>
> ************************************************************************
> Dr. Daniel G. Schwartz                            Office    850-644-5875
> Dept. of Computer Science, MC 4530                CS Dept   850-644-4029
> Florida State University                          Fax       850-644-0058
> Tallahassee, FL 32306-4530                        schwartz at cs.fsu.edu
> U.S.A.                                   http://www.cs.fsu.edu/~schwartz
> ************************************************************************