System Feature Description: Importing Refutations into the GAPT Framework

Second International Workshop on Proof Exchange for Theorem Proving

Cvetan Dunchev1 ; Alexander Leitsch1 ; Tomer Libal1 ; Martin Riener1 ; Mikheil Rukhaia1 ; Daniel Weller2 ; Bruno Woltzenlogel-Paleo1 ; 1 Institute of Computer Languages (E185)

Others  :  http://ceur-ws.org/Vol-878/paper4.pdf
PID  :  43476

来源: CEUR

【 摘 要 】

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-specied 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 ne-grained inference rules (resolution, factoring and paramodulation) and are therefore more suitable for manipulation by the proof-theoretic