Семинар по маломерной математике Москва-Петербург
25 апреля 2003

        Об автоматическом доказательстве 
        с помощью индукции и алгебры равенств.

        С.Д.Мешвелиани 
        Институт программных систем, Переславль-Залесский.

Это вводный доклад "от начинающего для начинающих".
Докладчик 13 лет занимался вычислительной алгеброй и ее 
программированием. Год назад начал изучать смежную область: 
автоматическое доказательство в алгебре. 

Рассматривается простейший алгоритм доказательства утверждений в 
алгебре и программировании, основанный на действиях с равенствами
(переписывании термов), пополнении по Кнуту-Бендиксу.  
Вывод по индукции выражается через добавление равенств.
Особенность способа состоит в (1) "без-тупиковом" пополнении,
(2) приеме распределения запаса шагов.
Способ применяется к таким примерам как  "для любых N,M  N+M = M+N"  
для алгоритма сложения,  rev(rev(Xs)) = Xs  для программы 
переворачивания списка. Данные алгоритмы выражены в виде множеств 
равенств. 
Попутно рассматривается привлекательный современный язык 
программирования для логики равенств и соответствующие понятия логики 
моделей.
Цель: узнать как можно определеннее, чего не хватает программе для 
успешного решения многих более содержательных задач.
Затруднений много. Например: как автоматически и удачно выбирать 
выражение для индукции.