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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Asperti, A., & Tassi, E. (2007). Higher order proof reconstruction from paramodulation-based refutations: The unit equality case. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4573 LNAI, pp. 146–160). Springer Verlag. https://doi.org/10.1007/978-3-540-73086-6_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
