Enderton-style sentential and first order logic verifier.
This repository includes three parts (and frontends for the first two):
- A sentential logic proof verifier. A live version of the frontend can be found at sl.shaie.ar
- A first order logic proof verifier. A live version of the frontend can be found at fol.shaie.ar.
- A sentential logic proof generator. This is just a quick demostration that there is a trivial way of generating proofs for sentential logic (given some constraints).
For more information, please see the slides or the technical write-up, which go into more detail about how the project works.
- Sentential logic and first order logic verifiers:
This binaries are mostly meant to be compiled to WASM and run from the frontend, but it is also possible to run them directly.
Make sure go is installed (this is the only dependency) and available in the path. It should be enough to run go build, which will produce a binary accepting a JSON file. See this example for sentential logic and this example for first order logic. Run the binary with -help for more information.
- Frontends:
They are built with Svelte + Vite, so it should be enough to run pnpm install and pnpm run dev. If any modifications are made to the go backend, make sure to compile that to WASM and copy the corresponding file to the public/ subdirectory in the frontend.
- Sentential logic proof generator:
See this example for the input format. Make sure python is installed and available in the path. Run python generate_proof.py <input.json>.
This was made as my final project for MATH069 - Logic at Dartmouth College. I want to thank Professor Daniel Rockmore for this course, and his guidance through the project. The style of proof is based on Enderton's "A Mathematical Introduction to Logic".