Decidability of the Clark's Completion Semantics for Monadic Programs and Queries

TL;DR

This paper proves that the Clark's completion semantics is decidable for monadic general logic programs and queries, providing a restricted but computationally manageable subset of logic programming.

Contribution

It establishes the first decidability result for Clark's completion semantics in the context of monadic programs and queries.

Findings

Decidability of Clark's completion semantics for monadic programs

Restrictions on programs ensure computational manageability

Advances understanding of semantics in logic programming

Abstract

There are many different semantics for general logic programs (i.e. programs that use negation in the bodies of clauses). Most of these semantics are Turing complete (in a sense that can be made precise), implying that they are undecidable. To obtain decidability one needs to put additional restrictions on programs and queries. In logic programming it is natural to put restrictions on the underlying first-order language. In this note we show the decidability of the Clark's completion semantics for monadic general programs and queries. To appear in Theory and Practice of Logic Programming (TPLP)