There are lots of different types of theorem prover, but basically they fall into three major categories:
* Boolean (Satisfiability/Model) provers
For example, in the statement:
(L || K) && (!L || !K) && (!L || M) && (!M || K) && (M || R)
for what set of values L,M,K,R is the above statement true?
There are a few methods - the most obvious is to just try all values, and then simplify at the end (you can use a Karnaugh-map to get a simple boolean expression from a truth-table), or there are various better methods.
One such method is the Davis Putnam method (which you can look up for more info if you want) which basically goes along the lines of
Using the notation (for readability) AB = A || B ; A, B = A && B ; a = !A, the above becomes
LK, lk, lM, mK, MR
Since R is pure, we can set R in our model to be true, and the last OR becomes true, so we can get rid of it,
LK, lk, lM, mK (model = {R} )
If L is true:
LK is true, lk is true iff k is true, lM is true iff M is true, mK is unchanged:
k, M, mK
model = {L,R}
If K is also true
Then k is false, and the entire statement is false, so K cannot also be true
Else k is true
Then k is true, M is unchanged, mK is true iff m is true
M, m
model {L,R,K}
But M and m cannot both be true, so contradition
EndIf
So the model {L,R} is not true if we have either K or k to be true, so the model {L,R} doesn't work
Else if l is true
LK is true iff K is true, lk is always true, lM is always true, mK is unchanged
K, mK
model = {l,R}
K is pure in both of the above statements, so we can take it out;
model = {l,R,K}
and we've run out of statements, so setting the values
L = false, R = true, K = true and M = anything will yield true for the original statement\
The next type of theorem prover is the "proper" math style theorem prover, used to generate mathematical proofs. These fall into two general categories of "theorem prover" and "theorem checker", which are basically distinguished by the fact that "theorem provers" are cool, clever and difficult to make, and "theorem checkers" are manual, boring and easy to make. So let's talk about the provers.
For example, Let me tell you that:
1. tan[x] = sin[x] / cos[x]
2. sec[x] = 1 / cos[x]
3. d[sin[x]] = cos[x] * d[x]
4. d[cos[x]] = - sin[x] * d[x]
5. d[a / b] = ( v * d[u] - u d[v] ) / (v^2)
And some helper ones:
6. a * - b = -(a * b)
7. a * a = a ^ 2
8. (a*b) - (c*b) = (a -c) * b
9. (a * b) / b = a (if b is non-zero)
10. (a / b) / c = a/ (b*c)
11. 1 * a = a
12. -sin[x]^2 + cos[x]^2 = 1
13. (a/(b*c)) = (a/b) * (1/c)
What is d [tan[x]] / d[x] ?
d[tan[x]] / d[x]
By rule 1
d[sin[x] / cos[x]] / d[x]
By rule 5 where a = sin[x], b = cos[x]
((sin[x] * d[cos[x]]) - (cos[x] * d[sin[x]]) / cos[x]^2) / d[x]
By rule 4
((sin[x] * - sin[x] d[x]) - (cos[x] * d[sin[x]]) / cos[x]^2) / d[x]
By rule 6
(( -sin[x] * sin[x] * d[x]) - (cos[x] * d[sin[x]]) / cos[x]^2) / d[x]
By rule 7
(( -sin[x]^2 * d[x]) - (cos[x] * d[sin[x]]) / cos[x]^2) / d[x]
By rule 4
(( -sin[x]^2 * d[x]) - (cos[x] * cos[x] * d[x]) / cos[x]^2) / d[x]
By rule 6
((- sin[x]^2 * d[x]) - (cos[x]^2 * d[x])) / cos[x]^2) / d[x]
By rule 8
((-sin[x]^2 + cos[x]^2) * d[x]) / cos[x]^2) / d[x]
By rule 12
((1 * d[x]) / cos[x]^2) / d[x]
By rule 11
(d[x] / cos[x]^2) / d[x]
By rule 10
d[x] / cos[x]^2 * d[x]
By rule 9 (making sure to note that d[x] != 0)
1 / cos[x]^2
By inverse of rule 7
1 / cos[x] * cos[x]
By rule 13
(1 / cos[x]) * (1 / cos[x])
By rule 2
(sec[x]) * (1 / cos[x])
By rule 2
(sec[x]) * (sec[x])
By rule 7
sec[x]^2
So without knowing anything about differentiation, and using the only feature that d[x] != 0, we've derived by application of other rules the general result that the differential of tan with respect to x is the square of the secant of x.
The third type of theorem prover is about program verification (yay!). This is all about showing that a program is correct, typically from contractual specifications, and has applications all over compiler theory (e.g. liveness analysis, program flow analysis, optimisations etc)
For example, in the Spec#-esque function:
class List<T> {
...
T[]! array;
int Capacity { get { return array.Length; } }
void EnsureCapacity(int capacity)
ensures Capacity >= capacity
{
if(capacity <= 0) {
array = new T[0];
}else {
T[] bigger = new T[capacity];
this.CopyIntoArray(bigger);
array = bigger;
}
}
}
Let's check the ensures condition:
{
if(capacity <= 0) {
:: Requires( capacity <= 0)
array = new T[0];
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity];
this.CopyIntoArray(bigger);
array = bigger;
}
:: Ensures ( Capacity >= capacity)
}
Is true only if it's true at the end of the two paths in the if: (Let's also expand out the definition of Capacity at the same time)
if(capacity <= 0) {
:: Requires (capacity <= 0)
array = new T[0];
:: Ensures ( array.Length >= capacity)
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity];
this.CopyIntoArray(bigger);
array = bigger;
:: Ensures ( array.Length >= capacity)
}
if(capacity <= 0) {
:: Requires (capacity <= 0)
array = new T[0]; // <- (new T[X]).Length = X
:: Ensures ( 0 >= capacity)
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity];
this.CopyIntoArray(bigger);
:: Ensures ( bigger.Length >= capacity)
array = bigger;
}
if(capacity <= 0) {
:: Requires (capacity <= 0)
:: Ensures ( capacity <= 0)
array = new T[0]; // <- (new T[X]).Length = X
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity];
:: Ensures ( bigger.Length >= capacity)
this.CopyIntoArray(bigger); // does not affect the Length of bigger
array = bigger;
}
if(capacity <= 0) {
:: Requires (capacity <= 0)
:: Ensures ( capacity <= 0)
array = new T[0]; // <- (new T[X]).Length = X
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity]; <- (new T[capacity]).Length = capacity
:: Ensures ( capacity >= capacity)
this.CopyIntoArray(bigger); // does not affect the Length of bigger
array = bigger;
}
if(capacity <= 0) {
:: Requires (capacity <= 0)
:: Ensures ( true ) ; // guarranteed by the requires condition
array = new T[0]; // <- (new T[X]).Length = X
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity];
:: Ensures (true ) // tautological
this.CopyIntoArray(bigger); // does not affect the Length of bigger
array = bigger;
}
Since any Ensures(true) statement can be eliminated, we've eliminated all ensures contracts from the method, so we've proved that the method was correct! Hooray!
if(capacity <= 0) {
:: Requires (capacity <= 0)
array = new T[0]; // <- (new T[X]).Length = X
}else {
:: Requires( !(capacity <= 0))
T[] bigger = new T[capacity];
this.CopyIntoArray(bigger); // does not affect the Length of bigger
array = bigger;
}
So there you have it, a brief overview of the three forms of theorem provers.
Channel 10: Black Friday Deals on Windows 7 Machines
ASP.NET: Presenting in Europe Next Week
WindowsClient: You know your post rate has gone down...
Silverlight: Geek Profiles – Scott Guthrie
