Ecosyste.ms: Repos
An open API service providing repository metadata for many open source software ecosystems.
GitHub topics: automated-theorem-provers
newca12/awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Size: 279 KB - Last synced: 7 days ago - Pushed: 7 days ago - Stars: 278 - Forks: 9
pSub/master-thesis
A Language for the Specification and Efficient Implementation of Type Systems
Language: TeX - Size: 1.6 MB - Last synced: 25 days ago - Pushed: over 5 years ago - Stars: 5 - Forks: 1
rdbliss/prop
Resolution-based theorem proving for propositional logic in Haskell
Language: Haskell - Size: 54.7 KB - Last synced: 2 months ago - Pushed: about 4 years ago - Stars: 0 - Forks: 0
joom/hezarfen 📦
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
Language: Idris - Size: 48.8 KB - Last synced: 3 months ago - Pushed: over 5 years ago - Stars: 118 - Forks: 3
kovzol/ag
Towards an Automated Geometer
Language: HTML - Size: 12 MB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 1 - Forks: 1
Chymyst/curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Language: Scala - Size: 413 KB - Last synced: 3 months ago - Pushed: over 2 years ago - Stars: 254 - Forks: 14
lambduli/plover
An implementation of Minilog (my other) toy language with a complete search strategy making it a simple, naive, toy theorem prover with Prolog syntax.
Language: Haskell - Size: 2.72 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 3 - Forks: 0
aztek/atp
Haskell interface to automated theorem provers
Language: Haskell - Size: 352 KB - Last synced: 4 days ago - Pushed: over 2 years ago - Stars: 6 - Forks: 0
abtsousa/ProverX-Helper-Functions
Work-in-progress. Small helper Python functions I made while working for LaiTeP in NOVA (Laboratory for Augmented Intelligence in Theorem Proving). ProverX is an extension of Prover9 and is automated theorem prover available at http://proverx.com
Language: Python - Size: 1.95 KB - Last synced: 8 months ago - Pushed: 11 months ago - Stars: 0 - Forks: 0
curegit/knuth-bendix-completion
クヌース・ベンディックス完備化アルゴリズムの OCaml 実装
Language: OCaml - Size: 67.4 KB - Last synced: 9 months ago - Pushed: 9 months ago - Stars: 2 - Forks: 1
joshuacrotts/masters-thesis
This is a repository for my Master's thesis LaTeX source.
Language: TeX - Size: 21.9 MB - Last synced: 10 months ago - Pushed: almost 2 years ago - Stars: 1 - Forks: 0
FelipeCortez/prover
Automated theorem prover for Reasoning @ UoB
Language: Python - Size: 141 KB - Last synced: 11 months ago - Pushed: about 9 years ago - Stars: 0 - Forks: 0
aztek/tptp
Parser and pretty printer for the TPTP language
Language: Haskell - Size: 1.49 MB - Last synced: 5 days ago - Pushed: over 2 years ago - Stars: 6 - Forks: 2
pkel/ocaml-tableau
Basic tableau prover written in ocaml
Language: OCaml - Size: 42 KB - Last synced: about 1 year ago - Pushed: over 6 years ago - Stars: 1 - Forks: 0
elhaddadyacine/ekstrakto Fork of Deducteam/ekstrakto
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Language: OCaml - Size: 117 KB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 2 - Forks: 0
