Is Horn clause logic decidable?

[James Harland]

RMIT Classification: Trusted

Tarnlund showed in 1977 that Horn clauses are Turing-complete, and hence undecidable. See https://link.springer.com/article/10.1007/BF01932293

-----Original Message-----
From: Daniel Schwartz <schwartz at cs.fsu.edu>
Sent: Sunday, 17 October, 2021 9:00 AM
To: fom at cs.nyu.edu
Subject: Is Horn clause logic decidable?

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