Skip to Main content Skip to Navigation
Conference papers

A Proof-Theoretic Approach to Certifying Skolemization

Kaustuv Chaudhuri 1 Matteo Manighetti 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : When presented with a formula to prove, most theorem provers for classical first-order logic process that formula following several steps, one of which is commonly called skolemization. That process eliminates quantifier alternation within formulas by extending the language of the underlying logic with new Skolem functions and by instantiating certain quantifiers with terms built using Skolem functions. In this paper, we address the problem of checking (i.e., certifying) proof evidence that involves Skolem terms. Our goal is to do such certification without using the mathematical concepts of model-theoretic semantics (i.e., preservation of satisfiability) and choice principles (i.e., epsilon terms). Instead , our proof checking kernel is an implementation of Gentzen's sequent calculus, which directly supports quanti-fier alternation by using eigenvariables. We shall describe deskolemization as a mapping from client-side terms, used in proofs generated by theorem provers, into kernel-side terms, used within our proof checking kernel. This mapping which associates skolemized terms to eigenvariables relies on using outer skolemization. We also point out that the removal of Skolem terms from a proof is influenced by the polarities given to propositional connectives.
Document type :
Conference papers
Complete list of metadata

Cited literature [36 references]  Display  Hide  Download

https://hal.inria.fr/hal-02368946
Contributor : Dale Miller <>
Submitted on : Tuesday, November 19, 2019 - 11:51:07 AM
Last modification on : Friday, April 30, 2021 - 10:02:41 AM
Long-term archiving on: : Thursday, February 20, 2020 - 3:26:52 PM

File

skolem-draft.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller. A Proof-Theoretic Approach to Certifying Skolemization. CPP 2019 - 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩. ⟨hal-02368946⟩

Share

Metrics

Record views

90

Files downloads

552