What does it do?
It checks your proofs. Suppose you have a potential proof of X and you want to be sure that your proof is correct. X might be a statement of mathematics, philosophy, theology, etc. You just have to write your proof in the language of Oak, and then Oak will tell you whether or not it is correct.
What doesn't it do?
It doesn't write the proof for you. Rather, it gives you a formal language in which to write a proof, and then checks that the proof is correct.
How does it work?
Oak translates each step of your proof into a statement of first-order logic, and passes it to an external theorem prover called E
. The prover then checks whether the given statement is valid. If it is, Oak proceeds to the next step of your proof. If it isn't, or if the prover exceeds a certain "amount of work", Oak stops and tells you there was a problem.
What does it look like?
Here is a simple example of a proof written in the language of Oak.
axiom every man is mortal
axiom Socrates is a man
so Socrates is mortal
Here is a more complicated example. This proof, and the included file "peano.oak", are available in Oak's examples directory.
# natural numbers are closed under addition
for all a,b in N, a+b is in N
# define a property to be used for induction
P_def: for some P, for all a in N,
P(a) iff for all b in N, a+b is in N
P(0) by P_def, peano # base case
1: take any a in N
2: suppose P(a) # induction hypothesis
3: take any b in N
a+b is in N by P_def, 1, 2, 3
so (a+b)+1 is in N by peano
so (a+1)+b is in N by peano, 1, 3
so P(a+1) by P_def, peano, 1
so for all a in N, P(a) by induction
so thesis by P_def
Who made it?
Oak was created by Tim Smith