Higher order Proof Reconstruction from Paramodulation-Based Refutations: The Unit Equality Case

In this paper we address the problem of reconstructing a higher order, checkable proof object starting from a proof trace left by a first order automatic proof searching procedure, in a restricted equational framework. The automatic procedure is based on superposition rules for the unit equality case. Proof transformation techniques aimed to improve the readability of the final proof are discussed.

• Type: Conference
• Year: 2007
• Where: MKM
• Authors: Andrea Asperti, Enrico Tassi
• Keywords: Checkable Proof Object, MKM 2007, Order Automatic Proof, Proof Transformation Techniques