Deducteam/lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Language: OCaml - Size: 38.8 MB - Last synced at: 4 days ago - Pushed at: 9 days ago - Stars: 328 - Forks: 36

Deducteam/Dedukti

Implementation of the λΠ-calculus modulo rewriting

Language: OCaml - Size: 9.68 MB - Last synced at: 4 days ago - Pushed at: 17 days ago - Stars: 209 - Forks: 23

Deducteam/lean2dk

WIP translation from Lean to Dedukti

Language: Lean - Size: 162 KB - Last synced at: 4 days ago - Pushed at: 11 days ago - Stars: 5 - Forks: 1

Deducteam/Agda2Dedukti

Language: Haskell - Size: 556 KB - Last synced at: 4 days ago - Pushed at: over 3 years ago - Stars: 19 - Forks: 4

Deducteam/Logipedia

An encyclopedia of proofs

Language: OCaml - Size: 61.2 MB - Last synced at: 4 days ago - Pushed at: 6 months ago - Stars: 60 - Forks: 11

Deducteam/zenon_modulo

First-order automated theorem prover based on the tableau method

Language: OCaml - Size: 8 MB - Last synced at: 4 days ago - Pushed at: 6 months ago - Stars: 15 - Forks: 6

Deducteam/coq-hol-light-real-with-N

Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers

Language: Coq - Size: 148 KB - Last synced at: 4 days ago - Pushed at: about 1 month ago - Stars: 1 - Forks: 3

Deducteam/coq-hol-light

HOL-Light library in Coq

Language: Coq - Size: 1.38 MB - Last synced at: 4 days ago - Pushed at: about 1 month ago - Stars: 4 - Forks: 2

Deducteam/opam-repository Fork of ocaml/opam-repository

Main public package repository for opam, the source package manager of OCaml.

Size: 148 MB - Last synced at: 4 days ago - Pushed at: 17 days ago - Stars: 0 - Forks: 0

Deducteam/lambdapi-stdlib

Repository of Lambdapi developments

Language: Answer Set Programming - Size: 172 KB - Last synced at: 4 days ago - Pushed at: about 2 months ago - Stars: 6 - Forks: 7

Deducteam/TranslationTemplates

Language: OCaml - Size: 956 KB - Last synced at: 4 days ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

Deducteam/hol2dk

HOL-Light to Dedukti/Lambdapi translator

Language: Coq - Size: 618 KB - Last synced at: 4 days ago - Pushed at: 2 months ago - Stars: 6 - Forks: 4

Deducteam/CoqInE

A Coq plugin to translate Coq proofs into Dedukti terms.

Language: OCaml - Size: 1.12 MB - Last synced at: 4 days ago - Pushed at: 3 months ago - Stars: 8 - Forks: 4

Deducteam/pog2why

Translate a POG file into a lambdapi file

Language: OCaml - Size: 152 KB - Last synced at: 4 days ago - Pushed at: 3 months ago - Stars: 1 - Forks: 1

Deducteam/lambdapi-logics

Logic files for Lambdapi

Language: Makefile - Size: 32.2 KB - Last synced at: 4 days ago - Pushed at: 4 months ago - Stars: 5 - Forks: 2

Deducteam/coq-hol-light-real-with-nat

Translation in Coq of the HOL-Light definition of real numbers

Language: Coq - Size: 186 KB - Last synced at: 5 days ago - Pushed at: 4 months ago - Stars: 1 - Forks: 1

Deducteam/isabelle_dedukti

Isabelle component generating Dedukti proofs

Language: Scala - Size: 309 KB - Last synced at: 4 days ago - Pushed at: 7 months ago - Stars: 4 - Forks: 5

Deducteam/Construkti

A double negation translator for higher-order Dedukti proofs

Language: OCaml - Size: 1.09 MB - Last synced at: 4 days ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0

Deducteam/personoj

People's Verification System in Dedukti

Language: Common Lisp - Size: 743 KB - Last synced at: 4 days ago - Pushed at: 11 months ago - Stars: 4 - Forks: 2

Deducteam/Dedukti-standard

This repository aims to provide documents which describe the Dedukti standard

Language: TeX - Size: 81.1 KB - Last synced at: 4 days ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0

Deducteam/ekstrakto

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

Language: OCaml - Size: 116 KB - Last synced at: 4 days ago - Pushed at: about 2 years ago - Stars: 3 - Forks: 3

Deducteam/nubo

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

Language: Makefile - Size: 124 KB - Last synced at: 4 days ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 0

Deducteam/B-in-Dedukti

Implementation of the mathematical theory of the B method in Dedukti

Size: 43 KB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

Deducteam/verine

Translation of proofs from the SMT solver veriT to Dedukti

Language: OCaml - Size: 1.37 MB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

Deducteam/smt2d

Translation from the SMT-LIB language to Dedukti

Language: OCaml - Size: 114 KB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 0

Deducteam/predicativize

A tool for sharing proofs with predicative systems

Language: OCaml - Size: 9.9 MB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 6 - Forks: 0

Deducteam/dedukti_set_theory

Language: Makefile - Size: 196 KB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 1 - Forks: 0

Deducteam/SKonverto

A tool to transform proofs containing Skolem symbol in first order logic.

