Solve predicate-variable

An instantiation of the Solve predicate-variable computes, in the minimal case, the value of the other parameter Y from the induction parameter X. An instantiation of the SolveNonMin predicate-variable computes, in the sub-case of the non-recursive case, the value of Y from the decomposition of X. 

Instances of Solve may be defined by fairly complex formulas, including divisions into sub-cases and the corresponding discriminating mechanisms, just as in non-minimal cases. But since this is relatively exceptional, we prefer to keep the schema simple, and always treat such a formula as the instance of a single predicate-variable. 

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. 

The objective at Step 5 is to instantiate the predicate-variables Solve and SolveNonMini of the divide-and-conquer schema. The number v of sub-cases of the non-recursive case must also be found. This amounts to transforming LA (r) into LA5(r) such that it is covered by the following schema ... 

Thus, my conclusion is that to describe safety case arguments, we need a formalism that includes quantification, uninterpieted predicates and constants, set theory, and arithmetic - but the theorem proving needs pushbutton automation only for the unquantified case. These capabilities are (a subset of) the capabihties of formahsms built on, or employing, SMT solvers (i.e., solvers for the problem of Satisfiabihty Modulo Theories) (Rushby 2006). Modem SMT solvers are very effective, often able to solve problems with hundreds of variables and thousands of constraints in seconds. They are the subject of an aimual competition, and this has driven very rapid improvement in both their performance and the range of theories over which they operate. 

---