Theorem Prover
Authors: Kiana Rashidi, Chester Gould, Oussama Saoudi
Smooth Prove
What is the problem?
We aim to explore the feasibility of implementing a theorem prover for a specific first-order logic set theory. To this aim, we will implement a Smooth Prover for the specific set theory used in the CPSC509 course. We will investigate Prolog's suitability for this task by examining the proof search methods used and the rate of success.
Will Prolog loop and fail? Will it Prove Like Butter?™️
What is the something extra?
We will start by implementing the Smooth Prover only on the zero-th order subset of the logic, and extend it to work with first-order quantifiers after.
What did we learn from doing this?
What is the bottom-line? Is logic programming suitable for (part-of) the task?
1. Prolog is excellent for this task. Since its model of execution is proof search, implementing a system which treats proofs is very natural.
2. Even though our logic isn't decidable, and so we don't expect a computer to be able to prove arbitrary propositions, Prolog's depth first search means that less theorems are inferred than we would have liked.
3. Taking into account 2., the fact that we can write a simple proof checker and get a proof assistant for free is very nice.
Work division
How was the workload divided? Who did what? (This can be in a private communication to the TA if you do not want it to be public).
We all worked together and the work was divided equally.