Принцип - резолюция
Cтраница 4
 |
Последовательность действий эксперта-системного аналитика при описании множества экспертных утверждений. [46] |
Аксиоматическая составляющая модели ЛАМ соответствует понятию экспертная модель принятия решений в данном плане проблемных ситуаций. Иными словами, экспертные модели являются множествами информации о способах и приемах поиска управляющих решений в некотором классе ситуаций и описываются языком логики предикатов первого порядка. Выбор такого языка описания не случаен, а определен наличием общей процедуры поиска решений, именуемой принципом резолюций. [47]
Принцип резолюции или вариации этого принципа используются во многих системах по автоматическому доказательству теорем или для нахождения доказательства или проведения вывода. Отметим только, что хотя принцип резолюции очень простой, его практическое применение во многом зависит от того, каким образом уменьшить пространство перебора, когда мы пытаемся провести сравнение. Мы также отметим, что принцип резолюции тесно связан с графическим сравнением. Фактически мы можем представить предложение ( или дизъюнкты) с помощью ( модифицированной) семантической сети и провести логические выводы путем применения принципа резолюции к семантической сети. [48]
Недостаток процедуры вывода Эрбрана состоит в экспоненциальном росте множества фундаментальных примеров Si при увеличении г. Мультипликативный метод, использованный Гилмором при машинной реализации этой процедуры, также неэффективен. Как легко видеть, даже для малого множества из десяти двухлитерных фундаментальных примеров дизъюнктов существует 210 конъюнкций в ДНФ. Робинсон, который ввел принцип резолюции, являющийся теоретической базой для построения большинства методов автоматического доказательства теорем. [49]
В ряде случаев для определения тождеств удобен так называемый алгоритм редукции. Алгоритм основан на доказательстве путем приведения к абсурду. Метод особенно хорош, когда формула содержит много импликаций. Согласно принципу дедукции, вопрос о выводимости ( не выводимости) некоторой формулы сводится, в конечном счете, к анализу невыполнимости множества ее дизъюнктов. Множество дизъюнктов невыполнимо тогда и только тогда, когда логическим следствием из него является пустой дизъюнкт. Метод, позволяющий получить логические следствия из множества дизъюнктов, основан на применении принципа резолюций. [50]
Страницы: 1 2 3 4