Is Horn clause logic decidable?

[Dominik Kirst]

Dear Daniel,

this is shown by reduction from the Post correspondence problem (PCP) in Manna’s textbook ‘Mathematical theory of computation’ where the idea is attributed to Floyd. Given an instance S of PCP consisting of pairs of strings (s,t), one constructs Horn formulas in a language suitable to express strings and with a binary relation R and a propositional constant Q as follows:

C1 := P(s,t), one instance for each (s,t) in S, stating “all initial pairs can be derived"
C2 := for all x y. P(x,y) -> P(sx,ty), one instance for each (s,t) in S, stating “derived pairs can be extended component-wise"
C3 := for all x. P(x,x) -> Q, stating “matching derivations are solutions"

It can be verified that S has a solution iff from C1,C2,C3 one can derive Q, establishing a many-one reduction from PCP to Horn clause logic and hence the undecidability of the latter.

In case you are interested in a more detailed argument, you could also have a look at our paper describing a mechanised version of this and related reductions using the Coq proof assistant (https://www.ps.uni-saarland.de/extras/fol-undec/ <https://www.ps.uni-saarland.de/extras/fol-undec/>). Note however that we work in a constructive meta-theory, so while the reduction to validity (Section 3.1) is in Horn format as described above, the reduction to classical provability (Section 3.5) is obtained by a more complicated Friedman-style double-negation translation.

Hope this is helpful,
Dominik

-----------------------------------------
Programming Systems Lab
Saarland University
http://www.ps.uni-saarland.de/~kirst/ <http://www.ps.uni-saarland.de/~kirst/>



> On 16. Oct 2021, at 23:59, 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/db0ea687/attachment-0001.html>