Correctness of Logic Algorithms

Let be the / -ary intended relation. The final objective is to obtain a logic program that succeeds on the /z-tuples of 1, and fails on the /i-tuples of (which is the complement of in the set of all ground /2-tuples over the universe U of terms). 

We now formally define the notion of specified relation. It consists of the set of /2-tuples for which the specified predicate r n is true according to the specification, and of the set of /2-tuples for which r n is false according to the specification  

Definition 7-1 The specified relation of a specification by examples and properties EP r) consists of the following two sets  

It is clear that the specified relation is usually different from the intended relation. It is usually expected to be a subset of the intended relation, though. It is also clear that EP r) is not always the complement of EP (r), We however assume that EP(r) is internally consistent, that is that the intersection between EP (r) and EP (r) is empty. 

A logic algorithm induces a computed relation. It also consists of two sets  

---

This allows a definition of logic algorithm correctness that is only in terms of the specifications of the used predicates. It establishes an equivalence between the specified relation and the set of Herbrand-logical consequences of the logic algorithm. 

Tuning is essential for the correct performance of the system. Thus, measurements of flow and pressure are used to adjust well parameters and pipe friction. Temperature measurements are used to adjust heat transfer coefficients. Single-loop tuning algorithms are used. A system of logic and data validation is used to ensure that bad measurements are not used. 

The idea behind correctness of a logic algorithm wrt its intentions is to state that the intended relation is identical to the relation computed by LA(r) ... 

Correctness thus states an identity, in the Herbrand models of LA(r), between the intended relation and the interpretation of predicate rin. The second condition, which in general is not a consequence of the first one, is necessary to handle logic algorithms with negation (also see [Deville 90]). 

The total correctness of a logic algorithm wrt its intended relation can however be re-expressed more conveniently, yielding what we call the actual criteria ... 

Total correctness thus means that what is computed (positively or negatively) by the logic algorithm must be consistent with its (part of the) specification. For a tuple t where the considered (part of the) specification is undecidable (that is, where t EP (r) and t EP r)), r(t) can be either true or false in the logic algorithm. 

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. 

Example 9-1 Intuitively, the first objective consists of adding atoms to a logic algorithm so that it becomes totally correct wrt a given set of properties. For instance, given the logic algorithm LA(efface) ... 

The latter task cannot be further explained here, as the heuristics are application-specific. A semantic specialization of LA r) would be T(r) re-expressed as a logic algorithm. The most useful specialization is however a syntactic specialization that only adds atoms to the existing disjuncts of LA(r), and hence preserves the existing computations. Indeed, the ultimate objective is not that LA r) be totally correct wrt fP(r), but that LA" r) be totally correct wrt di. So the construction of LA r) is only a useful intermediate step. 

The problem is correctly solved iff the natural extension of (r) is the unknown intended relation This is of course impossible to verify, so the main issue is to infer a logic algorithm that gives maximal confidence that the problem is correctly solved. 

Within a restricted setting, the MSG Method infers, from a finite set of general examples, a non-recursive logic algorithm that is defined in terms of the =/2 primitive only, and that is correct wrt a natural extension of the given examples. The underlying algorithm is non-deterministic. 

---