No choice: Reconstruction of first-order ATP proofs without skolem functions. Färber, M. & Kaliszyk, C. CEUR Workshop Proceedings, 1635(Paar):24--31, 2016.
abstract   bibtex   
Copyright ? by the paper's authors.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.
@article{Farber2016,
abstract = {Copyright ? by the paper's authors.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.},
author = {F{\"{a}}rber, Michael and Kaliszyk, Cezary},
file = {:Users/jonaprieto/Mendeley/F{\"{a}}rber, Kaliszyk - 2016 - No choice Reconstruction of first-order ATP proofs without skolem functions.pdf:pdf},
issn = {16130073},
journal = {CEUR Workshop Proceedings},
number = {Paar},
pages = {24--31},
title = {{No choice: Reconstruction of first-order ATP proofs without skolem functions}},
volume = {1635},
year = {2016}
}

Downloads: 0