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.
Higher order proof reconstruction from paramodulation-based refutations: the unit equality case / A.Asperti; E.Tassi.. - STAMPA. - 4573:(2007), pp. 146-160. (Intervento presentato al convegno MKM 2007 tenutosi a Hagenberg, Austria nel 27 - 30 June 2007).
Higher order proof reconstruction from paramodulation-based refutations: the unit equality case.
ASPERTI, ANDREA;TASSI, ENRICO
2007
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
