Cтраница 4
В данной ситуации особое значение приобретает способность алгоритма проводить направленный вывод, не генерировать излишних дизъюнктов, а также быстро определять кандидатов на резольвиро-вание и получать соответствующую резольвенту. Подобным требованиям удовлетворяют алгоритмы дедуктивного вывода на графах связей, так как пространство поиска на каждом шаге является легко обозримым ( в графе одновременно хранится информация обо всех кандидатах на резольвирование), дизъюнкты, которые не могут результативно участвовать в процессе вывода ( дизъюнкты с чистыми литерами - литерами без связей), удаляются из графа связей вместе со всеми связями, значительно упрощая его структуру. Быстрота вывода обеспечивается однократным вычислением и постоянным хранением унификатора для каждой связи. Также достоинством процедуры вывода на графе связей является возможность адаптации существующих алгоритмов для вывода на графе связей, что позволяет комбинировать достоинства существующих алгоритмов вывода и алгоритмов вывода на графах связей. Недостатками процедуры вывода на графе связей являются необходимость пересчета графа связей на каждом шаге резольвирования с вычислением новых связей и унификаторов и необходимость хранения всего графа связей в оперативной памяти. Параллельный вывод на графах связей позволяет частично решить проблему необходимости пересчета графа на каждом шаге резольвирования, так как одновременно резольвируются несколько связей. Недостатком процедур параллельного вывода является генерация некоторого количества бесполезных, лишних дизъюнктов, что вытекает из самого принципа организации параллельного вывода, когда резольвируются все связи одновременно. [46]
Доказано, что DCDP-параллельная резолюция корректна. Считаем, что исходное множество дизъюнктов не имеет чистых литер и тавтологий. Предварительно построим исходный граф связей. Если граф связей содержит пустой дизъюнкт, то он невыполним и, следовательно, алгоритм достиг конечного состояния. Алгоритм DCDP-параллельной резолюции отличается от алгоритма OR-параллельной резолюции 1 - м шагом, на котором, в случае DCDP-параллельной резолюции, происходит выбор множества DCDP-связей и проводится параллельное резольвирование по всем связям из выбранного множества. [47]
В данной ситуации особое значение приобретает способность алгоритма проводить направленный вывод, не генерировать излишних дизъюнктов, а также быстро определять кандидатов на резольвиро-вание и получать соответствующую резольвенту. Подобным требованиям удовлетворяют алгоритмы дедуктивного вывода на графах связей, так как пространство поиска на каждом шаге является легко обозримым ( в графе одновременно хранится информация обо всех кандидатах на резольвирование), дизъюнкты, которые не могут результативно участвовать в процессе вывода ( дизъюнкты с чистыми литерами - литерами без связей), удаляются из графа связей вместе со всеми связями, значительно упрощая его структуру. Быстрота вывода обеспечивается однократным вычислением и постоянным хранением унификатора для каждой связи. Также достоинством процедуры вывода на графе связей является возможность адаптации существующих алгоритмов для вывода на графе связей, что позволяет комбинировать достоинства существующих алгоритмов вывода и алгоритмов вывода на графах связей. Недостатками процедуры вывода на графе связей являются необходимость пересчета графа связей на каждом шаге резольвирования с вычислением новых связей и унификаторов и необходимость хранения всего графа связей в оперативной памяти. Параллельный вывод на графах связей позволяет частично решить проблему необходимости пересчета графа на каждом шаге резольвирования, так как одновременно резольвируются несколько связей. Недостатком процедур параллельного вывода является генерация некоторого количества бесполезных, лишних дизъюнктов, что вытекает из самого принципа организации параллельного вывода, когда резольвируются все связи одновременно. [48]
Доказана полнота и состоятельность процедуры вывода на графе связей. Вышеприведенный алгоритм является недетерминированным. Для реализации его на детерминированной машине он нуждается в детерминированной процедуре выбора резольвируемой связи. В данном вопросе возможно использование нескольких основных методик, например, выбор связи, активация которой приведет к уменьшению количества дизъюнктов в графе, количества связей или количества вхождений предикатов в дизъюнкты. Также к упрощению графа приводит слияние одинаковых предикатов из дизъюнктов-родителей. Еще одним фактором, влияющим на выбор связи, является единственность связи для предиката, что приводит, как сказано ранее, к удалению дизъюнкта, содержащего этот предикат после резольвирования. В случае, когда упрощения графа добиться не удается, следует выбрать связь, резольвирование которой приведет к минимальному усложнению графа связей. [49]
Доказана полнота и состоятельность процедуры вывода на графе связей. Вышеприведенный алгоритм является недетерминированным. Для реализации его на детерминированной машине он нуждается в детерминированной процедуре выбора резольвируемой связи. В данном вопросе возможно использование нескольких основных методик, например, выбор связи, активация которой приведет к уменьшению количества дизъюнктов в графе, количества связей или количества вхождений предикатов в дизъюнкты. Также к упрощению графа приводит слияние одинаковых предикатов из дизъюнктов-родителей. Еще одним фактором, влияющим на выбор связи, является единственность связи для предиката, что приводит, как сказано ранее, к удалению дизъюнкта, содержащего этот предикат после резольвирования. В случае, когда упрощения графа добиться не удается, следует выбрать связь, резольвирование которой приведет к минимальному усложнению графа связей. [50]
Математический препроцессор базируется на распознавании на этапе предварительной обработки некоторого множества встроенных или введенных функций. В качестве базисных используются элементарные арифметические функции: сложение ( ADD), вычитание ( SUB), деление ( DIV), умножение ( MUL), взятие по модулю ( ABS), а также суперпозиции элементарных арифметических функций: функции модуля суммы ( AADD), модуля разности ( ASUB), модуля частного ( ADIV), модуля произведения ( AMUL); операции сравнения на: равенство ( EQ), неравенство ( NEQ), меньше ( LT) и больше ( GR), а также логические функции NOT, AND и OR. Операндами в арифметических функциях могут быть числовые константы и переменные, принимающие числовые значения. Те из арифметических операций, которые дают числовой результат, могут также использоваться в качестве операндов. Операндами в логических функциях могут быть те константы и переменные, которые принимают логические значения. Операции сравнения дают логический результат и могут быть использованы в качестве операндов в логических функциях. Логические функции тоже могут быть использованы в них в качестве операндов. Логические функции могут также являться функциями-ограничениями на резольвирование для того или иного дизъюнкта. [51]