Management and Analysis of ATP System Proofs
Abstract
This talk gives an overview of a range of proof management and analysis tools
associated with the Thousands of Problems for Theorem Provers (TPTP) problem
library for Automated Theorem Proving (ATP) systems.
The introduction of the talk provides an overview of ATP, the TPTP, and the
Thousands of Solutions from Theorem Provers (TSTP) solution library.
The body of the talk focusses on the tools for:
selection of problems and solutions,
semantic derivation verification,
rating the interestingness of derived formulae,
interactive viewing of derivations,
computing ratings for problems and systems,
and leveraging the known solutions with ATP.
An application in the cross-verification of a large formal library is
described.