Pinned Repositories
Agda2Dedukti
CoqInE
A Coq plugin to translate Coq proofs into Dedukti terms.
Dedukti
Implementation of the λΠ-calculus modulo rewriting
dkmeta
A tool to rewrite Dedukti terms using rewrite rules
hol2dk
HOL-Light to Dedukti/Lambdapi translator
lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
lean2dk
WIP translation from Lean to Dedukti
Logipedia
An encyclopedia of proofs
SizeChangeTool
A termination checker for higher-order rewriting with dependent types
zenon_modulo
First-order automated theorem prover based on the tableau method
Deducteam's Repositories
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Deducteam/Dedukti
Implementation of the λΠ-calculus modulo rewriting
Deducteam/zenon_modulo
First-order automated theorem prover based on the tableau method
Deducteam/hol2dk
HOL-Light to Dedukti/Lambdapi translator
Deducteam/lean2dk
WIP translation from Lean to Dedukti
Deducteam/coq-hol-light
HOL-Light library in Coq
Deducteam/isabelle_dedukti
Isabelle component generating Dedukti proofs
Deducteam/lambdapi-logics
Logic files for Lambdapi
Deducteam/personoj
People's Verification System in Dedukti
Deducteam/predicativize
A tool for sharing proofs with predicative systems
Deducteam/ekstrakto
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Deducteam/lambdapi-stdlib
Repository of Lambdapi developments
Deducteam/matita_lib_in_agda
Deducteam/nubo
Nubo is a repository of interoperable formal proofs written in Dedukti.
Deducteam/smt2d
Translation from the SMT-LIB language to Dedukti
Deducteam/Sukerujo
Syntactic sugar for Dedukti
Deducteam/Construkti
A double negation translator for higher-order Dedukti proofs
Deducteam/B-in-Dedukti
Implementation of the mathematical theory of the B method in Dedukti
Deducteam/cc-in-dk
Deducteam/Deducteam.github.io
Webpage for Dedukti and related tools
Deducteam/Dedukti-standard
This repository aims to provide documents which describe the Dedukti standard
Deducteam/hol-light
The HOL Light theorem prover
Deducteam/kontroli-rs
Alternative implementation of the logical framework Dedukti in Rust
Deducteam/lambdapi-zenon
Lambdapi library for Zenon
Deducteam/opam-lambdapi-repository
Opam repository of Lambdapi libraries
Deducteam/opam-repository
Main public package repository for opam, the source package manager of OCaml.
Deducteam/pog2why
Translate a POG file into a lambdapi file
Deducteam/PVS
The People's Verification System
Deducteam/sttfaxport
Deducteam/verine
Translation of proofs from the SMT solver veriT to Dedukti