Deducteam/Sukerujo

Stars
1
Language
OCaml
License
Other
Created over 6 years ago
Updated over 1 year ago

Deducteam/Sukerujo

Deducteam

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Syntactic sugar for Dedukti

lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Dedukti

Implementation of the λΠ-calculus modulo rewriting

Logipedia

An encyclopedia of proofs

Agda2Dedukti

zenon_modulo

First-order automated theorem prover based on the tableau method

SizeChangeTool

A termination checker for higher-order rewriting with dependent types

CoqInE

A Coq plugin to translate Coq proofs into Dedukti terms.

hol2dk

HOL-Light to Dedukti/Lambdapi translator

predicativize

A tool for sharing proofs with predicative systems

dkmeta

A tool to rewrite Dedukti terms using rewrite rules

Libraries

A collection of hand-written files for Dedukti

lean2dk

WIP translation from Lean to Dedukti

matita_lib_in_agda

universo

A universe reconstruction tool based on Dedukti and the encoding of CiC in Dedukti

personoj

People's Verification System in Dedukti

isabelle_dedukti

Isabelle component generating Dedukti proofs

lambdapi-logics

Logic files for Lambdapi

coq-hol-light

HOL-Light library in Coq

ekstrakto

Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).

lambdapi-stdlib

Repository of Lambdapi developments

Holide

A translator from OpenTheory to Dedukti

zenon_modulo-lib-gen

Translation script (from BWare to Dedukti) using Zenon Modulo

smt2d

Translation from the SMT-LIB language to Dedukti

resystance

Rewrite system stats n' count

pvs-with-proofs

dkpsuler

Instantiate constants with dkmeta

nubo

Nubo is a repository of interoperable formal proofs written in Dedukti.

HOLLightToDk