Deductive oracle

For non-recursive literals, since they are assumed to be primitives, it is possible to compute the witnesses without knowing We thus only need an oracle for the specified predicate rin. A candidate mechanized oracle is one that performs deduction using the specification EP(r) as knowledge about rIn, Such a deductive oracle is sound provided EP(f) is consistent with % Other oracles can be imagined, performing analogical reasoning, say. In the sequel we just assume the existence of such an oracle, but do not require it to be sound or complete. A more practical version of the previous definition is thus ... 

Indeed, if TR - [], then the deductive oracle infers that either = or = , according to example E and property P, respectively. This illustrates three things. First, some of the existential variables may have to be regrouped into tuples in order to avoid losing some relationships. Second, the availability of the examples to the oracle provokes the appearance of an answer that is totally unrelated to any computation of ejface b,[b,c], namely = . 

In the following, once a specification EP r) has been clearly mentioned, we assume that 0(r) is the deductive oracle based on EP r), and that Mr) is the positive example set of EP(r). This allows a more compact notation for the exp/3 operator. 

Indeed, if TL - [b,c], then the deductive oracle infers that either TP = [b,c] or TP -[cM, according to properties P and P3, respectively. But the effacefi atom only holds for the first answer. ... 

Other researchers have tackled Shapiro s remarks on oracle mechanization [Shapiro 82, Section 3.7] via the incorporation of constraints and partial specifications . The solutions by [Lichtenstein and Shapiro 88], [Drabent et al. 88], and [De Raedt and Bruynooghe 92a] are surveyed in Chapter 6. The solution by [Dershowitz and Lee 93] seems unrealistic in general, because it relies on a complete specification, which could thus rather be used to perform deductive synthesis. 

---