Deducteam/Logipedia Deducteam/Logipedia

  • Stars
    star
    56
  • Rank 530,104 (Top 11 %)
  • Language
    OCaml
  • Created over 6 years ago
  • Updated over 2 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
Deducteam/Logipedia
github

Deducteam

Reviews

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

Repository Details

An encyclopedia of proofs

More Repositories

1

lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
OCaml
268
star
2

Dedukti

Implementation of the λΠ-calculus modulo rewriting
OCaml
198
star
3

Agda2Dedukti

Haskell
16
star
4

zenon_modulo

First-order automated theorem prover based on the tableau method
OCaml
11
star
5

SizeChangeTool

A termination checker for higher-order rewriting with dependent types
OCaml
9
star
6

CoqInE

A Coq plugin to translate Coq proofs into Dedukti terms.
OCaml
7
star
7

hol2dk

HOL-Light to Dedukti/Lambdapi translator
OCaml
6
star
8

predicativize

A tool for sharing proofs with predicative systems
OCaml
5
star
9

dkmeta

A tool to rewrite Dedukti terms using rewrite rules
OCaml
4
star
10

Libraries

A collection of hand-written files for Dedukti
Makefile
4
star
11

lean2dk

WIP translation from Lean to Dedukti
Lean
4
star
12

matita_lib_in_agda

Agda
3
star
13

universo

A universe reconstruction tool based on Dedukti and the encoding of CiC in Dedukti
OCaml
3
star
14

personoj

People's Verification System in Dedukti
Common Lisp
3
star
15

isabelle_dedukti

Isabelle component generating Dedukti proofs
Scala
3
star
16

lambdapi-logics

Logic files for Lambdapi
Makefile
3
star
17

coq-hol-light

HOL-Light library in Coq
Coq
3
star
18

ekstrakto

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

lambdapi-stdlib

Repository of Lambdapi developments
Makefile
2
star
20

Holide

A translator from OpenTheory to Dedukti
OCaml
2
star
21

zenon_modulo-lib-gen

Translation script (from BWare to Dedukti) using Zenon Modulo
Shell
1
star
22

Sukerujo

Syntactic sugar for Dedukti
OCaml
1
star
23

smt2d

Translation from the SMT-LIB language to Dedukti
OCaml
1
star
24

resystance

Rewrite system stats n' count
OCaml
1
star
25

pvs-with-proofs

Common Lisp
1
star
26

dkpsuler

Instantiate constants with dkmeta
OCaml
1
star
27

nubo

Nubo is a repository of interoperable formal proofs written in Dedukti.
Makefile
1
star
28

HOLLightToDk

OCaml
1
star