Is Horn clause logic decidable?

Gernot Salzer gernot.salzer at
Mon Oct 18 03:44:23 EDT 2021

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

Best, Gernot

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",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
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:",

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
> U.S.A.                         
> ************************************************************************

More information about the FOM mailing list