Refinement Operator

From GM-RKB
Jump to: navigation, search

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



References

2015

2010

2009

2008

2007a

2007b

2001

1. [math]p \vdash q[/math], i.e. everything provable from [math]q[/math] is provable from [math]p[/math], or equivalently, [math]p[/math] is at least as general as [math]q[/math].
2. [math]size(p) \lt size(q)[/math] under some size metric. In logic programming terms, Shapiro uses the following:
The [math]size[/math] of a sentence [math]p[/math], [math]size(p)[/math], is the number of symbol occurrences in [math]p[/math] (excluding punctuation symbols) minus the number of distinct variables occurring in [math]p[/math].
Intuitively, building a monotonic size increase into the notion of refinement means that all refinements of [math]p[/math] are more specific/weaker than [math]p[/math], 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 [math]\rho[/math] is then defined to be a set-valued function that maps a statement [math]p[/math] to a subset of its refinements, with some technical side-conditions.