Refinement Operator

A Refinement Operator is a Set-Valued Function that maps a statement to a subset of its refinements.

References

2001

1. $p \vdash q$, i.e. everything provable from $q$ is provable from $p$, or equivalently, $p$ is at least as general as $q$.
2. $size(p) \lt size(q)$ under some size metric. In logic programming terms, Shapiro uses the following:
The $size$ of a sentence $p$, $size(p)$, is the number of symbol occurrences in $p$ (excluding punctuation symbols) minus the number of distinct variables occurring in $p$.
Intuitively, building a monotonic size increase into the notion of refinement means that all refinements of $p$ are more specific/weaker than $p$, as it requires more things to be provable (in the case of adding a body goal) or more structure to be present in the query (if a function symbol is introduced, or two or more variables are unified). This exploits the intimate relationship between the syntax and semantics of logic programs.
A refinement operator $\rho$ is then defined to be a set-valued function that maps a statement $p$ to a subset of its refinements, with some technical side-conditions.