3.9.2. Метатеории рассматриваемой программы

Программа Ж. Питра работает в различных аксиоматиках исчисления высказываний. Она использует восемь мета-метатеорем, приведенных ниже:

Эти мета-ме.татеоремы используются математиками. Чтобы иметь возможность доказывать другие мета-метатеоремы, программа содержит («знает») пять мета-мета-метатеорем. В них символ ! обозначает конъюнкцию, а символ дедукцию (вывод) в мета-мета-метаязыке. Ниже приведены эти мета-мета-метатеоремы (-теоремы);

На рис. 3.22 приведены обозначения операторов конъюнкции и импликации в языках различного уровня.

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

Рис. 3.22. Обозначения логических операторов в языках различного уровня.

приведенных выше. Так, например, когда в какой-то специальной теории доказана формула

то третья МММ-теорема позволит нам вывести из нее следующую мета-метатеорему:

Чтобы программа могла создавать что-то новое, необходимо решить две фундаментальные проблемы:

• Как отбирать интересные результаты?

• Как выбирать контрольные задачи для испытания программы?

Отбор результатов

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

1) выражение считается тем более интересным, чем меньше символов оно содержит;

2) продукция считается тем более интересной, чем ближе антецедент к консеквенту (напомним, что продукция — это порождающее правило, т. е. -теорема с одним или несколькими антецендентами);

3) лучше затратить время на отбор выражений для архива, чем терять его в бесполезных проверках выражений.

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

дают простой результат после значительно более сложных расчетов), всегда сохраняются.

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

Случай с теоремами является более сложным, так как если продукции уже по их определению состоят из антецедентов и консеквента, что позволяет легко производить сопоставление, то теоремы содержат лишь последовательности символов данного языка. Реальная полезность теоремы заключается в том, что она связана с возможными интерпретациями данной формальной системы. Поэтому связи между языком и метаязыком, возникающие в процессе проверки продукций какой-либо теоремы, рассматриваются только с этой точки зрения.