The Proofs-as-Programs Method

In this chapter, we develop the Proofs-as-Programs Method, which adds atoms to a logic algorithm so that some correctness criteria wrt a set of properties become satisfied. This method is part of our tool-box of methods for instantiating the predicate-variables of a schema. First, in Section 9.1, we state the problem. Then, in Section 9.2, we explain a method to solve this problem, and discuss its correctness in Section 9.3. In Section 9.4, we illustrate this method on a few sample problems. Future work and related work are discussed in Section 9.5 and Section 9.6, respectively, before drawing some conclusions in Section 9.7. 

SLD resolution is parameterized on a computation rule and a search rule [Lloyd 87]. For extended execution, these rules are, for the purpose of the Proofs-as-Programs Method, instantiated as follows ... 

The problem statement of the Proofs-as-Programs Method requires that LA r) be complete wrt P(r), and this, in retrospective, according to the new criterion (1). Indeed, there wouldn t exist any complete syntactic specialization otherwise. But in practice, it is often impossible to know beforehand whether this constraint is satisfied... 

Definition 9-5 The Proofs-as-Programs Method succeeds iff LA r) is proven (by extended execution) to be complete wrt P(r). It fails otherwise. 

So far for the proof aspects of the Proofs-as-Programs Method. Let s now turn to the condition extraction aspects. 

The Proofs-as-Programs Method is deterministic because the results of all successful derivations are collected before computing 21 therefrom. The method is thus independent of any ordering of disjuncts within LA r), or of properties within P(r). The method may fail, as conveyed by Definition 9-5. However, nothing can be said about the synthesized logic algorithms in terms of determinism or finiteness, because nothing is known about the properties. 

In this chapter, we have presented the Proofs-as-Programs Method, which adds atoms to (and hence specializes) a logic algorithm so that it is complete wrt a set of given properties. The added atoms are extracted from the proof that the initial logic algorithm is already complete wrt these properties. 

An instantiation of the Discriminate/, predicate-variable tests the values of HX, TX, Y in order to see whether ProcComp/ is applicable. Step 7 yields LA-/ r) by invoking the Proofs-as-Programs Method (see Chapter 9) and generalizing its results via some heuristics. 

For instance, in our case the Proofs-as-Programs Method performs as shown in Example 9-4, where the following instances of Discriminate/ are synthesized ( = 2,...,3) ... 

Note that the Proofs-as-Programs Method wouldn t need to prove that the examples are logical consequences of the input logic algorithm, as we know that LA (r) is already complete wrt Cfr). Moreover, such proofs would result in very specialized discriminants, and hence in the need for considerable generalization afterwards. But the presence of some examples is often necessary within the theories, so that DC/ may reduce atoms of predicate rin in case no property is applicable. The following definition and heuristic capture this ... 

Heuristic 13-6 At Step 7, only provide the properties and property-examples of EP r) as input property set to the Proofs-as-Programs Method. 

Example 13-11 For the compress problem. Step 7 proceeds as in Example 9-4. There is one property-example, namely Ej, so Heuristic 13-6 provides E and the properties of EP(compress) as a property-set to the Proofs-as-Programs Method. The applied generalization heuristics are Heuristic 13-3, Heuristic 13-4, and Heuristic 13-5, respectively. The resulting logic algorithm and its expansion are shown in Example 11-1. 

In Section 11.1, we have constrained the bodies of logic algorithms and properties to be free of negation, namely because the Proofs-as-Programs Method (which is used by Step 7 of the synthesis mechanism) cannot handle negation. As outlined in Section 9.5, this method could be extended to handle negated atoms that have primitive predicates, which would thus overcome the overall restriction. 

---