dedukti
From MaRDI portal
Dedukti
Cited in
(32)- Objects and subtyping in the \(\lambda\)-\(\Pi\)-calculus modulo
- FoCaLiZe and Dedukti to the rescue for proof interoperability
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Proof checking and logic programming
- Size-based termination of higher-order rewriting
- Proof certificates in PVS
- Proof checking and logic programming
- Soundly proving B method formulæ using typed sequent calculus
- Certification of nonclausal connection tableaux proofs
- scientific article; zbMATH DE number 7178363 (Why is no real title available?)
- Zenon
- On completeness of reducibility candidates as a semantics of strong normalization
- BWare
- FoCaLiZe
- CoqMTU
- CoqMT
- GAPT
- CompCertS
- cubicaltt
- ProofScript
- Meta Dedukti
- Focalide
- CoqInE
- ArchSAT
- ekstrakto
- Logipedia
- OpenTheory
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
- Theoretical aspects of computing -- ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24--31, 2016. Proceedings
- Tactics and certificates in Meta Dedukti
- Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings
This page was built for software: dedukti
