Supervisionary: a proof-checking system for HOL
-
Updated
May 2, 2023 - Rust
Supervisionary: a proof-checking system for HOL
Math Question Solver
The Supervisionary proof-checking kernel for higher-order logic
Verify equation truth using a custom logical language
A proof assistant based on the internal language of topos with NNO (intuitionistic higher-order arithmetic)
proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.
Razor is a tool for constructing finite models for first-order theories
not noq
First-order logic theorem prover supporting unification with approximate vector similarity
🎼 Translate answer set programs to first-order theorem prover language
Add a description, image, and links to the theorem-proving topic page so that developers can more easily learn about it.
To associate your repository with the theorem-proving topic, visit your repo's landing page and select "manage topics."