12.4. Синтаксические стратегии

12.4.0. Введение

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

Различают две основные синтаксические стратегии очищения: - упорядочение и С - упорядочение (Рейтер, 1971). В случае А-упорядочения атомы в множестве как-то упорядочиваются, а в качестве литерала резолюции выбирается атом левого родительского предложения с наибольшим номером. Л-упорядочение можно комбинировать со слиянием и линейным выводом; получающаяся в результате стратегия очищения, использующая слияние, А-упо-рядочение и линейный вывод (а. а. л.), обладает свойством полноты. Эта стратегия упрощает выбор предложений в линейном выводе, диктуя выбор литерала резолюции в случае, когда возможны два литерала. Дерево на рис. 12.9 иллюстрирует как раз такую ситуацию. Однако при Л-упорядочении приходится рассматривать довольно много резолюций. Вторая стратегия, предложенная Рейтером, С-упорядочение, кажется более ограничительной.

12.4.1. С-упорядочение

С-упорядочение также можно комбинировать со слиянием и линейным выводом; получающаяся в результате стратегия очищения, использующая слияние, С-упорядочение и линейный вывод (с. с. л.), обладает свойством полноты. В самом деле, С-упорядочение предполагает линейность, так как при его определении различаются левое и правое родительские предложения. Пусть С — предложение из Обозначим через предложение С с заданным на нем произвольным порядком литералов, а через — множество таких упорядоченных предложений. Если предложение порождается в линейном выводе то пусть

и будут его упорядоченными левым и правым родительскими предложениями с литералами предложения расположенными в порядке т. е. самый правый литерал левого родительского предложения является литералом резолюции), и с литералами предложения в порядке . Ясно, что для некоторого Тогда упорядоченное предложение С таково:

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

Проиллюстрируем С-упорядочение на примере

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

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

Сикел и Хант (1973) расширили применение С-упорядочения, объединив его со слиянием, предпочтением одночленов, использованием подслучаев и линейным выводом. Для этого они переопределили стратегию использования подслучаев, потребовав, чтобы в предложении, являющемся подслучаем другого предложения, литералы этого другого предложения были расположены в том же порядке. Это было необходимо, чтобы в течение всего вывода сохранить С-упорядочение. Кроме того, они ввели стратегию абсолютного предпочтения одночленов, которая означает, что резолюцию с одночленами можно пытаться провести в любом месте вывода независимо от происхождения соответствующего одночлена. В частности, стратегия предпочтения одночленов получила приоритет перед линейной стратегией. Объединение слияния, переопределенной стратегии использования подслучаев, абсолютного

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

Рис. 12.10. Линейное опровержение при помощи С-упорядочения для задачи (98).

Рис. 12.11. Линейное опровержение со слиянием при помощи С-упорядочения.

Стратегия, предложенная Сикелем и Хантом, наиболее полезна в ситуациях, когда объем памяти лимитирован, так как она позволяет удалять из памяти предложение после того, как выведено предложение, для которого первое является подслучаем.