Title: Completeness Issues in RUE-Resolution: The Undecidability of Viability
Authors: James J. Lu, V.S. Subrahmanian.
Abstract
We show that the algorithm directly induced by the viability definition does not terminate in general. As a consequence, RUE-resolution in strong form is not complete. Moreover, we show that ground query processing for covered pure logic programs can be reduced to computing viability. Since the problem of ground query processing is strictly recursively enumerable even under the above restrictions, it follows that the notion of viability is undecidable. Finally, we present a modified viability check that solves the non-termination problem for ground terms.
Journal of Automated Reasoning, 10, 1993, 371-388.