close

Вход

Забыли?

вход по аккаунту

?

2. 19(1)

код для вставкиСкачать
2. Логика предикатов. Исчисление предикатов 2.1 Выполнить задание по алгебре предикатов и исчислению предикатов для выражения F=(∀x(A(x)→B(х)&∃y(B(x) →C(y)))→∃z(C(y)→ (D(z))
а. Привести выражение к виду ПНФ:
F=(∀x(A(x)→B(х)&∃y(B(x)→C(y)))→∃z(C(y)→(D(z)) = (∃x(A(x)&¬B(x))∀y(B(х)&¬C(y))∃z(¬C(y)D(z)) = ∃k∀n∃z(A(n)&¬B(n)B(x)&¬C(n)¬C(y)Dz = ∃k∀n∃z(A(k)&¬B(k)B(x))&(A(k)&¬B(k)C(n)¬C(y)D(z) = ∃k∀n∃z(A(k)B(x))&(B(x)¬B(k))&B(x)¬B(k))&¬C(n)(A(k)&¬C(n)v¬B(k))&C(y)D(z)=∃k∀n∃z(A(k)vB(x)¬C(y)D(z))&B(x)¬B(k)v¬C(y)D(z))&¬C(n)(A(k)¬C(y)D(z))&¬C(n)v¬B(k)&¬C(y)D(z)
F=∃k∀n∃z(A(k)vB(x)¬C(y)D(z))&B(x)¬B(k)v¬C(y)D(z))&¬C(n)(A(k)¬C(y)D(z))&¬C(n)v¬B(k)&¬C(y)D(z)
б. Привести выражение к виду ССФ:
Для приведения к виду ССФ воспользуемся алгоритмом Сколема, поэтому будет проведена следующая замена:
k = a, где a - предметная постоянная
z = f(n), где f(n) - переменная от функции
В результате получится следующее выражение:
F=∀n(A(a)vB(x)¬C(y)D(f(n)))&B(x)¬B(a)v¬C(y)D(f(n)))&¬C(n)(A(a)¬C(y)D(f(n)))&¬C(n)v¬B(a)&¬C(y)D(f(n)
в. Доказать истинность заключения методом дедуктивного вывода (с построением графа дедуктивного вывода):
Представим формулу в следующем виде:
{∀k∃y(¬A(k)B(k))&(¬B(x)C(y))) ∀z(C(y)&¬D(z)) Построим граф дедуктивного вывода для доказательства выводимости заключения из данного множества посылок:
∀x(A(x)→B(х)) ∃y(B(x)→C(y))
↓y∀x ↓y∃y
A(x)→B(х) B(x)→C(y)
A(x)→C(y)
y
¬A(x)C(y)
b
¬C(y)v¬C(y)v¬A(x)C(y)D(z)
¬C(y)D(z)
∃z(C(y)→(D(z))
Рисунок 7 - Граф дедуктивного вывода
г. Доказательство истинности заключения методом резолюции
Представим нашу формулу в следующем виде:
H = {∀k∃y(¬A(k)B(k))&(¬B(x)C(y))) ∀z(C(y)&¬D(z)) где L = ∀k∃y(¬A(k)B(k))&(¬B(x)C(y))) - посылка,
M = ∀z(C(y)&¬D(z)) - заключение.
Посылка L и отрицание заключения ¬M были приведены к виду ССФ.
L = ¬∀(k)B(k)¬B(x)C(y)
¬M = (C(y)&¬D(z))
K = {¬∀(k)B(k)¬B(x)C(y), C(y), ¬D(z)} - множество дизъюнктов.
Граф вывода пустой резольвенты для формулы H представлен на рисунке
¬∀(k)B(k)¬B(x)C(y)C(y)¬D(z)
Так как данное нам число дизъюнктов не сокращается, то мы можем сделать вывод, что принцип резолюции в данном примере не выполняется.
15
Документ
Категория
Без категории
Просмотров
10
Размер файла
34 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа