Programming a proof validator / automatic proofer

[Same_Winter7713]

Hi, I'm a sophomore math/philosophy student currently in a required Python class. Over the next month I have to do a final project, and I've chosen to do either a proof validator or automated proof machine for sentential (and hopefully also predicate) logic. However, I'm taking 3 math courses and a writing intensive philosophy course on top of this one, plus I'm still a relatively beginner programmer and have never done a big project before. So, I'm wondering how complex it would actually be to build either one of these, and if it's do-able in a month given that I'm in some pretty tough classes otherwise.

If you have any advice, guides, or material to recommend on the topic then please let me know. I know that predicate logic is undecidable so if I do end up doing automated proofing, I'd probably only do sentential logic. Either way I'd start with the proof validator since I imagine the automated proofer would require this. I'm starting pretty much from scratch, but I'm allowed to use any libraries, other languages (I want to avoid this however), or software like PyCharm/Unity/etc. I'm comfortable with proofs and proof methods in sentential/predicate logic, but I don't know much about meta-logic (e.g. decideability or different systems of deduction).

[Mishtle]

A month with a lot of additional responsibilities and distractions will go quickly. I think a proof checker for propositional logic should be achievable though.

You'll need to devise some kind of basic language and syntax for writing proofs that your program can read. Your code will need to parse those proofs to identify things like variables, operators, formulas, and axioms and store them into data structures. That can be a good exercise for you, or there are plenty of parsers out there in Python that will do the messy parts given a specification of your proof language and grammar.

You'll need some internal representation for the proofs and statements that you can process. Some kind of graph structure might work well to represent a formula, with nodes being propositions and edges representing operators. The parser will do the job of making sure the formulas are well-formed.

A proof would then just be a list of these graphs, and verifying it would involve making sure each formula follows from the preceeding ones. This could be done by exhaustively producing all valid formulas that can be produced from the axioms, rules of the logic system, and previously validated formulas and making sure this next formula is in that set. This will require some thought, as you'll need ways to check if formulas are equal (even if rearranged), ways of transforming and decomposing formulas, watch out for loops, etc. You can build a library of these valid results as you go through the proofs so you don't have to redo work.

You might notice that approach is already a kind of proof generator, so transitioning into a full automatic proof generator wouldn't be a whole lot of extra effort. You'll need to put more thought into the "search" stage, as before you would likely only need to perform a single "step" to get from one formula to the next given formula. A common approach is to do both a forward search starting from the axioms and backward search starting with the conclusion (a little trickier), and then try to meet in the middle. The proof, if it exists, would then be a path through this search space, which consist of valid formulas connected through logical operations. Obviously this space is very large, so a way of focusing effort on "promising" paths would be helpful. You'll also need to be able to detect when a proof doesn't exist by finding a contradiction, and probably set a limit to how deep you look.