Страница 1 из 3 Любая процедура обратной резолюции, в которой стратегия полной резолюции действует в противоположном направлении, в принципе представляет собой полный алгоритм изучения теорий первого порядка. Это означает, что если на основе некоторой неизвестной гипотезы Hypothesis вырабатывается множество примеров, то процедура обратной резолюции может выработать гипотезу Hypothesis из этих примеров. Такое замечание подсказывает любопытную возможность: предположим, что имеющиеся примеры включают данные о разнообразных траекториях падающих тел. Существует ли такая теоретическая возможность, что программа обратной резолюции позволит вывести логическим путем закон гравитации? Очевидно, что ответ на этот вопрос является положительным, поскольку именно закон гравитации позволяет объяснять все примеры траекторий при использовании подходящего вспомогательного математического аппарата. Аналогичным образом, вполне можно представить себе, что в пределах возможностей программ ILP находится открытие законов электромагнитного поля, квантовой механики и теории относительности. Разумеется, открытие этих законов находится и в пределах возможностей такой экспериментальной установки, в которой обезьяну посадили за пишущую машинку; нужны лишь более качественные эвристики и новые способы структуризации пространства поиска. Но не углубляясь в эти крайности, можно отметить, что системы обратной резолюции действительно позволяют совершать небольшие, но важные открытия — создавать новые предикаты. Такую их способность часто рассматривают как нечто магическое, поскольку компьютеры принято считать устройствами, "просто работающими с тем, что им задано". Но в действительности новые предикаты непосредственно следуют из этапов обратной резолюции. Простейшим случаем создания таких предикатов является преобразование в гипотезы двух новых выражений С1 и С2 на основе выражения С. Применение операции резолюции к выражениям С1 и С2 приводит к удалению в этих двух выражениях общего литерала, поэтому вполне возможно, что удаленный литерал содержал предикат, который не присутствовал в С. Таким образом, при проведении доказательства в обратном направлении одна из возможностей состоит в формировании нового предиката, из которого реконструируется недостающий литерал.
<< В начало < Предыдущая 1 2 3 Следующая > В конец >> |