Course:CPSC-312-2021/ProofChecker
What is the problem?
In the context of mathematical and logical proofs, It can be difficult to confirm the validity of large proofs. We propose a prolog program that is able to answer the question "Do these axioms and this proof lead to this conclusion?" or "what proof reaches this conclusion given these axioms?". We have constructed a checker for Peano arithmetic (in first-order logic with equality, function and relation symbols), a logic powerful enough to state and prove some interesting theorems.
What is the something extra?
The program not only implements the rules of this logic to check them, but can act as a proof assistant: You can provide an incomplete proof (one with "holes"), and the checker will identify all of the holes in the proof and summarize the subgoal that that subproof must show, and additionally what assumptions we are allowed to use in that subproof. For example, if you were proving an implication, and you left a hole underneath the conditional proof for the implication, you'll get a goal for the consequent, with a hypothesis for the antecedent.
What did we learn from doing this?
Going in, we hypothesized that Prolog would be good choice for a proof checker, but we encountered some difficulties that we did not expect. Prolog is well-suited to implementing rules of inference, but has trouble on rules of inference that are not syntax-directed, like the ones for more powerful logics that we initially looked at (like the calculus of constructions). It is also hard to correctly implement logics that have quantifiers, like first-order logic's forall and exists, or lambda calculi. We cannot rely on Prolog's built-in unification to do substitution for us, since it has no understanding of free or bound variables.
Link to code
https://github.com/sjsch/proof-checker
| Guidelines | Create Your Wiki Page | Past Projects | Help and Resources |
| Course title | |
|---|---|
 | |
| Course title | |
| Instructor: | |
| Email: | |
| Office: | |
| Office Hours: | |
| Class Schedule: | |
| Important Course Pages | |
Add a content here. You can also copy and paste content for each tabs from below: