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 firstorder 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 FirstOrder Logic, or Automated Theorem Proving?
Writing a Theorem Prover
Moderators: phlip, Moderators General, Prelates

 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.
Then it's just a question of moving outwards in concentric circles. Good luck with this: it's probably pretty tricky.

 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 nontrivial 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 =)
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.
Who is online
Users browsing this forum: No registered users and 7 guests