Is Horn clause logic decidable?

Lawrence Paulson lp15 at
Mon Oct 18 06:04:06 EDT 2021

Surely it is simply that the programming language Prolog is based on Horn clause logic, and even without its non-logical extensions, Prolog is obviously Turing complete.

Larry Paulson
On 18 Oct 2021, 05:05 +0100, 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

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211018/03533754/attachment-0001.html>

More information about the FOM mailing list