Completeness issues in RUE-NRF deduction: The undecidability of viability |
| |
Authors: | James J. Lu V. S. Subrahmanian |
| |
Affiliation: | (1) Department of Computer Science, Bucknell University, 17837 Lewisburg, PA, USA;(2) Department of Computer Science, University of Maryland, 20742 College Park, MD, USA |
| |
Abstract: | We show that the algorithm directly induced by the viability definition in Ref. [4] does not terminate in general. As a consequence, RUE-resolution in strong form is not complete. Moreover, we show that ground query processing forcovered 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.Work supported in part by NSF grants IRI-9015251 and IRI-9109755 and by Army Research office grant DAAL-03-92-G-0225. |
| |
Keywords: | Theorem proving equality logic programming undecidability |
本文献已被 SpringerLink 等数据库收录! |
|