Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
Logic in Computer Science
2025-09-18 v2
Abstract
The Vampire automated theorem prover is extended to output machine-checkable proofs in the Dedukti concrete syntax for the LambdaPi-calculus modulo. This significantly reduces the trusted computing base, and in principle eases proof reconstruction in other proof-checking systems. Existing theory is adapted to deal with Vampire's internal logic and inference system. Implementation experience is reported, encouraging adoption of verified proofs in other automated systems.
Keywords
Cite
@article{arxiv.2503.15541,
title = {Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo},
author = {Anja Petković Komel and Michael Rawson and Martin Suda},
journal= {arXiv preprint arXiv:2503.15541},
year = {2025}
}
Comments
10 pages main text, 5 pages references and appendix