Резольвирование
Cтраница 1
Резольвирование этой фразы с - д формирует новую фразу, которая содержит остальные литералы, причем для доказательства противоречия все они должны быть удалены в процессе резольвирования. [1]
Резольвирование дизъюнктов с функциями-ограничениями производится только при условии, что функция означена не полностью или означена полностью и имеет значение true. В первом случае резольви-рование производится по обычным правилам, так как в этом случае функция-ограничение воспринимается только препроцессором, а для остальных процедур видим только сам исходный дизъюнкт. Однако процедура применения подстановки выполняется как для исходного дизъюнкта, так и для функции-ограничения. [2]
Ограничение резольвирования по условию согласованности унификатора здесь не работает, так как все предикаты содержат разные переменные. [3]
Таким образом, процесс резольвирования для данной связи представляет собой получение резольвенты, добавление резольвенты в граф связей, добавление связей резольвенты в граф связей и удаление старых связей и дизъюнктов из графа связей. [4]
Так как нахождение всех возможных множеств DCDP-связей, резольвирование по этим связям и определение наиболее подходящего варианта резольвирования является вычислительно неэффективным, необходимо использование эвристик для определения потенциально лучших кандидатов на резольвирование. [5]
Принцип ( 3) отдает предпочтение связям, резольвирование которых позволяет получить чистые дизъюнкты, а при их удалении значительно упрощается структура графа связей. [6]
Как было указано выше, при выборе связи для резольвирования в графе связей можно использовать различные эвристические функции оценки. В случае параллельного резольвирования необходимо делать выбор множества связей, отвечающих некоторым условиям. Стоит отметить, что неудачный выбор связи может привести к экспоненциальному росту количества дизъюнктов при решении сложных задач, что сделает процедуру вывода практически непригодной. В то же время удачный выбор связи может значительно увеличить эффективность процедуры вывода. Например, резольвирование единственной связи предикатной литеры в дизъюнкте приведет к появлению так называемого чистого дизъюнкта, который должен быть удален. Удаление чистого дизъюнкта в свою очередь может привести к каскадному удалению других дизъюнктов и к эффекту снежного кома. В результате структура графа связей может значительно упроститься. [7]
В графах связей стратегия поиска заключается в проблеме выбора связи для резольвирования на каждом шаге резольвирования. Эта проблема аналогична проблеме выбора последовательности резольвирования предикатов во многих традиционных системах вывода. Большинство методов, использованных в этих системах, без значительных усложнений могут быть применены и к выводу на графе связей. [8]
С каждой связью в графе связей ассоциируется единственная резольвента, являющаяся результатом резольвирования предикатов, соединенных данной связью. После генерации резольвенты не составляет особого труда добавить ее в граф. Новые связи дизъюнкта-резольвенты могут быть вычислены с использованием имеющейся информации о наследуемых связях дизъюнктов-потомков. [9]
Процедура OR-параллельного вывода сводится к нахождению множества связей предикатной литеры дизъюнкта и последующему резольвированию с удалением дизъюнкта, содержащего предикатную литеру, по которой производилось резольвирование. В данной ситуации особое значение приобретает задача нахождения множества связей, резольвирование по которым приведет к максимальному упрощению графа связей. [10]
Принцип ( 2) также служит для упрощения результирующего графа связей, так как резольвирование дизъюнктов с малым числом связей после резольвирования приводит к получению дизъюнктов также с малым числом связей. [11]
В графах связей стратегия поиска заключается в проблеме выбора связи для резольвирования на каждом шаге резольвирования. Эта проблема аналогична проблеме выбора последовательности резольвирования предикатов во многих традиционных системах вывода. Большинство методов, использованных в этих системах, без значительных усложнений могут быть применены и к выводу на графе связей. [12]
Подобная попытка, путем введения эвристической функции выбора следующей связи, была реализована в алгоритме параллельного резольвирования. [14]
Так как нахождение всех возможных множеств DCDP-связей, резольвирование по этим связям и определение наиболее подходящего варианта резольвирования является вычислительно неэффективным, необходимо использование эвристик для определения потенциально лучших кандидатов на резольвирование. [15]
Страницы: 1 2 3 4