Automated theorem proving has attracted much attention, notably in the fields of integrated circuit design and software verification. Simplify is an automated theorem prover for first-order formulas. Although it is a research prototype, Simplify has been used as a proof engine in some well-known projects, including extended static checking (ESC), the SLAM Static Driver Verifier, and the Spec# programming system. This paper provides a thorough description of Simplify, which is based on a combination of both mature research results in the field and novel techniques designed for the specific goal of program checking.

Given an arbitrary first-order formula with quantification, it is not always possible to recognize its validity with automatic theorem proving. Nonetheless, in the context of program checking, the goal of Simplify is to find simple proofs rapidly when they exist. Since the queries to Simplify are typically verification conditions for the absence of specific programming errors, rather than general formulas, it appears that the incompleteness is not as essential as the sufficient level of automation and performance.

Simplify handles quantifiers with a matcher that heuristically chooses relevant instances, reducing the query to quantifier-free formulas, which are in turn reasoned with a backtracking search for finding satisfying assignments. This paper documents the key aspects of Simplify, including the combined decision procedures for the theories of equality and linear rational arithmetic, the built-in theories for maps and partial orders, the heuristics for linear integer arithmetic for improving performance, and the pattern-driven instantiation of quantified formulas. It provides both high-level descriptions with examples and detailed algorithms for carrying out the ideas efficiently. It also describes techniques for helping the user determine the reason for an error. Furthermore, it includes performance figures for evaluating the practicality of the techniques and the effectiveness of the heuristics.

Although recent advances in decision procedures have surpassed it on unquantified formulas, Simplify seems to be a good choice for quantified formulas. More importantly, this paper serves as a thorough documentation of Simplify for a wide range of audiences. It is self-contained, so an informed outsider with a background in logic can easily pick up the basics. It also documents efficient implementation details, design alternatives, and potential improvements. Therefore, it is helpful for beginners learning automatic theorem proving, people using Simplify as part of other software, and researchers exploring related solutions.