Is Horn clause logic decidable?

Daniel Schwartz schwartz at
Mon Oct 18 08:35:22 EDT 2021

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

Dan Schwartz


Daniel Schwartz <schwartz at> 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
> U.S.A.                         
> ************************************************************************

More information about the FOM mailing list