Deducteam/lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

langage: OCaml - taille: 38,8 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 6 jours - étoiles: 328 - forks: 36

Deducteam/Dedukti

Implementation of the λΠ-calculus modulo rewriting

langage: OCaml - taille: 9,68 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 14 jours - étoiles: 209 - forks: 23

Deducteam/lean2dk

WIP translation from Lean to Dedukti

langage: Lean - taille: 162 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 8 jours - étoiles: 5 - forks: 1

Deducteam/Agda2Dedukti

langage: Haskell - taille: 556 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 3 ans - étoiles: 19 - forks: 4

Deducteam/Logipedia

An encyclopedia of proofs

langage: OCaml - taille: 61,2 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 6 mois - étoiles: 60 - forks: 11

Deducteam/zenon_modulo

First-order automated theorem prover based on the tableau method

langage: OCaml - taille: 8 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 6 mois - étoiles: 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

langage: Coq - taille: 148 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ un mois - étoiles: 1 - forks: 3

Deducteam/coq-hol-light

HOL-Light library in Coq

langage: Coq - taille: 1,38 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a environ un mois - étoiles: 4 - forks: 2

Deducteam/opam-repository Fork de ocaml/opam-repository

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

taille: 148 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 14 jours - étoiles: 0 - forks: 0

Deducteam/lambdapi-stdlib

Repository of Lambdapi developments

langage: Answer Set Programming - taille: 172 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ 2 mois - étoiles: 6 - forks: 7

Deducteam/TranslationTemplates

langage: OCaml - taille: 956 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ 2 mois - étoiles: 0 - forks: 0

Deducteam/hol2dk

HOL-Light to Dedukti/Lambdapi translator

langage: Coq - taille: 618 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 2 mois - étoiles: 6 - forks: 4

Deducteam/CoqInE

A Coq plugin to translate Coq proofs into Dedukti terms.

langage: OCaml - taille: 1,12 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 3 mois - étoiles: 8 - forks: 4

Deducteam/pog2why

Translate a POG file into a lambdapi file

langage: OCaml - taille: 152 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 3 mois - étoiles: 1 - forks: 1

Deducteam/lambdapi-logics

Logic files for Lambdapi

langage: Makefile - taille: 32,2 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 4 mois - étoiles: 5 - forks: 2

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

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

langage: Coq - taille: 186 ko - dernière synchronisation: il y a 3 jours - enregistré: il y a 4 mois - étoiles: 1 - forks: 1

Deducteam/isabelle_dedukti

Isabelle component generating Dedukti proofs

langage: Scala - taille: 309 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 7 mois - étoiles: 4 - forks: 5

Deducteam/Construkti

A double negation translator for higher-order Dedukti proofs

langage: OCaml - taille: 1,09 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 8 mois - étoiles: 1 - forks: 0

Deducteam/personoj

People's Verification System in Dedukti

langage: Common Lisp - taille: 743 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 10 mois - étoiles: 4 - forks: 2

Deducteam/Dedukti-standard

This repository aims to provide documents which describe the Dedukti standard

langage: TeX - taille: 81,1 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ un an - étoiles: 1 - forks: 0

Deducteam/ekstrakto

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

langage: OCaml - taille: 116 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ 2 ans - étoiles: 3 - forks: 3

Deducteam/nubo

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

langage: Makefile - taille: 124 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ 2 ans - étoiles: 2 - forks: 0

Deducteam/B-in-Dedukti

Implementation of the mathematical theory of the B method in Dedukti

taille: 43 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 1 - forks: 0

Deducteam/verine

Translation of proofs from the SMT solver veriT to Dedukti

langage: OCaml - taille: 1,37 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 1 - forks: 0

Deducteam/smt2d

Translation from the SMT-LIB language to Dedukti

langage: OCaml - taille: 114 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 2 - forks: 0

Deducteam/predicativize

A tool for sharing proofs with predicative systems

langage: OCaml - taille: 9,9 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 6 - forks: 0

Deducteam/dedukti_set_theory

langage: Makefile - taille: 196 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 1 - forks: 0

Deducteam/SKonverto

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

langage: OCaml - taille: 272 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ 3 ans - étoiles: 1 - forks: 4

Deducteam/ett-in-lambdapi

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

