DFKI Research Report-93-09



Language: English

by Philipp Hanschke, Jörg Würtz

Satisfiability of the Smallest Binary Program

8 Pages


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 P(l1,...,ln) left-arrow P(r1,...,rn). 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.

DFKI-Bibliothek (bib@dfki.uni-kl.de)

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.