System Feature Description: Importing Refutations into the GAPT Framework.
Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel S. Weller, Bruno Woltzenlogel Paleo · 2012
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 for manipulation by the proof-theoretic algorithms implemented in GAPT. 1