Deducteam/rocq-hollight

Translation of HOL-Light libraries in Rocq

langage: Rocq Prover - taille: 215 ko - dernière synchronisation: il y a environ 5 heures - enregistré: il y a environ 13 heures - étoiles: 0 - forks: 0

Deducteam/isabelle_dedukti

Isabelle component generating Dedukti proofs

langage: Scala - taille: 344 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 6 jours - étoiles: 6 - forks: 7

Deducteam/hol2dk

HOL-Light to Dedukti/Lambdapi translator

langage: Rocq Prover - taille: 690 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 15 jours - étoiles: 8 - forks: 6

Deducteam/lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

langage: OCaml - taille: 39,2 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 11 jours - étoiles: 356 - forks: 38

Deducteam/rocq-hollight-logic

Translation of HOL-Light's Logic library in Rocq

langage: Rocq Prover - taille: 748 ko - dernière synchronisation: il y a 4 jours - enregistré: il y a 13 jours - étoiles: 1 - forks: 2

Deducteam/rocq-hollight-logic-unif

Translation in Rocq of HOL-Light's Logic library until unify using hol2dk

langage: Rocq Prover - taille: 600 ko - dernière synchronisation: il y a 4 jours - enregistré: il y a 13 jours - étoiles: 0 - forks: 2

Deducteam/lambdapi-zenon

Lambdapi library for Zenon

langage: Answer Set Programming - taille: 29,3 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 14 jours - étoiles: 1 - forks: 2

Deducteam/lambdapi-stdlib

Repository of Lambdapi developments

langage: Answer Set Programming - taille: 127 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 14 jours - étoiles: 7 - forks: 9

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

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

langage: Rocq Prover - taille: 160 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 14 jours - étoiles: 2 - forks: 5

Deducteam/Dedukti

Type-checker for the λΠ-calculus modulo rewriting

langage: OCaml - taille: 9,7 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 21 jours - étoiles: 223 - forks: 28

Deducteam/opam-lambdapi-repository

Opam repository of Lambdapi libraries

langage: Shell - taille: 25,4 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 20 jours - étoiles: 1 - forks: 2

Deducteam/mathcomp-hollight-real-with-N

Translation in Rocq of the HOL-Light definition of real numbers using MathComp

langage: Rocq Prover - taille: 104 ko - dernière synchronisation: il y a 1 jour - enregistré: il y a 21 jours - étoiles: 0 - forks: 2

Deducteam/zenon_modulo

First-order automated theorem prover based on the tableau method

langage: OCaml - taille: 7,85 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 21 jours - étoiles: 17 - forks: 7

Deducteam/lambdapi-logics

Logic files for Lambdapi

langage: Answer Set Programming - taille: 36,1 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 22 jours - étoiles: 7 - forks: 3

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

Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat

langage: Rocq Prover - taille: 243 ko - dernière synchronisation: il y a 7 jours - enregistré: il y a 22 jours - étoiles: 3 - forks: 2

Deducteam/Logipedia

An encyclopedia of proofs

langage: OCaml - taille: 61,2 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a environ un an - étoiles: 64 - forks: 12

Deducteam/TranslationTemplates

langage: OCaml - taille: 968 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 26 jours - étoiles: 2 - forks: 1

Deducteam/coq-hol-light

Translation of HOL-Light's Multivariate library in Rocq

langage: Rocq Prover - taille: 1,28 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 27 jours - étoiles: 7 - forks: 3

Deducteam/Leo-III-lambdapi-lib

Repository for the Lambdapi encodings of various inference rules and meta-theorems used in the verification of the HOL ATP Leo-III

langage: Answer Set Programming - taille: 114 ko - dernière synchronisation: il y a 4 jours - enregistré: il y a environ 2 mois - étoiles: 0 - forks: 0

Deducteam/dedukti.github.io

Webpage for Dedukti

langage: HTML - taille: 137 Mo - dernière synchronisation: il y a 4 jours - enregistré: il y a environ un an - étoiles: 2 - forks: 4

Deducteam/sublime-lambdapi

Grammar of the Lambdapi language

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

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

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

taille: 154 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 23 jours - étoiles: 0 - forks: 0

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

The HOL Light theorem prover

langage: OCaml - taille: 29 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 2 mois - étoiles: 0 - forks: 0

Deducteam/CoqInE

A Coq plugin to translate Coq proofs into Dedukti terms.

langage: OCaml - taille: 1,14 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a 3 mois - étoiles: 10 - forks: 6

Deducteam/lean2dk

WIP translation from Lean to Dedukti

langage: Lean - taille: 218 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 28 jours - étoiles: 8 - forks: 2

Deducteam/atom-dedukti

Atom mode for Dedukti (Lambdapi)

langage: JavaScript - taille: 1,11 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a plus de 7 ans - étoiles: 2 - forks: 1

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 5 jours - enregistré: il y a environ 7 ans - étoiles: 3 - forks: 1

