8.4. Аналогия в доказательстве теорем

Рассуждения по аналогии могут быть использованы в доказательстве теорем. Первым систему для доказательства теорем с помощью правил вывода на основе аналогий создал Клинг в 1971 г. Подобие по Клингу – это образ А во втором из следующих ниже условий для двух заданных теорем Т₁ и Т₂ (Т₁ – доказана, а Т₂ – нет):

1. Т₁ и Т₂ имеют грамматически одинаковые структуры;

2. существует образ А, который сохраняет словарные значения в обозначениях Т₁ и Т₂ (обозначениях предикатов, функций, переменных).

Работа системы Клинга начинается с получения А, который расширяется до образа А для используемых аксиом, затем с помощью А доказательство Т₁ по правилам вывода преобразуется в доказательство Т₂. Однако большинство примеров успешного применения этой системы было связано с Т₁ и Т₂, которые были почти идентичны, система оказалась недостаточно аргументированной и унифицированной, чего нельзя сказать об используемых понятиях и методах.

Область доказательства теорем одновременно с Клингом исследовал Плейстид. Его исследования были связаны с процедурами для нахождения доказательств актуальных в данный момент теорем с использованием доказательств абстрактных теорем. Существенное отличие от системы Клинга состоит в том, что получается соответствие (подобие) уже доказанной теоремы Т₁ и недоказанной теоремы Т₂, никакого вывода на основе этого подобия не делается, а с целью упрощения задачи из Т₂ строится абстрактная теорема Т₂. Следовательно, соответствие между Т₂ и Т₂ полностью известно с самого начала, поэтому, получив «абстрактное доказательство» Р₂ абстрактной теоремы Т₂, можно из Р₂ получить доказательство Р₂ теоремы Т₂.

Подобный метод доказательства теорем по правилам вывода называется стратегией абстрагирования, он показан на рис. 4.

При таком подходе вместо проблемы поиска возникает новая проблема: до какого уровня абстрагировать решение исходной задачи? Плейстид математически определил абстрагирование логических формул и дал одно из решений этой проблемы. Продемонстрируем на простом примере основную идею его решения.

Рис. 4. Стратегия абстрагирования

П ример. Пусть G – ограниченное множество высказываний, а С – высказывание. Будем записывать G C, если из G по правилам вывода можно вывести С. Определим вывод G C с помощью стратегии абстрагирования.

Пусть G ={P(x)  Q(x)  R(x), P(x), Q(a)}, C = R(а). Для доказательства этой теоремы можно использовать методы исчисления предикатов, однако проще это можно сделать с помощью стратегии абстрагирования. Оставим только обозначения предикатов, а все остальное отбросим, получим абстрактную задачу G :

G  ={P  Q  R, P, Q}, C = R. Очевидно, что вывод G C сделать легче, чем вывод G C, ему соответствует следующее дерево вывода:

Т еперь укажем способ вывода G C исходной задачи из вывода G C.

P(x), P(x)  Q(x)  R(x), Q(а) благодаря пропозициональному абстрагированию связывается соответственно с P, P  Q  R , Q . Поэтому рассмотрим метод построения вывода G C, при котором сохраняется каждый вывод, обусловленный абстрагированием (рис. 5). При построении выводимых высказываний С₁ и С₂ сначала перейдем к выводу С₁, С₂, С₃.

В данном примере начнем с вывода Р, P Q R Q R, затем, проверив вывод P(x), P(x)  Q(x)  R(x), получим:

Рис. 5. Перенос вывода на другое множество

P (x), P(x)  Q(x)  R(x) Q(x)  R(x).

Обратим внимание на то, что здесь Q R – это пропозициональное абстрагирование выводимого высказывания Q(x)  R(x). Далее сделаем выводQ R, Q R и получим Q(x)  R(x), Q(a) R(a).

Таким образом, отправляясь от дерева вывода G C, можно получить дерево вывода G C.