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.