3.9.3. Выбор контрольных задач для испытания программы

При отборе и проверке результатов программа работает следующим образом. Вначале рассматривается результат, считающийся наиболее существенным. Ниже приводится описание последовательности рассмотрения этих результатов. Если это теорема, к ней применяются все продукции, у которых антецедент упрощает результат (т. е. увеличивает его полезность). Если рассматривается продукция, которая упрощает исходное выражение, ее применяют ко всем хранящимся в архиве программы теоремам и ко всем продукциям, которые усложняют исходные выражения, используя их в качестве антецедентов. Если это продукция, которая усложняет исходное выражение, она применяется к упрощающим продукциям, так же как и к продукциям с несколькими антецедентами. Выполняются не все возможные испытания и проверки продукций и теорем. Это связано с тем, что программа хранит наряду с каждым таким выражением комбинации, в которых оно уже участвовало. Поэтому такие операции не повторяются.

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

Результаты

Программа работает с шестью формальными теориями, построенными Расселом, Лукасевичем, Гильбертом, Бернеем и Шеффером. Она отыскивает все основные теоремы, причем иногда дает для них оригинальные доказательства. При этом используются все заданные метауровни. Программа умеет работать и на уровне предположений: ей задается конкретное выражение и требуется его доказать. Используемые программой стратегии в этом случае мало отличаются от обычных. Она просто инвертирует свои продукции, чтобы перейти от предположения к аксиомам. Во всяком случае, программа преуспела в том, что смогла сама доказать некоторые теоремы, которые ее создатель не смог доказать. Приведем беспристрастное суждение об этом самого Лукасевича: быть очень опытным и искусным в построении логических доказательств, чтобы суметь вывести из трех аксиом логики закон коммутативности или даже закон упрощения Программа Ж. Питра эффективно доказывает оба этих утверждения в рассматриваемой аксиоматике.

Пример доказательства

Аксиомы:

Продукция.

Продукция вначале порождает две мета-метатеоремы благодаря МММ-теоремам, которыми располагает сама программа. Для удобства мы будем использовать при доказательстве форму нотации, принятую в программе (префиксную польскую запись), только лишь для теорем. Программа получает следующие первые результаты:

Например, выводится из мета-мета-метатеоремы И и из с использованием подстановки для для к для с, где запятая употребляется в том смысле, как она используется в мета-метатеореме I программы. Таким образом, получаем

Рассмотрим теперь часть порождающего дерева, которое приводит нас в данном случае к интересной теореме:

(кликните для просмотра скана)

Чтобы достичь этого результата только своими средствами (полностью автономно), программа строит 5 мета-метатеорем, 21 метатеорему и 21 теорему, используя описанные выше процедуры. Отметим при этом важные результаты, полученные попутно в процессе общего доказательства, — это теоремы . Само доказательство теоремы в целом приведено в табл. 3.6. Другие теоремы, доказанные в дайной аксиоматике и при других наборах аксиом, можно найти в работе (Pitrat, 1966).