## Writing a Theorem Prover

A place to discuss the implementation and style of computer programs.

Moderators: phlip, Moderators General, Prelates

Kurushimi
Posts: 841
Joined: Thu Oct 02, 2008 12:06 am UTC

### Writing a Theorem Prover

I'm doing a theorem prover for my science fair project. Because I slacked off for quite a while, I have about a month to do it. I was planning to make it to do Geometric proofs. Things like "Prove that the sum of the angles of a triangle is 180 degrees" or "Prove these to segments are congruent". I'm just a little worried. I have a good basic knowledge of propositional and first-order logic and am an average programmer, but I'm not sure if I wasted too much time. What I'm really looking for is some reassurance. Do you think I could a project like this in time?

P.S. Does anyone know any good forums I could to for asking questions about First-Order Logic, or Automated Theorem Proving?

Agent_Irons
Posts: 213
Joined: Wed Sep 10, 2008 3:54 am UTC

### Re: Writing a Theorem Prover

I've thought about doing this once or twice. It's essentially a graph search problem. Every mathematical statement is a tree, and every equation can be applied to other equations.

Then it's just a question of moving outwards in concentric circles. Good luck with this: it's probably pretty tricky.

stephentyrone
Posts: 778
Joined: Mon Aug 11, 2008 10:58 pm UTC
Location: Palo Alto, CA

### Re: Writing a Theorem Prover

A general theorem prover is very interesting, but be aware that getting it to do non-trivial proofs is a bigger undertaking than you might expect at first.

You might start by learning a bit about the language prolog, which is actually itself a limited theorem prover, and is fairly simple to implement an interpreter for. That may give you some ideas for how to get started. It's also just a cool language to know =)
GENERATION -16 + 31i: The first time you see this, copy it into your sig on any forum. Square it, and then add i to the generation.