Popular repositories Loading

1. coqine coqine Public

   Forked from mboes/coqine

   An encoding of the Calculus of Inductive Constructions (as implemented in Coq) in Europa.

   OCaml 3 1

2. iProverModulo iProverModulo Public

   Extension of iProver to Deduction Modulo Theory

   C 1

3. logtk logtk Public

   Forked from c-cube/logtk

   Logic toolkit, designed primarily for first-order automated reasoning. It aims at providing basic types and algorithms (terms, unification, orderings, indexing, etc.) that can be factored out of se…

   OCaml

4. opium opium Public

   Forked from rgrinberg/opium

   Sinatra like web toolkit for OCaml

   OCaml

5. lrat2dk lrat2dk Public

   Translation of SAT proofs in LRAT format into Dedukti format

   OCaml

6. Dedukti Dedukti Public

   Forked from Deducteam/Dedukti

   Implementation of the λΠ-calculus modulo rewriting

   OCaml