How do proof-writing programs work?

This is a pretty complicated topic! I can't tell you how they work because I don't know. But I can point you in the right direction.

The first thing to keep in mind is that there's a difference between automated theorem proving and proof assistants. The purpose of a proof assistant is to verify proofs, it may contain some automated theorem proving stuff, but it doesn't need to. Automated theorem proving is for... automated theorem proving.

The idea behind most techniques in automated theorem proving that I've seen are entirely proof theoretical. What I mean by this is that they look either exploit the structure of a formula (i.e., horn clauses and resolution) or perhaps they exploit the structure of the proof system itself (i.e., focusing and the sequent calculus).

Where to look next? Pfenning has some great lecture notes on automated theorem proving. There's also the Handbook of Practical Logic and Automated Reasoning. I also know that Ebbinghaus-Thomas-Flum has an introduction to resolution in its later chapters.

/r/math Thread