gburel

Pinned Repositories

archsat
A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
Language:OCaml00
coqine
An encoding of the Calculus of Inductive Constructions (as implemented in Coq) in Europa.
Language:OCaml3 3 01
Dedukti
Implementation of the λΠ-calculus modulo rewriting
Language:OCaml00
ekstrakto
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Language:OCaml00
iProverModulo
Extension of iProver to Deduction Modulo Theory
Language:C1 2 00
lambdapi-logics
Logic files for Lambdapi
Language:Makefile00
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 several applications.
Language:OCaml00
lrat2dk
Translation of SAT proofs in LRAT format into Dedukti format
Language:OCaml00
opium
Sinatra like web toolkit for OCaml
Language:OCaml00
SKonverto
A tool to transform proofs containing Skolem symbol in first order logic.
Language:OCaml0 1 00

gburel's Repositories

gburel/coqine
An encoding of the Calculus of Inductive Constructions (as implemented in Coq) in Europa.
Language:OCaml3 3 01
gburel/iProverModulo
Extension of iProver to Deduction Modulo Theory
Language:C1 2 00
gburel/archsat
A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.
Language:OCaml00
gburel/Dedukti
Implementation of the λΠ-calculus modulo rewriting
Language:OCaml00
gburel/ekstrakto
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Language:OCaml00
gburel/lambdapi-logics
Logic files for Lambdapi
Language:Makefile00
gburel/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 several applications.
Language:OCaml00
gburel/lrat2dk
Translation of SAT proofs in LRAT format into Dedukti format
Language:OCaml00
gburel/opium
Sinatra like web toolkit for OCaml
Language:OCaml00
gburel/SKonverto
A tool to transform proofs containing Skolem symbol in first order logic.
Language:OCaml0 1 00
gburel/zenon_modulo
First-order automated theorem prover based on the tableau method
Language:OCaml0 2 00
gburel/zenon
The Zenon theorem prover
Language:OCaml0 0