Completeness issues in RUE-NRF deduction: The undecidability of viability

James J. Lu*, V. S. Subrahmanian

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

1 Scopus citations

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 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.

Original languageEnglish (US)
Pages (from-to)371-388
Number of pages18
JournalJournal of Automated Reasoning
Volume10
Issue number3
DOIs
StatePublished - Oct 1993
Externally publishedYes

Keywords

  • equality
  • logic programming
  • Theorem proving
  • undecidability

ASJC Scopus subject areas

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Fingerprint

Dive into the research topics of 'Completeness issues in RUE-NRF deduction: The undecidability of viability'. Together they form a unique fingerprint.

Cite this