Topic: "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: 312 KB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 330 - Forks: 11
Chymyst/curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Language: Scala - Size: 413 KB - Last synced at: 3 days ago - Pushed at: over 3 years ago - Stars: 258 - Forks: 16
joom/hezarfen 📦
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
Language: Idris - Size: 48.8 KB - Last synced at: 5 months ago - Pushed at: over 6 years ago - Stars: 119 - Forks: 3
aztek/atp
Haskell interface to automated theorem provers
Language: Haskell - Size: 352 KB - Last synced at: 2 days ago - Pushed at: about 3 years ago - Stars: 9 - Forks: 0
aztek/tptp
Parser and pretty printer for the TPTP language
Language: Haskell - Size: 1.49 MB - Last synced at: 18 days ago - Pushed at: over 3 years ago - Stars: 7 - Forks: 2
pSub/master-thesis
A Language for the Specification and Efficient Implementation of Type Systems
Language: TeX - Size: 1.6 MB - Last synced at: about 2 months ago - Pushed at: about 6 years ago - Stars: 5 - Forks: 1
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 at: over 1 year ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0
kovzol/ag
Towards an Automated Geometer
Language: HTML - Size: 12 MB - Last synced at: 2 months ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 1
curegit/knuth-bendix-completion
クヌース・ベンディックス完備化アルゴリズムの OCaml 実装
Language: OCaml - Size: 67.4 KB - Last synced at: 2 days ago - Pushed at: over 1 year ago - Stars: 2 - Forks: 2
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 at: about 2 years ago - Pushed at: almost 4 years ago - Stars: 2 - Forks: 0
joshuacrotts/masters-thesis
This is a repository for my Master's thesis LaTeX source.
Language: TeX - Size: 21.9 MB - Last synced at: over 1 year ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0
pkel/ocaml-tableau
Basic tableau prover written in ocaml
Language: OCaml - Size: 42 KB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 1 - 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 at: over 1 year ago - Pushed at: almost 2 years ago - Stars: 0 - Forks: 0
rdbliss/prop
Resolution-based theorem proving for propositional logic in Haskell
Language: Haskell - Size: 54.7 KB - Last synced at: about 1 year ago - Pushed at: almost 5 years ago - Stars: 0 - Forks: 0
FelipeCortez/prover
Automated theorem prover for Reasoning @ UoB
Language: Python - Size: 141 KB - Last synced at: 7 days ago - Pushed at: about 10 years ago - Stars: 0 - Forks: 0
