← All papers
Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory
cs.LO
Sep 2, 2024 · v1
TL;DR
Implements a superposition-based automated theorem prover as a native Lean 4 tactic with proof production.
Abstract
The authors present Duper, a proof-producing theorem prover for Lean based on the superposition calculus. It can be called directly as a terminal tactic in interactive Lean proofs and is designed with proof reconstruction for a future Lean hammer in mind. The paper describes Duper's approach to proof search and proof reconstruction, emphasizing the challenges of working in a dependent type theory, and compares its performance to Metis on pre-existing benchmarks.
Problem
Lean lacks a built-in superposition-based theorem prover that can produce kernel-checkable proof terms, limiting the automation available for first-order reasoning within interactive proofs.
Approach
Duper is a proof-producing theorem prover for Lean based on the superposition calculus. It can be called as a terminal tactic in interactive Lean proofs and reconstructs proof terms compatible with Lean's dependent type theory kernel. The design targets proof reconstruction for a future Lean hammer.
Results
Duper functions as a terminal tactic in Lean proofs and is compared against Metis on pre-existing benchmarks. The paper describes challenges of proof reconstruction in a dependent type theory setting.