Automated theorem proving for Metamath

DOI10.4230/LIPICS.ITP.2023.9MaRDI QIDQ6642984zbMATH OpenFDO

Authors Mário D. Carneiro, Chad E. Brown, Josef Urban

Publication date 26 November 2024

Full work available at URL https://doi.org/10.4230/LIPICS.ITP.2023.9

zbMATH Keywords

automated theorem provingformal proof assistantsinteractive theorem provingMetamathproof discovery

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited in

(3)

• Hammering higher order set theory
• Duper: a proof-producing superposition theorem prover for dependent type theory
• Canonical for automated theorem proving in Lean

This page was built for publication: Automated theorem proving for Metamath

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6642984)