The Eagle automated theorem prover



Welcome to the future home of the eagle automated theorem prover, right now the project is focused more upon writing a theorem prover for first order logic than writing a web site about said prover, but perhaps you could check out the temporary page for the Eagle automated theorem prover.
What is Eagle?
Eagle is an automated theorem prover for first order predicate logic. Given a set of axioms (truths by definition) of the universe of discourse, Eagle will be able to prove that a theorem holds. The main Eagle kernel will be written to use different methods, and an emphasis on the comparison of these methods is taken. Among the methods are binary resolution, davis putnam algorithms, tableau methods.
How can we prove a theorem using a machine?
Proofs constructed by automated theorem provers are not the same kind as those written by humans, which usually follow a logical path and have an element of beauty. Proofs by automated methods are usually refutation based proofs; instead of showing that the theorem must be right, mechanical proofs show that the theorem cannot be wrong. The basic idea is usually to show that the conjunction of the axioms and negated theorem yield a set which is unsatisfiable (i.e. there is no interpretation that can make the set correct). Because of the law of the excluded middle, the theorem must be correct.

Unfortunately, that's all there is now, hope to see you back later.