ДЗ 1: Метод резолюций в логике предикатов первого порядка

Представлено 11 вариантов решения домашнего задания по МЛиТА. Это позволит Вам ознакомиться с разными выбранными предметными областями, посмотреть разные процессы формализации утверждений. Посмотреть примеры использования правил сколемизации, а также метода резолюций. На их основании Вы можете сделать собственное творческое домашнее задание.
Копировать имеющиеся здесь предметные области смысла нет, так как происходит проверка на антиплагиат.

ОБЩАЯ ФОРМУЛИРОВКА ЗАДАНИЯ
1. Самостоятельно выбрать предметную область для формулировки в ней утверждений и фактов.
2. Сформулировать словесно:
- утверждения в избранной предметной области;
- не менее четырех;
- факты;
- заключение (вопрос) по базе утверждений и фактов.
Формулировки утверждений и заключения должны предполагать введение квантификаций, желательно получить не менее трех логических связок в каждом утверждении и в заключении.
3. Выписать предикаты и указать их области определения в виде множеств. Наличие хотя бы одного двухместного предиката обязательно. Области определения задавать только для одноместных предикатов.
4. Формализовать в терминах логики предикатов первого порядка предметную область: утверждения, факты и заключение. Использовать логические связки: ¬, ∨, ∧, →. Наличие логических связок отрицания и импликации обязательно, однако допускается наличие до двух формул без импликации (не считая факты).
5. Выполнить последовательно для каждой формулы: преобразование в ПНФ, сколемовскую и клаузальную формы, элиминацию кванторов всеобщности и элиминацию конъюнкций до получения множества дизъюнктов Г. Указать универсум Эрбрана Н(Г).
6. Методом резолюций доказать или опровергнуть теорему о логическом следовании заключения из базы утверждений и фактов. При необходимости вводить унификаторы. Перед резольвированием указывать как сам унификатор, так и полученную в результате унифицирования формулу.
7. В случае доказанности получить конкретный ответ на вопрос заключения.Показать/скрыть дополнительное описание