elhaddadyacine / ekstrakto Star 2 Code Issues Pull requests Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory). ocaml tptp vampire automated-theorem-provers dedukti tstp lambdapi zenon-modulo e-prover zipperposition Updated Jul 6, 2021 OCaml
kernelpanic888 / TMI-OS-Experiment Star 0 Code Issues Pull requests Private passport-compiled experiment domain for TMI-OS: guard dictionary, Lean 4 / Vampire / E build axis, controlled push surface. experiment guard passport formal-methods vampire e-prover lean4 tmi-os Updated Jun 24, 2026 Shell
kernelpanic888 / TMI-Lean-Formal-Library Star 0 Code Issues Pull requests Lean 4 formal library for interface-event theory, OLean boundary checking, claim passports, and TLFL proof-state self-modeling with Z3/Vampire/E mirrors. theorem-proving proof-assistant lean z3 formal-methods tmi e-prover lean4 interface-theory vampire-prover formal-library Updated Jun 29, 2026 Lean