Refinement Operator

From GM-RKB
Jump to navigation Jump to 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. pq, i.e. everything provable from q is provable from p, or equivalently, p is at least as general as q.
2. size(p)<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 ρ 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.