dedukti

Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, 31, 2003, pp. 33-72.


References in zbMATH (referenced in 19 articles , 2 standard articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Carette, Jacques; Farmer, William M.; Kohlhase, Michael; Rabe, Florian: Big math and the one-brain barrier: the tetrapod model of mathematical knowledge (2021)
  2. Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
  3. Färber, Michael; Kaliszyk, Cezary: Certification of nonclausal connection tableaux proofs (2019)
  4. Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui: EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract) (2019) arXiv
  5. Blanqui, Frédéric: Size-based termination of higher-order rewriting (2018)
  6. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  7. Ayala-Rincón, Mauricio (ed.); Muñoz, César A. (ed.): Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26--29, 2017. Proceedings (2017)
  8. Cauderlier, Raphaël; Dubois, Catherine: Focalize and dedukti to the rescue for proof interoperability (2017)
  9. Gilbert, Frédéric: Proof certificates in PVS (2017)
  10. Miller, Dale: Proof checking and logic programming (2017)
  11. Cauderlier, Raphaël; Dubois, Catherine: ML pattern-matching, recursion, and rewriting: from focalize to dedukti (2016)
  12. Halmagrand, Pierre: Soundly proving B method formulæ using typed sequent calculus (2016)
  13. Sampaio, Augusto (ed.); Wang, Farn (ed.): Theoretical aspects of computing -- ICTAC 2016. 13th international colloquium, Taipei, Taiwan, ROC, October 24--31, 2016. Proceedings (2016)
  14. Cauderlier, Raphaël; Dubois, Catherine: Objects and subtyping in the (\lambda)-(\Pi)-calculus modulo (2015)
  15. Dowek, Gilles: Deduction modulo theory (2015)
  16. Miller, Dale: Proof checking and logic programming (2015)
  17. Ronan Saillard: Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice (2015) not zbMATH
  18. Delahaye, David; Doligez, Damien; Gilbert, Frédéric; Halmagrand, Pierre; Hermant, Olivier: Zenon modulo: when Achilles outruns the tortoise using deduction modulo (2013)
  19. Cousineau, Denis: On completeness of reducibility candidates as a semantics of strong normalization (2012)