System Feature Description: Importing Refutations into the GAPT Framework

Second Workshop on Proof eXchange for Theorem Proving, PxTP-2012
Manchester, UK


This paper describes a new feature of the GAPT framework, namely the ability to im- port refutations obtained from external automated theorem provers. To cope with coarse- grained, under-specified and non-standard inference rules used by various theorem provers, the technique of proof replaying is employed. The refutations provided by external theo- rem provers are replayed using GAPT’s built-in resolution prover (TAP), which generates refutations that use only three basic fine-grained inference rules (resolution, factoring and paramodulation) and are therefore more suitable to be manipulated by the proof-theoretic algorithms implemented in GAPT.