Theorem Prover for First-Order Logic

A theorem prover for the full version of first-order logic, available both as a binary and library. For a description of the code and algorithm, refer to report.pdf. The repository is at https://github.com/jchenche/theorem-prover.

Usage

• Output the help menu

$ cargo run -- --help

• Run our prover with sample formulas (refer to first_order.pest or report.pdf for the syntax to write your own)

$ cargo run -- formulas.txt

• Run unit tests (5 seconds)

$ cargo test

• Run end-to-end tests (60 seconds)

$ ./e2e_test.sh