Moscow-Petersburg seminar on low-dimensional mathematics
April 25, 2003, 16:00, room 311 of PDMI

S.Mechveliani (Pereslavl-Zalessky)
On automated proofs using induction and equational algebra

This is an introductory talk by the beginner in the area of automatic
proofs (the author's field was always computer algebra).

We consider certain simplest proof method for assertions in algebra
and programming based on the equality operations (Term Rewriting),
Knuth-Bendix completion and inductive reasoning.

The particular features of approach are: (1) failless completion,
(2) resource distribution between the current proof goals.

There are considered such examples of assertions as 
"forall N M  (N+M = M+N)"  for the addition algorithm,
" rev(rev(Xs)) = Xs "  for the list reversing.

It is also discussed certain nice modern programming language for
order-sorted term rewriting and the corresponding notions of logic
of models.

The study is in its beginning. Its aim is to find out what 
principles should be added to the program to enable it to solve 
more serious tasks. 

---
http://www.pdmi.ras.ru/~lowdimma