catseye / Philomath Star 14 Code Issues Pull requests MIRROR of https://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C) theorem-proving propositional-logic c89 natural-deduction ansi-c theorem-prover proof-checking lcf-style proof-checker Updated Dec 19, 2023 C
timjb / set-theory-prover Star 6 Code Issues Pull requests Simple LCF-style proof assistant for ZFC proof-assistant set-theory lcf-style zfc hilbert-calculus Updated Nov 2, 2017 Haskell
cpressey / LCF-style-ND Star 5 Code Issues Pull requests Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system theorem-proving propositional-logic encapsulation natural-deduction theorem-prover proof-checking lcf-style proof-checker parse-dont-validate cpressey-theory Updated Oct 31, 2023
edoput / lcf-prover Star 5 Code Issues Pull requests silly automated prover for minimal propositional logic silly theorem-prover lcf-style Updated Jun 21, 2019 OCaml
veracruz-project / supervisionary Star 3 Code Issues Pull requests Discussions The Supervisionary proof-checking kernel for higher-order logic theorem-proving webassembly proof-assistant formal-methods formal-verification higher-order-logic theorem-prover privacy-enhancing-technologies lcf-style confidential-computing veracruz Updated May 11, 2022 Rust
FlorianCassayre / lcf-scala Star 1 Code Issues Pull requests Prototype for LCF-style theorem proving, verified by the compiler and execution-less. scala theorem-proving lcf-style Updated Nov 7, 2019 Scala
FlorianCassayre / semester-project Star 0 Code Issues Pull requests Semester Project at LARA (EPFL) epfl set-theory formal-methods automated-reasoning lara lcf-style Updated Nov 21, 2020 Scala