Is Horn clause logic decidable?

[Josef Urban]

Prolog is Turing-complete (
https://en.wikipedia.org/wiki/Prolog#Turing_completeness). A recent
reference seems to be
https://link.springer.com/chapter/10.1007/3-540-56503-5_7 .

On Mon, Oct 18, 2021 at 6:03 AM Daniel Schwartz <schwartz at cs.fsu.edu> 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
> ************************************************************************
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20211018/b2d2652d/attachment-0001.html>