The potential of MetiTarski for interactive theorem proving
Larry Paulson

MetiTarski is an automatic theorem prover for real-valued special
functions including sine and cosine, logarithm, exponential and the
hyperbolic functions. Architecturally, it consists of a superposition
theorem prover (Joe Hurd's Metis) combined with a decision procedure
for real closed fields (QEPCAD). It requires axioms that give upper or
lower bounds -- typically rational functions obtained from power
series or continued fraction expansions -- for special functions. The
prover includes code to simplify algebraic expressions and additional
inference rules to help break down complicated expressions, especially
non-linear products involving special functions. MetiTarski returns
machine-readable proofs that combine standard resolution steps with
the extensions noted above.

If MetiTarski is to be added to an interactive theorem prover as a
trusted oracle, little effort is required other than to ensure that
all problems submitted to it are first-order with all variables
ranging over the real numbers. To reduce the level of trust required,
MetiTarski's various technologies can be treated independently.
Arithmetic simplification in MetiTarski involves little more than
reducing polynomials to canonical form and extending the scope of the
division operator; these steps should be easy to verify by automation
in an LCF-style interactive theorem prover. The axioms used by
MetiTarski are simply mathematical facts that could, in principle, be
developed in any capable interactive theorem prover. Formal
developments of the familiar power series expansions already widely
available. However, expansions based on continued fractions are much
more accurate and hold over wider intervals; the theory of continued
fraction expansions of particular special functions unfortunately
seems to rest on substantial bodies of mathematics that are yet to be
mechanised.

The most difficult obstacle is that of the real closed fields decision
procedure. It uses quantifier elimination to decide logical
combinations of polynomial inequalities. Unfortunately, the algorithms
are complicated and inherently hyperexponential in the number of
variables. We have few implementations to choose from, and until now
there has been little interest in implementing algorithms that justify
their answers with evidence. MetiTarski's proof search does not have
to be justified, only the final proof, which may involve only a few
decision procedure calls. Nevertheless, the few methods that do
deliver evidence (sum of squares, for example) may be hard pressed to
justify even these few calls.

Before undertaking such integration, it is natural to consider
potential applications. MetiTarski seems to have potential in solving
problems that arise in systems specified by linear differential
equations, including hybrid and control systems along with analog
circuits.