DFKI Research Report-93-09
by Philipp Hanschke, Jörg Würtz
Satisfiability of the Smallest Binary Program
Recursivity is well known to be a crucial and important concept in programming theory. The simplest scheme of recursion in the context of logic programming is the binary Horn clause . The decidability of the satisfiability problem of programs consisting of such a rule, a fact and a goal -- called smallest binary program -- has been a goal of research for some time. In this paper the undecidability of the smallest binary program is shown by a simple reduction of the Post Correspondence Problem.
This document is available as Postscript.
The next abstract is here, and the previous abstract is here.
Note: This page was written to look best with CSS stylesheet support Level 1 or higher. Since you can see this, your browser obviously doesn't support CSS, or you have turned it off. We highly recommend you use a browser that supports and uses CSS, and review this page once you do. However, don't fear, we've tried to write this page to still work and be readable without CSS.