Deducteam/GeoCoqInE-Euclid

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

Deducteam/HOLLightToDk

langage: OCaml - taille: 20,3 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a environ 6 ans - étoiles: 3 - forks: 1

Deducteam/pvs-with-proofs

langage: Common Lisp - taille: 451 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a environ 6 ans - étoiles: 3 - forks: 1

Deducteam/dkpsuler

Instantiate constants with dkmeta

langage: OCaml - taille: 7,81 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a environ 6 ans - étoiles: 3 - forks: 1

Deducteam/Holide

A translator from OpenTheory to Dedukti

langage: OCaml - taille: 5,05 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a environ 6 ans - étoiles: 5 - forks: 3

Deducteam/GeoCoqInE-Tarski

langage: Makefile - taille: 30,3 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 6 ans - étoiles: 2 - forks: 1

Deducteam/SizeChangeTool

A termination checker for higher-order rewriting with dependent types

langage: OCaml - taille: 6,56 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a plus de 5 ans - étoiles: 12 - forks: 1

Deducteam/dk2agda

A tool to convert files written in Dedukti to Agda

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

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 5 jours - enregistré: il y a plus de 5 ans - étoiles: 6 - forks: 2

Deducteam/Libraries

A collection of hand-written files for Dedukti

langage: Makefile - taille: 93,8 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a environ 5 ans - étoiles: 7 - forks: 2

Deducteam/dkmeta

A tool to rewrite Dedukti terms using rewrite rules

langage: OCaml - taille: 79,1 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 5 ans - étoiles: 7 - forks: 2

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 5 jours - enregistré: il y a presque 4 ans - étoiles: 3 - forks: 1

Deducteam/Agda2Dedukti

langage: Haskell - taille: 556 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 4 ans - étoiles: 21 - forks: 5

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 5 jours - enregistré: il y a plus de 3 ans - étoiles: 3 - forks: 5

Deducteam/resystance

Rewrite system stats n' count

langage: OCaml - taille: 104 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a plus de 3 ans - étoiles: 3 - forks: 3

Deducteam/dedukti_set_theory

langage: Makefile - taille: 196 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a plus de 3 ans - étoiles: 3 - forks: 1

Deducteam/predicativize

A tool for sharing proofs with predicative systems

langage: OCaml - taille: 9,9 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a environ 3 ans - étoiles: 8 - forks: 1

Deducteam/smt2d

Translation from the SMT-LIB language to Dedukti

langage: OCaml - taille: 114 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 3 ans - étoiles: 4 - forks: 1

Deducteam/verine

Translation of proofs from the SMT solver veriT to Dedukti

langage: OCaml - taille: 1,37 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 3 ans - étoiles: 3 - forks: 1

Deducteam/B-in-Dedukti

Implementation of the mathematical theory of the B method in Dedukti

taille: 43 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 3 ans - étoiles: 3 - forks: 1

Deducteam/sttfaxport

langage: OCaml - taille: 194 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 3 ans - étoiles: 2 - forks: 3

Deducteam/Sukerujo

Syntactic sugar for Dedukti

langage: OCaml - taille: 3,95 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 3 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 5 jours - enregistré: il y a plus de 2 ans - étoiles: 4 - forks: 1

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 5 jours - enregistré: il y a plus de 2 ans - étoiles: 5 - forks: 4

Deducteam/cc-in-dk

langage: HTML - taille: 32,1 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 2 ans - étoiles: 2 - forks: 1

Deducteam/matita_lib_in_agda

langage: Agda - taille: 614 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a plus d'un an - étoiles: 5 - forks: 1

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 5 jours - enregistré: il y a plus d'un an - étoiles: 3 - forks: 1

Deducteam/personoj

People's Verification System in Dedukti

langage: Common Lisp - taille: 743 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a plus d'un an - étoiles: 6 - forks: 3

Deducteam/Construkti

A double negation translator for higher-order Dedukti proofs

langage: OCaml - taille: 1,09 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a environ un an - étoiles: 3 - forks: 1

Deducteam/pog2why

Translate a POG file into a lambdapi file

langage: OCaml - taille: 152 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 10 mois - étoiles: 3 - forks: 2

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 5 jours - enregistré: il y a presque 3 ans - étoiles: 0 - forks: 0

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 5 jours - enregistré: il y a presque 4 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 5 jours - enregistré: il y a presque 3 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 5 jours - enregistré: il y a presque 6 ans - étoiles: 0 - forks: 0

Deducteam/Krajono Fork de LPCIC/matita

Matita (proof assistant) with embedded elpi

langage: OCaml - taille: 28,6 Mo - dernière synchronisation: il y a 5 jours - enregistré: il y a presque 7 ans - étoiles: 0 - forks: 0