Online Otter-λ
Examples
The Arithmetic-Geometric Mean Inequality (AGM)
This is the inequality
sqrt(ab) ≤ (a+b)/2.
with the hypotheses 0 ≤ a and 0 ≤ b. To formulate this for resolution theorem-proving, we negate the desired conclusion, obtaining two clauses: a ≠ b and the negation of sqrt(ab) < (a+b)/2. While MathXpert does not require the use of * to explicitly indicate multiplication, Otter does require it, so it is used in the otter-lambda input file and in the proof. Here is the proof produced by Otter-lambda:
2 [] x<=y|y<=x.
3 [] -(x<=y)| -(u<=v)|x+u<=y+v.
4 [] 0<=a.
5 [] 0<=b.
6 [] -(0<=x)| -(x<=y)|x^2<=y^2.
8 [] a!=b.
9 [] -(sqrt(a*b)< (a+b)/2).
10 [simplify,9] a+b<=2* (a*b)^ (1/2).
12 [hyper,10,6,2,simplify,unit_del,8] a<= -b.
20 [hyper,12,3,5,simplify] a<=0.
21 [hyper,12,3,4,simplify] b<=0.
23 [hyper,20,6,4,simplify] a=0.
29 [hyper,21,6,5,simplify] b=0.
41 [para_into,29,23] b=a.
49 [para_into,41,29] 0=a.
50 [para_into,49,41] 0=b.
51 [para_into,50,49] a=b.
52 [binary,51,8] $F.
The proof begins at line 10, simplifying the negation of < to ≤ (reversing the arguments), and writing sqrt as a fractional exponent. The next step is somewhat surprising! A lot has been done for one step. Let's first decipher the hyperresolution step: Here [10] was matched to the second literal of [6], and the first literal of [6] was matched to the first literal of [2], giving the x of [6] (and the y of [2]) the value a+b, and the y of [6] the value 2(ab)^(1/2). The conclusion of the hyperresolution inference is then:
(a+b)^2 <= (2(ab)^(1/2))^2 | a+b <= 0.
This then goes to MathXpert to be simplified. MathXpert squares both sides, subtracts one side from the other, expands the square, collects like terms, factors, and arrives at (a-b)^2 <= 0. The most problematic step is the simplification of ((ab)^(1/2))^2 to ab. This requires the side condition 0 <= ab for its validity. That assumption is available to MathXpert since the call to external simplification passes all unit equalities and inequalities along with the clause being simplified, so actually clauses [4] and [5] are being used here, even though they are not reported as reasons for this step. [We admit, the failure to report them in the justification list is a defect, but it's only a cosmetic defect.]
In earlier versions, only one clause was sent to MathXpert at a time. In such as case MathXpert makes assumptions and returns a clause including the negations of the assumptions it had to make. That would have also worked in this example; the returned clause would have included -(0 <= ab).
Having arrived at (a-b)^2 <= 0, MathXpert isn't finished: it reduces this to a=b. The second literal of the clause passed to MathXpert was a+b <=0. That is "simplified" to a <= -b. The clause finally returned to Otter-lambda by MathXpert is then
a=b | a <= -b.
Since clause [8] is a != b, unit deletion applies to eliminate the literal a=b, leaving as the final result of this step, a <= -b, clause [12]. With so much accomplished in one line of the proof, you would think the proof is almost over. But amazingly, it still requires nine more steps to finish this proof! Those nine lines are adequately explained by their justifications, if you know that MathXpert can simplify a^2 <= 0 to a=0, something that was already mentioned above. No shorter way to finish the proof is obvious, it seems.
This is a fairly simple example of the interactions between proof and computation. As a matter of fact, if you give the problem
sqrt(ab) <= (a+b)/2
to MathXpert under the topic Inequalities, it assumes 0 <= a and 0 < b and produces a much more readable step-by-step justifcation than Otter-lambda does. One could complain that the assumption 0 < b is unnecessary; 0 <=b should suffice, so MathXpert makes an unnecessary assumption; but under that assumption, it does find a correct proof. Otter-lambda has to be told what to assume, and still needs the help of MathXpert to do the algebra. Nevertheless, our aim here is to connect simplification to resolution proof-finding, and other examples certainly can't be done by MathXpert alone (for example, Bernoulli's inequality).