Lean mathematical components library
-
Updated
Apr 9, 2022 - Lean
#
proof-automation
Here are 11 public repositories matching this topic...
-
Updated
Aug 17, 2021 - Haskell
Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker
-
Updated
Sep 2, 2021 - OCaml
Proof automation – for Agda, in Agda.
-
Updated
Sep 7, 2020 - Agda
Ring and field tactics for Mathematical Components
-
Updated
Apr 7, 2022 - Coq
Open
Test suite
2
good first issue
Good for newcomers
joom
commented
Mar 1, 2022
Applying a proof tree moves the proof tree to the right. It should stay stable.
-
Updated
Feb 9, 2022 - Zig
a linear logic prover based on Naoyuki Tamura's llprover that works under SWI Prolog
-
Updated
Oct 8, 2018 - Prolog
multi-logic proof generator
-
Updated
Apr 8, 2022 - Python
The Open Deduction Proof Editor allows proof theorists (or anyone) to deconstruction proofs step by step. It currently supports deep inference formalisms, namely Open Deduction and naturally the Calculus of Structures. The front end of the application is written in Java, while the back end is written in Maude. There is also an implementation of proof search both with and without proof variables.
-
Updated
Nov 12, 2020 - Java
Improve this page
Add a description, image, and links to the proof-automation topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the proof-automation topic, visit your repo's landing page and select "manage topics."
We need a test suite automatically ran by CI, and also extensive test cases to detect regressions. I think it makes sense to include
example.vin it.