Примитивная резолюция. 
Символический искусственный интеллект: математические основы представления знаний

Можно избежать неприятностей, подобных выявленной в примере п. 5.2.3. Один из способов сделать это заключается в следующем.

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

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

В нашей постановке задачи предикат Р и константы 1 и -1 являются примитивными, и им разрешено появляться в программе. Предикат Q — непримитивный, и ему не разрешается попадать в программу.

Дизъюнкт, содержащий предикат ANS, называется жизненным.

После преобразования доказательства в блок-схему те узлы, где был предикат ANS, останутся, а где этого предиката не было — не останутся.

Переменная, входящая в жизненный дизъюнкт, называется жизненной.

Те переменные, которые входят в такой дизъюнкт, останутся в виде переменных программы, а те, которые не входят, не выживут. Они не нужны и являются лишними:

• • —IР (х) v Q (x, 1) — не жизненное предложение;
• • Q (x, -1) v ANS () — жизненное предложение.

Примитивная резолюция — это тот же самый метод резолюций, С_х v L_x, С₂ v -1L₂ —> Ciр, где (р = НОУ(L_v L₂), С = C_{vC_2y на который наложены следующие два ограничения:

• • резольвирование разрешено только, если все константы и функции, которые подставляются вместо лсизненпых переменных в ср, являются примитивными. Это ограничение фактически определяет, какие присваивания мы разрешаем себе синтезировать. Допускается синтез только таких присваиваний, в правых частях которых используются примитивные функции и константы;
• • в случаях, когда оба резольвируемых предложения С_х и С₂ жизненны (а это означает, что у нас в блок-схеме появятся ветвления), требуется дополнительно к указанному выше ограничению, чтобы предикат в литералах L_x и Ь₂ был примитивным, поскольку наиболее общий частный случай литералов появится в проверке условия.

Теорема 5.1 (без доказательства). Примитивная резолюция полна.

Другими словами, если существует какое-либо доказательство по методу резолюций некоторого утверждения, то существует и примитивное доказательство этого утверждения.

Обратимся еще раз к рис. 5.6. В верхушке дерева имеется два нежизненных дизъюнкта, и подстановка допустима. Второй шаг — один дизъюнкт жизненный, а другой — нет. Резольвирование ведется по предикату Q, но подстановка тоже допустима. Третий шаг — оба дизъюнкта жизненные, а резольвирование ведется по предикату Q, который не является примитивным. Другими словами, третий вывод не является примитивным и будет забракован методом примитивной резолюции.

В случае же примера, приведенного на рис. 5.2, легко видеть, что все применения правила резолюции являются примитивными. Они подчиняются обоим ограничениям — ограничению на присваивания и ограничению на ветвления.

Из этих наблюдений можно сделать следующий вывод. Если ограничиться классом линейно-ветвящихся программу то никаких проблем в дедуктивном синтезе нет. Хорошо известный и многократно реализованный метод резолюций, который дополнен техникой предиката ANS и использованием примитивной резолюции, надежно и эффективно решает проблему автоматического дедуктивного синтеза линейных и ветвящихся программ^[1].

• [1] Алгоритм синтеза эффективен, синтезированный алгоритм также эффективен. Однакомыслительные трудозатраты на построение спецификации и применение алгоритма примитивной резолюции превышают мыслительные трудозатраты на написание программы (5.1)по-прежнему в несколько сот раз.