Language: OCaml - Size: 272 KB - Last synced at: 4 days ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 4

Deducteam/ett-in-lambdapi

An implementation of a translation from ETT to MLTT+FunExt+K in lambdapi

Language: Coq - Size: 213 KB - Last synced at: 4 days ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0

Deducteam/dkmeta

A tool to rewrite Dedukti terms using rewrite rules

Language: OCaml - Size: 79.1 KB - Last synced at: 4 days ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 1

Deducteam/Libraries

A collection of hand-written files for Dedukti

Language: Makefile - Size: 93.8 KB - Last synced at: 4 days ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 2

Deducteam/dk2agda

A tool to convert files written in Dedukti to Agda

Language: OCaml - Size: 65.4 KB - Last synced at: 4 days ago - Pushed at: almost 5 years ago - Stars: 1 - Forks: 0

Deducteam/universo

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

Language: OCaml - Size: 7.36 MB - Last synced at: 4 days ago - Pushed at: almost 5 years ago - Stars: 4 - Forks: 1

Deducteam/Holide

A translator from OpenTheory to Dedukti

Language: OCaml - Size: 5.05 MB - Last synced at: 4 days ago - Pushed at: over 5 years ago - Stars: 3 - Forks: 2

Deducteam/SizeChangeTool

A termination checker for higher-order rewriting with dependent types

Language: OCaml - Size: 6.56 MB - Last synced at: 4 days ago - Pushed at: almost 5 years ago - Stars: 10 - Forks: 0

Deducteam/opam-lambdapi-repository

Opam repository of Lambdapi libraries

Language: Shell - Size: 20.5 KB - Last synced at: 4 days ago - Pushed at: 3 months ago - Stars: 0 - Forks: 1

Deducteam/hol-light Fork of jrh13/hol-light

The HOL Light theorem prover

Language: OCaml - Size: 27.6 MB - Last synced at: 4 days ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

Deducteam/Deducteam.github.io

Webpage for Dedukti and related tools

Language: HTML - Size: 137 MB - Last synced at: 4 days ago - Pushed at: 8 months ago - Stars: 0 - Forks: 3

Deducteam/matita_lib_in_agda

Language: Agda - Size: 614 KB - Last synced at: 4 days ago - Pushed at: about 1 year ago - Stars: 3 - Forks: 0

Deducteam/lambdapi-zenon

Lambdapi library for Zenon

Language: Makefile - Size: 24.4 KB - Last synced at: 4 days ago - Pushed at: 10 months ago - Stars: 0 - Forks: 1

Deducteam/cc-in-dk

Language: HTML - Size: 32.1 MB - Last synced at: 4 days ago - Pushed at: over 1 year ago - Stars: 0 - Forks: 0

Deducteam/kontroli-rs Fork of 01mf02/kontroli-rs

Alternative implementation of the logical framework Dedukti in Rust

Size: 770 KB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

Deducteam/sttfaxport

Language: OCaml - Size: 194 KB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 2

Deducteam/agda Fork of agda/agda

Agda is a dependently typed programming language / interactive theorem prover.

Size: 127 MB - Last synced at: 4 days ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

Deducteam/PVS Fork of SRI-CSL/PVS

The People's Verification System

Language: Common Lisp - Size: 183 MB - Last synced at: 4 days ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0

Deducteam/zenon_modulo-lib-gen

Translation script (from BWare to Dedukti) using Zenon Modulo

Language: Shell - Size: 5.86 KB - Last synced at: 4 days ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

Deducteam/HOLLightToDk

Language: OCaml - Size: 20.3 MB - Last synced at: 4 days ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

Deducteam/pvs-with-proofs

Language: Common Lisp - Size: 451 KB - Last synced at: 4 days ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

Deducteam/resystance

Rewrite system stats n' count

Language: OCaml - Size: 104 KB - Last synced at: 4 days ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 2

Deducteam/GeoCoqInE-Tarski

Language: Makefile - Size: 30.3 KB - Last synced at: 4 days ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

Deducteam/GeoCoqInE Fork of GeoCoq/GeoCoq

A formalization of geometry in Coq based on Tarski's axiom system

Language: Coq - Size: 7.31 MB - Last synced at: 4 days ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0

Deducteam/Sukerujo

Syntactic sugar for Dedukti

Language: OCaml - Size: 3.95 MB - Last synced at: 4 days ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 2

Deducteam/Krajono Fork of LPCIC/matita

Matita (proof assistant) with embedded elpi

Language: OCaml - Size: 28.6 MB - Last synced at: 4 days ago - Pushed at: over 6 years ago - Stars: 0 - Forks: 0

Deducteam/dkpsuler

Instantiate constants with dkmeta

Language: OCaml - Size: 7.81 KB - Last synced at: 4 days ago - Pushed at: over 5 years ago - Stars: 1 - Forks: 0

Deducteam/GeoCoqInE-Euclid

Language: Coq - Size: 32.2 KB - Last synced at: 4 days ago - Pushed at: almost 6 years ago - Stars: 0 - Forks: 0

Deducteam/atom-dedukti

Atom mode for Dedukti (Lambdapi)

Language: JavaScript - Size: 1.11 MB - Last synced at: 4 days ago - Pushed at: almost 7 years ago - Stars: 0 - Forks: 0