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

1. Самостоятельно выбрать предметную область для формулировки в ней утверждений и фактов.

2. Сформулировать словесно: – утверждения в избранной предметной области – не менее четырех; – факты; – заключение (вопрос) по базе утверждений и фактов. Формулировки утверждений и заключения должны предполагать введение квантификаций, желательно получить не менее трех логических связок в каждом утверждении и в заключении.

3. Выписать предикаты и указать их области определения в виде множеств. Наличие хотя бы одного двухместного предиката обязательно. Области определения задавать только для одноместных предикатов.

4. Формализовать в терминах логики предикатов первого порядка предметную область: утверждения, факты и заключение. Использовать логические связки: , , , Ø Ù Ú ® . Наличие логических связок отрицания и импликации обязательно, однако допускается наличие до двух формул без импликации (не считая факты).

5. Выполнить последовательно для каждой формулы: преобразование в ПНФ, сколемовскую и клаузальную формы, элиминацию кванторов всеобщности и элиминацию конъюнкций до получения множества дизъюнктов Г. Указать универсум Эрбрана H (Г).

6. Методом резолюций доказать или опровергнуть теорему о логическом следовании заключения из базы утверждений и фактов. При необходимости вводить унификаторы. Перед резольвированием указывать как сам унификатор, так и полученную в результате унифицирования формулу.

7. В случае доказанности получить конкретный ответ на вопрос заключения.