Читайте также:
|
Логическое программирование - программирование, основанное на механизме доказательства теорем в логике. Теоремы описывают предметную область, а программа состоит из набора аксиом, описывающих предметную область и теоремы, которую необходимо доказать. Доказательство осуществляется методом резолюции.
Метод резолюции формируется следующим образом: если выводимые атомарные формулы (p || q) и (!p || R) то выводимы следующие формулы (Q || R), где p - заголовок атомарной формулы, Q и R - остальная часть формулы, возможно включающая комбинацию из других формул. (Q || R) - дизьюнктор (резолюция).
Процедура логического вывода, основанного на резолюция заключается в следующем: 1) к фразам, описывающих предметную область, добавляется отрицание теоремы. 2) выполняется поиск аксиомы, с которой может быть выполнена резолюция в простом линейном порядке. 3) При нахождении такой аксиомы, к применяется резолюция, и она добавляется во множество аксиом, описывающих предметную область. Эта процедура повторяется до тех пор, пока не будет получен пустой дизьюнкт.
Пустым дизьюнктом называется дизьюнкт следующего вида (p &&!p)
В процессе доказательства выполняются унификации атомарных формул, при этом возможна конкретизация переменных. Унификация проходит успешно, если совпадают предикатные имена, состовляющих формул и арности.
Дата добавления: 2015-07-19; просмотров: 73 | Нарушение авторских прав
| <== предыдущая страница | | | следующая страница ==> |
| Переменная, конкретизация переменных | | | Определение оператора и его свойства. |