Логическое программирование на языке Visual Prolog. Солдатова О.П - 16 стр.

UptoLike

ВУЗ: 

СГАУ | Самара

Составители: 

Рубрика: 

16
Пример 14. Доказать, что формула R(a, z) выводима из множества
дизъюнктов S={
¬
P(x, f(x))
∨
R(x, f(x), g(x)), Q(x, g(x))
∨
R(x, f(x), g(x)),
¬
Q(x,
g(x))
∧
P(x, f(x))}.
Пусть C
1
=
¬
P(x, f(x))
∨
R(x, f(x), C
2
= Q(x, g(x))
∨
R(x, f(x), C
3
=
¬
Q(x, g(x))
∨
P(x, f(x)). Добавим к множеству S единичный дизъюнкт C
4
=
¬
R(a, z).
Так как в дизъюнктах C
1
, C
2
, C
3
есть одинаковая переменная x, то
заменим её в C
2
на y, а в C
3
на u. Таким образом, решение исходной задачи
сводится к доказательству противоречивости следующего множества
дизъюнктов:
C
1
=
¬
P(x, f(x))
∨
R(x, f(x);
C
2
= Q(y, g(y))
∨
R(y, f(y);
C
3
=
¬
Q(u, g(u))
∨
P(u, f(u));
C
4
=
¬
R(a, z).
Найдём резольвенту C
5
дизъюнктов C
1
и C
3
и добавим её к множеству
дизъюнктов, для чего произведём унификацию переменных x и u, таким
образом, что u заменим на x, и получим C
5
= R(x, f(x))
∨
¬
Q(x, g(x)).
Найдём резольвенту C
6
дизъюнктов C
2
и C
5
и добавим её к множеству
дизъюнктов, для чего произведём унификацию переменных y и x, таким
образом, что y заменим на x, и получим C
6
= R(x, f(x))
∨
R(x, f(x))= R(x, f(x)).
Найдём резольвенту C
7
дизъюнктов C
2
и C
6
и добавим её к множеству
дизъюнктов, для чего произведём замену переменной x на константу a, а
переменную z заменим на функцию f(a), таким образом получим C
7
= , то
есть пустой дизъюнкт.
Алгоритм метода резолюций.
Шаг 1. Если в S есть пустой дизъюнкт, то множество невыполнимо,
иначе перейти к шагу 2.
Шаг 2. Найти в исходном множестве S такие дизъюнкты или склейки
дизъюнктов C
1
и C
2
, которые содержат унифицируемые литералы L
1
∈
C
1
и
L
2
∈
C
2
. Если таких дизъюнктов нет, то исходное множество выполнимо,
иначе перейти к шагу 3.
Шаг 3. Вычислить резольвенту C
1
и C
2
и добавить ее в множество S.
Перейти к шагу 1.
2 Введение в язык логического программирования ПРОЛОГ.
2.1 Общие положения
Язык Пролог объединяет два подхода: логический и процедурный.
По мнению Дж. Робинсона, в основе идеи логического
программирования лежит принцип описания задачи при помощи
совокупности утверждений на некотором формальном логическом языке и
получение решения
при помощи вывода в некоторой формальной системе.
Основой языка Пролог является логика предикатов первого порядка.

Страницы