How might one prove a calculation correct. The usual approach is to prove the algorithm correct, prove that the implementation (if different) is a correct implementation of the algorithm, and then the calculation by this algorithm/implementation is correct. However, it may not be possible to prove that the algorithm is correct, or that the implementation is correct. In this case, an alternative is for the implementation, while performing the calculation, to produce enough intermediate information that a proof engine, using these as hints, can then construct a proof of correctness of THIS calculation, rather than correctness of the general algorithm/implementation. We discuss this methodology in the context of real algebraic geometry (i.e. NRA in SMT-language).
Copyright. All Rights Reserved.