On Answer Substitutions in Logic Programming

TL;DR

This paper introduces a refined approach to answer substitutions in logic programming by distinguishing between noisy and silent existential quantifiers, enhancing the control over recorded answer instantiations.

Contribution

It proposes a novel refinement of existential quantifiers to support selective answer substitutions and discusses the concepts of don't-care and don't-know constants.

Findings

Differentiates noisy and silent answer substitutions.

Provides a formal framework for selective answer recording.

Enhances understanding of constants in logic programming.

Abstract

Answer substitutions play a central role in logic programming. To support {\it selective} answer substitutions, we refine $\exists x$ in goals into two different versions: the noisy version $\exists^o x$ and the silent version $\exists x$. The main difference is that only the instantiation in $\exists^o x$ will be recorded in the answer substitutions. Similarly for $\forall x$. In addition, we discuss the notion of don't-care constants and don't-know constants.