| Abstract: | In various applications of theorem proving, they not only check if a theorem holds true but also need a proof of the theorem, e.g., spurious counterexample analysis in verification.
The proofs can be presented in various formats to a user. Not all proof formats are conducive to the need of a user. The user may prefer one proof system over another. A user may prefer to have concise proofs, and other may like to have detailed proofs that allow inexpensive proof checking. Furthermore, there is no commonly acceptable API or file format for proof output. This situation allows the provers to produce proofs that are mutually incompatible and do not match the need of the users. Producing a proof after a run of an efficient and complex theorem prover is not a straight forward task. For example, the provers may apply various simplifications on input formulas before running the core proving algorithms. Such simplifications should be added as proof steps in the generated proofs. In long and arduous development process of a theorem prover, developers may forget to provide proper annotations to all the deduction steps such that a sufficiently detailed proof can be generated.
Currently, a Vampire proof only contains the information about the antecedents of the deduced clauses and the proof rule that is used to produce the clauses. This proof format leaves out various details. For example, an application of the superposition rule does not specify the terms that were unified to obtain the consequences. We propose to develop a comprehensive proof format and API that allows proofs with different level of granularity and are easy to use. |
