A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo

Abstract : The λΠ-calculus modulo is a proof language that has been proposed as a proof standard for (re-)checking and interoperability. Resolution and superposition are proof-search methods that are used in state-of-the-art first-order automated theorem provers. We provide a shallow embedding of resolution and superposition proofs in the λΠ-calculus modulo, thus offering a way to check these proofs in a trusted setting, and to combine them with other proofs. We implement this embedding as a back-end of the prover iProver Modulo.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00921513
Contributor : Guillaume Burel <>
Submitted on : Friday, December 20, 2013 - 3:10:49 PM
Last modification on : Saturday, February 9, 2019 - 1:24:52 AM
Long-term archiving on : Friday, March 21, 2014 - 12:10:49 PM

File

easychair.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00921513, version 1

Citation

Guillaume Burel. A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. PxTP - Third International Workshop on Proof Exchange for Theorem Proving - 2013, Jun 2013, Lake Placid, United States. pp.43-57. ⟨hal-00921513⟩

Share

Metrics

Record views

340

Files downloads

341