Cтраница 2
Если использовать классическое ограничение по условию согласованности унификатора, то в данной задаче было бы проведено 114 резольвирований и 114 бектрекингов, прежде чем был бы получен ответ. [16]
Принцип ( 2) также служит для упрощения результирующего графа связей, так как резольвирование дизъюнктов с малым числом связей после резольвирования приводит к получению дизъюнктов также с малым числом связей. [17]
Процедура OR-параллельного вывода сводится к нахождению множества связей предикатной литеры дизъюнкта и последующему резольвированию с удалением дизъюнкта, содержащего предикатную литеру, по которой производилось резольвирование. В данной ситуации особое значение приобретает задача нахождения множества связей, резольвирование по которым приведет к максимальному упрощению графа связей. [18]
В значительной мере гибкость и мощь процедуры вывода является следствием ее недетерминизма, так как на каждом шаге алгоритма может быть выбрана любая связь для резольвирования. [19]
Резольвирование этой фразы с - д формирует новую фразу, которая содержит остальные литералы, причем для доказательства противоречия все они должны быть удалены в процессе резольвирования. [20]
Так как нахождение всех возможных множеств DCDP-связей, резольвирование по этим связям и определение наиболее подходящего варианта резольвирования является вычислительно неэффективным, необходимо использование эвристик для определения потенциально лучших кандидатов на резольвирование. [21]
Задача Стимроллер характеризуется экспоненциальным ростом пространства поиска, поэтому для эффективной работы при решении данной задачи процедура вывода должна, во-первых, по возможности сокращать множество дизъюнктов и, во-вторых, выбирать наилучшие, или близкие к наилучшим, связи для резольвирования. [22]
Принцип ( 1) служит для упрощения результирующего графа связей, так как дизъюнкты с малым числом литер, как правило, имеют меньшее число связей. Также резольвирование по дизъюнктам, имеющим малое количество литер, позволяет получить одно-двулитеральные дизъюнкты, которые могут быть эффективно использованы в дальнейшем процессе вывода. [23]
Как было указано выше, при выборе связи для резольвирования в графе связей можно использовать различные эвристические функции оценки. В случае параллельного резольвирования необходимо делать выбор множества связей, отвечающих некоторым условиям. Стоит отметить, что неудачный выбор связи может привести к экспоненциальному росту количества дизъюнктов при решении сложных задач, что сделает процедуру вывода практически непригодной. В то же время удачный выбор связи может значительно увеличить эффективность процедуры вывода. Например, резольвирование единственной связи предикатной литеры в дизъюнкте приведет к появлению так называемого чистого дизъюнкта, который должен быть удален. Удаление чистого дизъюнкта в свою очередь может привести к каскадному удалению других дизъюнктов и к эффекту снежного кома. В результате структура графа связей может значительно упроститься. [24]
На некоторых шагах резольвирования, как было указано выше, процедуры вывода действовали весьма разумно. [25]
В графах связей стратегия поиска заключается в проблеме выбора связи для резольвирования на каждом шаге резольвирования. Эта проблема аналогична проблеме выбора последовательности резольвирования предикатов во многих традиционных системах вывода. Большинство методов, использованных в этих системах, без значительных усложнений могут быть применены и к выводу на графе связей. [26]
Такие характеристики, как число промежуточных дизъюнктов и число унификаций, являются более общими, но и к их использованию стоит относиться внимательно. Например, некоторые из использованных методов позволяют получать резольвенту путем одновременного резольвирования по нескольким дизъюнктам, поэтому такая характеристика, как число промежуточных дизъюнктов меняет свой смысл. В случае использования алгоритмов параллельного вывода может быть более полезным использование характеристики количество шагов вывода, так как на каждом шаге резольвирования мы можем получить больше чем один дизъюнкт. [27]
Алгоритм дедуктивного вывода на раскрашенных С-графах является наиболее эффективным для решения задачи Стимроллер, что определяется ее представлением в виде графа дизъюнктов, который имеет множество независимых вершин. При работе алгоритма происходит стяжка сети, на каждом шаге резольвирование идет по нескольким вершинам, что повышает эффективность алгоритма вывода. [28]
Процедура OR-параллельного вывода сводится к нахождению множества связей предикатной литеры дизъюнкта и последующему резольвированию с удалением дизъюнкта, содержащего предикатную литеру, по которой производилось резольвирование. В данной ситуации особое значение приобретает задача нахождения множества связей, резольвирование по которым приведет к максимальному упрощению графа связей. [29]
Тогда резолюция, у которой хотя бы один из двух дизъюнктов при резольвировании является входным, называется входной резолюцией. Входная резолюция проста, эффективна, но в общем случае, к сожалению, как было видно из примера 1.24, неполна. Однако она полна для множества так называемых хорновских дизъюнктов. [30]