Is type theory a required background to make an automated theorem prover?

Question

There's a lot of theory involved in automated reasoning, but why not represent things with any old OOP hierarchy that makes sense?

Do I need to learn another area of math to make something that functions?

Answer 1

It's certainly not necessary. However, many (but not all) theorem provers that let one reason about programs are formulated using type theory in some sense.

Isabelle makes use of some type theory (at least in the definition of it's programming language) but the basic system works in HOL.

ACL2 is a good bet if you both want to reason about computation and avoid type theory.

Personally, I think the reliance on type theory everywhere is a mistake. It's not that type theory isn't mathematically interesting but it introduces too much of an impedance mismatch between how mathematicians reason and how the theorem prover functions. More specifically, the insistence on leveraging the Curry-Howard isomorphism to identify proofs with types makes representation of proof by contradiction very unwieldy (you can do it via the lambda-mu calculus which associates proofs by contradiction with control operators but it's just not a natural fit).

My views seem to sorta be in a minority. I say sotra, because there are a lot of people out there (including people who work on some sub-area of ATP) who just aren't that aware of the issue.