Исчисление предикатов первого порядка в качестве модели представления знаний

В учебном пособии рассматривается применение исчисления предикатов первого порядка в системах искусственного интеллнкта. Дано краткое введение в формальные системы. Описано исчисление предикатов первого порядка (алфавит, формулы, аксиомы, правила вывода) и приведены примеры доказательства ряда теорем, среди которых правило резолюции. Рассмотрен метод резолюции, используемый для автоматического доказательства теорем. Введено понятие интерпретации исчисления предикатов первого порядка, позволяющей использовать язык исчисления предикатов для представления и манипулирования знаниями.

1. Формальные системы

Тест: Доказательство теоремы для формальной системы

2. Исчисление предикатов

Тест: Правильно построенные формулы ИППП

Тест: Замкнутые формулы ИППП

3. Интерпретация ИППП

Тест: Представление утверждения в виде п.п.ф. ИППП

Тест: Представление утверждения в виде формулы ИППП

4. Полезные теоремы

5. Эквивалентность формул ИППП

6. Правило резолюции

7. Преобразование множества п.п.ф. во множество предложений

Тест: Преобразование п.п.ф. во множество предложений

8. Унификация

9. Опровержение на основе резолюции

Тест: Доказательство теоремы методом резолюции