Input Welcome

Stream: new members

[Johan Commelin]

@Dania Ali This stream is the right place for that

[Dania Ali]

Great! Well, I'm still in the initial stages of my project so I have no concrete plan yet. I am thinking about how to auto-generate proofs for very simple theorems (from an undergrad course). The theorems are related to simple programming functions, so perhaps more complicated than theorems on propositional formulas.

[Dania Ali]

I've come across a paper from microsoft called "Automatically Generating Problems and Solutions for Natural Deduction" and their approach is to create a "Universal Proof Graph" where the nodes are truth tables and the edges are Inference rules (like Modus Ponens etc.), then their algorithm searches that data structure to generate a proof. I am wondering if I can do something similar but truth tables seem not to apply here. I am trying to come up with an approach.