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

Обратимся к примеру вывода формулы р Й р. Применим стратегию поиска, выбрав в качестве базовой формулы аксиому . Тогда первая метаформула такова: [p Й [A Й p]] Й [[p Й A] Й [p Й p]], где A - временная переменная. Сформулируем задачу поиска: для получения вывода формулы р Й р необходимо в выводе получить две формулы, структура первой из которых имеет вид p Й [A Й p], а структура второй - p Й A. Заметим, что первая из указанных подзадач решается тривиально, поскольку метаформула p Й [A Й p] по своей структуре совпадает с вариантом аксиомы . Для решения второй подзадачи, заменим A - на метаформулу B Й p, где В - новая временная переменная, тогда метаформула p Й [B Й p] может быть превращена в вариант аксиомы . При этом на структуру метапеременной A накладывается ограничение: A @ B Й p. Метапеременную B сразу заменим на переменную q, что превратит эту метаформулу p Й [B Й p] в аксиому . Обе подзадачи решены, и у нас имеется необходимая информация о соответствии временных переменных и формул исходного исчисления: метапеременная A «замещает» подформулу q Й p, а B - переменную q. Тем самым, ясен набор подстановок в аксиому : переменные s и q заменяем на p, а саму p - на q Й p, после проведения которых мы получим формулу [p Й [q Й p] Й p]] Й [[p Й [q Й p] Й [p Й p]]; и после двух применений к ней и аксиоме (второй раз - к варианту аксиомы ) правила модус поненс получим более короткий и понятный вывод формулы р Й р.

================

— данный текст является расширенными онлайновой версией доклада с учетом выступлений на международных конференциях «Развитие логики в России: итоги и перспективы» (1997), 2-ые «Смирновские чтения» (1999).

Литература:

1. Маслов С.Ю. Теория дедуктивных систем и ее применения. - М.: Радио и связь, 1986.

2. Черч А. Введение в математическую логику. - М.: ИЛ., 1960.
С.Л. Катречко

К методологии построения интеллектуальных систем

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

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

Наиболее перспективной методологией в этом направлении является переход к метаисчислениям, в которых, за счет дополнительной информации о структуре формуле, возможно более эффективно организовать поиск вывода. Для этого создаваемые метаисчисления должны не только «наследовать» свойства исходных исчислений, но и должны быть формульно-ориентированными.

С «процедурной» точки зрения, на которой как правило стоят исследователи, переход к метаисчислениям позволяет формулировать собственно допустимые правила вывода (метаправила), которые и выполняют роль «эвристик».

В этой связи можно задаться двумя вопросами. Во-первых, это вопрос о выразительных особенностях метаисчислений: что делает возможным формулирование метаправил? Во-вторых, это кантовский вопрос: как возможна формулировка метаправил?

Отвечая на первый вопрос, можно сказать, что формулирование метаправил связано с тем, что в метаязыке возможно введение новых абстрактных объектов, в которых «склеиваются» группы объектов «нижнего» уровня. В теории поиска вывода такой подход получил название «метод метапеременных». Тем самым одним из условий повышения эффективности исчислений является увеличение их выразительных возможностей, введение новых абстракций, «языковых фикций» (Гильберт). Однако, как можно заметить, введение новых абстракций предполагает, в свою очередь, постулирование «способности» системы к «схватыванию» идеи решения (Платон), к «синтетическим актам» по выработке таких идей (Кант) . Только в этом случае можно говорить об интеллектуальности систем.

Введенный критерий исключает из разряда интеллектуальных практически все существующие машинные системы «искусственного интеллекта», поскольку в них осуществляется моделирование только «аналитических» процедур.

В заключении отметим, что указание на необходимость моделирования «синтетической» деятельности не означает возврат к психологизму.