-- 0^2 + 1^2 + ... + n^2 = n*(n+1)*(2*n+1)/6
test2 := [ n:int; -- n is a variable of type int
def[S; fn(int,int); -- S is a functional constant of type int->int
S(0) = 0 | -- the defining axioms
S(n+1) = S(n) + (n+1)*(n+1) -- for S
]; -- end of definition of S
def[Q; fn(int,int); -- Q is a functional constant of type nat->nat
Q(n) = n*(n+1)*(2*n+1)/6 -- the defining axiom for Q
]; -- end of definition of Q
proof([
F := A[k:nat, S(k) = Q(k)] ; -- for all natural k A(k) = Q(k) - to be proved!
induction(F, basis, D:=def[c; nat; S(c) = Q(c)], step);
-- "induction" is the name of an induction inference rule:
-- To prove F (it must be of the form A[i:nat, P(i)] ) it is sufficient
-- to prove the formulas P(0) (basis) and P(c+1) (step) where the definition
-- of c must be of the form: def[c; nat; P(c)]
basis := S(0) = Q(0);
obvious(basis);
-- "obvious(P)" means that P must be proved by the system ;
-- the short form of "obvious(P)" is "!P" ;
c := D.c; -- without this line the name c would be invisible here
step := S(c+1) = Q(c+1);
expand(step, S(c+1), F1);
-- "expand" is the name of the "expand" inference rule;
-- in this case it means that in the formula step the result of replacement
-- the term "S(c+1)" according to definition of S must yield the formula F1
F1 := S(c) + (c+1)*(c+1) = Q(c+1);
apply(F1, S(c) = Q(c), F2); -- S(c) = Q(c) must be true
-- "apply" is the name of the "apply" inference rule;
-- in this case it means that replacement in F1 the term S(c) on Q(c)
-- must yield the formula F2; this rule is similar to the Subst rule,
-- (in the Subst rule F1 and F2 switch the roles).
F2 := Q(c) + (c+1)*(c+1) = Q(c+1);
expand(F2,Q(c),Q(c+1),F3);
F3 := c*(c+1)*(2*c+1)/6 + (c+1)*(c+1) =
(c+1)*(c+1+1)*(2*(c+1)+1)/6;
obvious(F3) -- using the standard simplification procedure of the
-- system
]) -- end of proof
] -- end of test2
Some other inference rules are:
logic(P0, P1, ... , Pk) - each Pi must be a formula and P0 must
follow from P1, ..., Pk(now this rule is
implemented using a resolution method);
case(P0, C, Q1, ... , Qk) - C must be a disjunction OR(p1,p2, ..., pk);
each Qi must have the form pi -> P0;
P0 is considered to be true if C,Q1,..., Qk
are true.
In the common case an inference rule R is a pair <F, I>, where
F is a boolean valued function defined on the set of all finite
sequences of terms, the first term in such a sequence S must be a formula ;
( this function defines " the applicability conditions" for R;
For instance for the rule induction these conditions are:
1) The length of S is equal to 4;
2) The first element of S has the form A[i:nat, P];
3) The second element of S is P(0);
4) The third element of S has the form def[c; nat; P(c)];
5) The fourth element of S is P(c+1); )
I is a set of numbers of the "input formulas" of R. For instance,
for the induction rule this set is {1,3} ; it means that if an application
of the induction rule has the form "induction(P0, P1, d, P3) then the
formula P0 will be considered as true if the formulas P1 and P3 are true.
It is relatively easy to introduce new inference rules into the system.
Any comments are welcomed. makv@delphi.com