langage: Coq - taille: 213 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 3 ans - étoiles: 1 - forks: 0

Deducteam/dkmeta

A tool to rewrite Dedukti terms using rewrite rules

langage: OCaml - taille: 79,1 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 4 ans - étoiles: 5 - forks: 1

Deducteam/Libraries

A collection of hand-written files for Dedukti

langage: Makefile - taille: 93,8 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 4 ans - étoiles: 5 - forks: 2

Deducteam/dk2agda

A tool to convert files written in Dedukti to Agda

langage: OCaml - taille: 65,4 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a presque 5 ans - étoiles: 1 - forks: 0

Deducteam/universo

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

langage: OCaml - taille: 7,36 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a presque 5 ans - étoiles: 4 - forks: 1

Deducteam/Holide

A translator from OpenTheory to Dedukti

langage: OCaml - taille: 5,05 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 3 - forks: 2

Deducteam/SizeChangeTool

A termination checker for higher-order rewriting with dependent types

langage: OCaml - taille: 6,56 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a presque 5 ans - étoiles: 10 - forks: 0

Deducteam/opam-lambdapi-repository

Opam repository of Lambdapi libraries

langage: Shell - taille: 20,5 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 3 mois - étoiles: 0 - forks: 1

Deducteam/hol-light Fork de jrh13/hol-light

The HOL Light theorem prover

langage: OCaml - taille: 27,6 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 5 mois - étoiles: 0 - forks: 0

Deducteam/Deducteam.github.io

Webpage for Dedukti and related tools

langage: HTML - taille: 137 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a 8 mois - étoiles: 0 - forks: 3

Deducteam/matita_lib_in_agda

langage: Agda - taille: 614 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a environ un an - étoiles: 3 - forks: 0

Deducteam/lambdapi-zenon

Lambdapi library for Zenon

langage: Makefile - taille: 24,4 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 10 mois - étoiles: 0 - forks: 1

Deducteam/cc-in-dk

langage: HTML - taille: 32,1 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus d'un an - étoiles: 0 - forks: 0

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

Alternative implementation of the logical framework Dedukti in Rust

taille: 770 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 0 - forks: 0

Deducteam/sttfaxport

langage: OCaml - taille: 194 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 0 - forks: 2

Deducteam/agda Fork de agda/agda

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

taille: 127 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 3 ans - étoiles: 0 - forks: 0

Deducteam/PVS Fork de SRI-CSL/PVS

The People's Verification System

langage: Common Lisp - taille: 183 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 2 ans - étoiles: 0 - forks: 0

Deducteam/zenon_modulo-lib-gen

Translation script (from BWare to Dedukti) using Zenon Modulo

langage: Shell - taille: 5,86 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 6 ans - étoiles: 1 - forks: 0

Deducteam/HOLLightToDk

langage: OCaml - taille: 20,3 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 1 - forks: 0

Deducteam/pvs-with-proofs

langage: Common Lisp - taille: 451 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 1 - forks: 0

Deducteam/resystance

Rewrite system stats n' count

langage: OCaml - taille: 104 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a presque 3 ans - étoiles: 1 - forks: 2

Deducteam/GeoCoqInE-Tarski

langage: Makefile - taille: 30,3 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 0 - forks: 0

Deducteam/GeoCoqInE Fork de GeoCoq/GeoCoq

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

langage: Coq - taille: 7,31 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 0 - forks: 0

Deducteam/Sukerujo

Syntactic sugar for Dedukti

langage: OCaml - taille: 3,95 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a environ 2 ans - étoiles: 1 - forks: 2

Deducteam/Krajono Fork de LPCIC/matita

Matita (proof assistant) with embedded elpi

langage: OCaml - taille: 28,6 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 6 ans - étoiles: 0 - forks: 0

Deducteam/dkpsuler

Instantiate constants with dkmeta

langage: OCaml - taille: 7,81 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 1 - forks: 0

Deducteam/GeoCoqInE-Euclid

langage: Coq - taille: 32,2 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a plus de 5 ans - étoiles: 0 - forks: 0

Deducteam/atom-dedukti

Atom mode for Dedukti (Lambdapi)

langage: JavaScript - taille: 1,11 Mo - dernière synchronisation: il y a 1 jour - enregistré: il y a presque 7 ans - étoiles: 0 - forks: 0