HOL-Light to Dedukti/Lambdapi translator
-
Updated
Aug 1, 2025 - Rocq Prover
#
lambdapi
Here are 7 public repositories matching this topic...
Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat
-
Updated
Aug 1, 2025 - Rocq Prover
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
ocaml tptp vampire automated-theorem-provers dedukti tstp lambdapi zenon-modulo e-prover zipperposition
-
Updated
Jul 6, 2021 - OCaml
Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers
-
Updated
Aug 1, 2025 - Rocq Prover
Translation in Rocq of HOL-Light's Logic library until unify using hol2dk
-
Updated
Aug 7, 2025 - Rocq Prover
Improve this page
Add a description, image, and links to the lambdapi topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the lambdapi topic, visit your repo's landing page and select "manage topics."