Is Horn clause logic decidable?

Dominik Kirst kirst at cs.uni-saarland.de
Mon Oct 18 04:46:54 EDT 2021


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>


More information about the FOM mailing list