Матлог. Отчет матлогика (1). Метод резолюций в логике предикатов первого порядка
 Скачать 13.8 Kb.
|
|
Отчет по домашнему заданию по дисциплине "Математическая логика и теория алгоритмов" Тема: "Метод резолюций в логике предикатов первого порядка" 1. Предметная область: Обсуждение в чате музыкальных предпочтений. 2. Утверждения Если x не лучше z, то x не лучше y или y не лучше z. Если x лучше y, то x хорош; никакой x не лучше самого себя. Существует такой x, что x не хорош, и существуют такие y и z, что y не лучше z. Если не существует такого y, что x лучше y, то x не хорош. Факт: a лучше b; факт: c лучше d; факт: d лучше a; факт: b не хорош. Вопрос: существуют ли такие y и z, что c лучше y, y лучше z, z не хорош? 3. Предикаты B(x) — x хорош (область определения: музыканты или музыкальные треки) M(x, y) — x лучше y. 4. Формульное представление ∀x∀y(¬M(x, z)→(¬M(x, y)∨¬M(y, z))) ∀x∀y(M(x, y)→B(x))∧¬∃xM(x, x) ∃x(¬B(x))∧∃y∃z¬M(y, z) ∀x((¬∃yM(x, y))→¬B(x)) Факты: M(a, b), M(c, d), M(d, a), ¬B(b). Заключение: ∃y∃z(M(c, y)∧M(y, z)∧¬B(z)) 5. Преобразование каждой формулы в ПНФ ∀x∀y(¬M(x, z)→(¬M(x, y)∨¬M(y, z))) — уже ПНФ ∀x∀y(M(x, y)→B(x))∧¬∃xM(x, x))преобразуется в ∀x∀y(M(x, y)→B(x))∧∀x¬M(x, x) и далее в ∀x∀y∀z((M(x, y)→B(x))∧¬M(z, z)) ∃x(¬B(x))∧∃y∃z¬M(y, z) преобразуется в ∃x∃y∃z(¬B(x))∧¬M(y, z) ∀x((¬∃yM(x, y))→¬B(x)) преобразуется в ∀x(∃yM(x, y)∨¬B(x)) и далее в ∀x∃y(M(x, y)∨¬B(x)) Заключение — уже ПНФ Сколемизация ∀x∀y(¬M(x, z)→(¬M(x, y)∨¬M(y, z))) ∀x∀y∀z((M(x, y)→B(x))∧¬M(z, z)) (¬B(d))∧¬M(e, g) M(x, f(x))∨¬B(x) Заключение: M(c, h)∧M(h, i)∧¬B(i) Клаузальная форма ∀x∀y(M(x, z)∨¬M(x, y)∨¬M(y, z)) ∀x∀y∀z((¬M(x, y)∨B(x))∧¬M(z, z)) (¬B(d))∧¬M(e, g) M(x, f(x))∨¬B(x) Заключение: M(c, h)∧M(h, i)∧¬B(i) Элиминация кванторов всеобщности M(x, z)∨¬M(x, y)∨¬M(y, z) (¬M(x, y)∨B(x))∧¬M(z, z) (¬B(d))∧¬M(e, g) M(x, f(x))∨¬B(x) Заключение: M(c, h)∧M(h, i)∧¬B(i) Элиминация конъюнкций M(x, z)∨¬M(x, y)∨¬M(y, z) ¬M(x, y)∨B(x) ¬M(z, z) ¬B(d) ¬M(e, g) M(x, f(x))∨¬B(x) Факты: M(a, b), M(c, d), M(d, a), ¬B(b) Заключение: M(c, h), M(h, i), ¬B(i) Универсум Эрбрана: {a, b, c, d, e, g, h, i, f(a), f(b), ..., f(i), f(f(a), ...)} 6. Применяем метод резолюций Подстановка в первую формулу: M(c, a)∨¬M(c, d)∨¬M(d, a) Резолюция: M(c, d), M(c, a)∨¬M(c, d)∨¬M(d, a) M(c, a)∨¬M(d, a) M(c, a)∨¬M(d, a), M(d, a) M(c, a) Получаем: M(c, a), M(a, b), ¬B(b), что соответствует заключению. 7. Заключение верно. |