No Choice: Reconstruction of First-order ATP Proofs without Skolem Function
Michael Färber, Cezary Kaliszyk5th Workshop on Practical Aspects of Automated Reasoning, CEUR-WS 1635, pp. 24-31, 2016.
Abstract
Proof assistants based on higher-order logic frequently use first-order
automated theorem provers as proof search mechanisms. The reconstruction
of the proofs generated by common tools, such as MESON and
Metis, typically involves the use of the axiom of choice to simulate the
Skolemisation steps. In this paper we present a method to reconstruct
the proofs without introducing Skolem functions. This enables us to
integrate tactics that use first-order automated theorem provers in logics
that feature neither the axiom of choice nor the definite description
operator.
BibTeX
@inproceedings{mfck-paar16, author = {Michael F{\"{a}}rber and Cezary Kaliszyk}, title = {No Choice: Reconstruction of First-order {ATP} Proofs without Skolem Functions}, pages = {24--31}, booktitle = {Proc. 5th Workshop on Practical Aspects of Automated Reasoning (PAAR 2016)}, year = {2016}, editor = {Pascal Fontaine and Stephan Schulz and Josef Urban}, series = {{CEUR}}, volume = {1635}, publisher = {CEUR-WS.org}, }