Is Horn clause logic decidable?

[Gernot Salzer]

If you are aquainted with Prolog, it is straight-forward to implement
Turing machines. But in fact, a single binary clause, a fact and a
one-atom-goal is sufficient, see
P. Devienne et al: One binary Horn clause is enough 
https://link.springer.com/chapter/10.1007%2F3-540-57785-8_128

Best, Gernot

@InProceedings{10.1007/3-540-57785-8_128,
author="Devienne, Philippe
and Leb{\`e}gue, Patrick
and Routier, Jean-Christophe
and W{\"u}rtz, J{\"o}rg",
editor="Enjalbert, Patrice
and Mayr, Ernst W.
and Wagner, Klaus W.",
title="One binary horn clause is enough",
booktitle="STACS 94",
year="1994",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="19--32",
abstract="This paper proposes an equivalent form of the famous B{\"o}hm-Jacopini theorem for declarative languages. C. B{\"o}hm and G. Jacopini [1] proved that all programming can be done with at most one single whiledo. That result is cited as a mathematical justification for structured programming. A similar result can be shown for declarative programming. Indeed the simplest class of recursive programs in Horn clause languages can be defined by the following scheme:",
isbn="978-3-540-48332-8"
}



On Sat, Oct 16, 2021 at 05:59:34PM -0400, Daniel Schwartz 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
> ************************************************************************