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

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