Cтраница 3
То же самое можно сказать и о принципе ( 4) - при резольвирова-нии по связи, содержащей подстановку константы вместо переменной, мы получаем в результате дизъюнкт, содержащий константные термы. Подобный дизъюнкт имеет, во-первых, малое число связей, а во-вторых, может быть эффективно использован при резольвировании. [31]
Для графов связей проблема поиска контрарной пары решается путем сохранения информации о потенциально резольвируемых предикатах в графе связей. Таким образом, установление потенциальной резольвируемости производится один раз при создании графа связей, и нет необходимости в просмотре всего множества дизъюнктов на каждом шаге резольвирования - достаточно лишь просмотреть дизъюнкты, полученные в результате резольвирования на последнем шаге. [32]
Проблема поиска контрарных пар решается путем сохранения информации о потенциально резольвируемых предикатах в графе связей. Таким образом, установление потенциальной резольвируемости производится один раз при создании графа связей, и нет необходимости в просмотре всего множества дизъюнктов на каждом шаге резольвирования - достаточно лишь просмотреть дизъюнкты, полученные в результате резольвирования на последнем шаге. Исключение дизъюнктов, которые не могут быть использованы в доказательстве, достигается с помощью простой процедуры нахождения чистых литер. [33]
В данной ситуации особое значение приобретает способность алгоритма проводить направленный вывод, не генерировать излишних дизъюнктов, а также быстро определять кандидатов на резольвиро-вание и получать соответствующую резольвенту. Подобным требованиям удовлетворяют алгоритмы дедуктивного вывода на графах связей, так как пространство поиска на каждом шаге является легко обозримым ( в графе одновременно хранится информация обо всех кандидатах на резольвирование), дизъюнкты, которые не могут результативно участвовать в процессе вывода ( дизъюнкты с чистыми литерами - литерами без связей), удаляются из графа связей вместе со всеми связями, значительно упрощая его структуру. Быстрота вывода обеспечивается однократным вычислением и постоянным хранением унификатора для каждой связи. Также достоинством процедуры вывода на графе связей является возможность адаптации существующих алгоритмов для вывода на графе связей, что позволяет комбинировать достоинства существующих алгоритмов вывода и алгоритмов вывода на графах связей. Недостатками процедуры вывода на графе связей являются необходимость пересчета графа связей на каждом шаге резольвирования с вычислением новых связей и унификаторов и необходимость хранения всего графа связей в оперативной памяти. Параллельный вывод на графах связей позволяет частично решить проблему необходимости пересчета графа на каждом шаге резольвирования, так как одновременно резольвируются несколько связей. Недостатком процедур параллельного вывода является генерация некоторого количества бесполезных, лишних дизъюнктов, что вытекает из самого принципа организации параллельного вывода, когда резольвируются все связи одновременно. [34]
Для графов связей проблема поиска контрарной пары решается путем сохранения информации о потенциально резольвируемых предикатах в графе связей. Таким образом, установление потенциальной резольвируемости производится один раз при создании графа связей, и нет необходимости в просмотре всего множества дизъюнктов на каждом шаге резольвирования - достаточно лишь просмотреть дизъюнкты, полученные в результате резольвирования на последнем шаге. [35]
Проблема поиска контрарных пар решается путем сохранения информации о потенциально резольвируемых предикатах в графе связей. Таким образом, установление потенциальной резольвируемости производится один раз при создании графа связей, и нет необходимости в просмотре всего множества дизъюнктов на каждом шаге резольвирования - достаточно лишь просмотреть дизъюнкты, полученные в результате резольвирования на последнем шаге. Исключение дизъюнктов, которые не могут быть использованы в доказательстве, достигается с помощью простой процедуры нахождения чистых литер. [36]
Количество успешных унификаций также не является универсальной характеристикой для оценки эффективности, так как в этом случае не учитывается количество неудачных попыток унификации и не рассматривается проблема нахождения произведения унификаторов. В графе связей, как было сказано выше, нет необходимости в нахождении контрарных пар для полученных дизъюнктов резольвент, так как они наследуют связи дизъюнктов-родителей, а унификаторы новых связей вычисляются путем объединения унификатора связи, по которой проводилось резольвирование, и унификатора связи дизъюнкта-родителя. [37]
Это достигается путем изменения процедуры выбора связи для резольвирования. Так, например, метод гиперрезолюции может быть встроен в процедуру вывода на графе связей. Таким образом, алгоритм дедуктивного вывода на графе связей позволяет аккумулировать в себе достоинства других методов. [38]
Такие характеристики, как число промежуточных дизъюнктов и число унификаций, являются более общими, но и к их использованию стоит относиться внимательно. Например, некоторые из использованных методов позволяют получать резольвенту путем одновременного резольвирования по нескольким дизъюнктам, поэтому такая характеристика, как число промежуточных дизъюнктов меняет свой смысл. В случае использования алгоритмов параллельного вывода может быть более полезным использование характеристики количество шагов вывода, так как на каждом шаге резольвирования мы можем получить больше чем один дизъюнкт. [39]
Отметим, что из всех типов параллельного вывода наиболее требовательным к выбору эвристики является DCDP-параллельный вывод. Таким образом, нельзя исключить из выбранного множества связей те связи, резольвирование по которым на данном шаге может оказаться бесполезным или малоэффективным. Естественно, при выборе дизъюнкта в AND-параллельном резольвировании или предикатной литеры в OR-параллельном выводе, используются различные функции эвристической оценки, но данные оценки распространяются на все множество связей в целом, в то время как при DCDP-параллельном выводе происходит последовательный отбор связей, и на каждом шаге добавляется связь, удовлетворяющая условиям и имеющая наилучшее значение оценки. [40]
Особенно заметно это проявляется при достаточно большом количестве дизъюнктов. В наиболее неудачных случаях требуется просмотреть все множество дизъюнктов, прежде чем будет найдена контрарная пара предикатов для резольвирования. Много времени занимает проверка возможности резольвирования предикатов, которые не резольвируемы. [41]
Как было указано выше, при выборе связи для резольвирования в графе связей можно использовать различные эвристические функции оценки. В случае параллельного резольвирования необходимо делать выбор множества связей, отвечающих некоторым условиям. Стоит отметить, что неудачный выбор связи может привести к экспоненциальному росту количества дизъюнктов при решении сложных задач, что сделает процедуру вывода практически непригодной. В то же время удачный выбор связи может значительно увеличить эффективность процедуры вывода. Например, резольвирование единственной связи предикатной литеры в дизъюнкте приведет к появлению так называемого чистого дизъюнкта, который должен быть удален. Удаление чистого дизъюнкта в свою очередь может привести к каскадному удалению других дизъюнктов и к эффекту снежного кома. В результате структура графа связей может значительно упроститься. [42]
Особенно заметно это проявляется при достаточно большом количестве дизъюнктов. В наиболее неудачных случаях требуется просмотреть все множество дизъюнктов, прежде чем будет найдена контрарная пара предикатов для резольвирования. Много времени занимает проверка возможности резольвирования предикатов, которые не резольвируемы. [43]
Отметим, что из всех типов параллельного вывода наиболее требовательным к выбору эвристики является DCDP-параллельный вывод. Таким образом, нельзя исключить из выбранного множества связей те связи, резольвирование по которым на данном шаге может оказаться бесполезным или малоэффективным. Естественно, при выборе дизъюнкта в AND-параллельном резольвировании или предикатной литеры в OR-параллельном выводе, используются различные функции эвристической оценки, но данные оценки распространяются на все множество связей в целом, в то время как при DCDP-параллельном выводе происходит последовательный отбор связей, и на каждом шаге добавляется связь, удовлетворяющая условиям и имеющая наилучшее значение оценки. [44]
На каждом шаге необходимо принимать решение о том, какой из параллельных методов следует применять. Сначала проверяется возможность применения DCDP-параллельной резолюции. Для этого строится вспомогательный граф ( см. разд. Если их мощность равна 1, то следует рассмотреть возможность применения OR - и AND-параллельной резолюции. В случае, если при выборе дизъюнктов при резольвировании удаляется только одна связь, возникает необходимость сделать один шаг с использованием последовательного метода. [45]