Correctness proofs for floating point programs are difficult to verify. To simplify the task, a similar, but less complex system, known as logarithmic arithmetic can be used. The Boyer-Moore Theorem Prover, NQTHM, mechanically verified the correctness of a simple implementation of logarithmic arithmetic. It also verified some useful theorems about accumulated relative error bounds for addition, multiplication and division in this logarithmic number system. These theorems were used to verify a program that approximates e^x using a truncated Taylor series. Axioms that characterize the finite precision of the logarithmic system using a rational base, b, were shown by the prover to be satisfiable for any choice of 1 < b < 2. The prover verified the correctness of a function for converting an arbitrary rational value to a logarithmic representation. It also verified that multiplication and division implementations produce exact results for exact inputs, and that addition implementation produces a result as accurate as possible for exact inputs. When these operations are used in combination by a program, such as evaluating a polynomial, the relative error increases in a way that can be bounded by simple expressions, referred to here as tolerances. Several mechanically verified theorems about tolerances allow us to construct mechanically verified proofs about logarithmic arithmetic programs. Although similar to interval arithmetic, tolerances are especially suited to logarithmic arithmetic.

翻译：浮点程序的正确性证明难以验证。为简化该任务，可采用一种相似但复杂度较低的系统，即对数算术。Boyer-Moore定理证明器NQTHM对一种简单对数算术实现的正确性进行了机械化验证。该证明器还验证了在此对数数系中关于加法、乘法与除法累积相对误差界的若干实用定理。这些定理被用于验证一个通过截断泰勒级数逼近e^x的程序。证明器展示了以有理数基数b表征对数系统有限精度的公理对于任意满足1 < b < 2的b值均可满足。证明器验证了将任意有理数值转换为对数表示形式的函数的正确性，同时验证了乘法与除法实现在输入精确时可产生精确结果，且加法实现在输入精确时可产生尽可能准确的结果。当程序组合使用这些运算（例如多项式求值）时，相对误差的增长方式可通过简单表达式（本文称为容差限界）界定。若干关于容差限界的机械化验证定理使我们能够构建关于对数算术程序的机械化验证证明。尽管与区间算术类似，容差限界特别适用于对数算术系统。