Deducteam/hol2dk

Stars
6
Rank 2,539,965 (Top 51 %)
Language
OCaml
License
Other
Created almost 2 years ago
Updated 5 months ago

Deducteam/hol2dk

Deducteam

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

HOL-Light to Dedukti/Lambdapi translator

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.

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

Sukerujo

Syntactic sugar for Dedukti

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