МАТЕМАТИЧЕСКАЯ ЛОГИКА

Лекция 9. Исчисление предикатов. Метод резолюций

9.1Исчисление предикатов (на «5» баллов)

9.2Метод резолюций для высказываний

9.3Метод резолюций для предикатов (на «5» баллов)

Основные определения

Исчисление предикатов – формальная система, позволяющая формировать новые высказывания путем указания исходных высказываний, имеющих значение «истина», а также аксиом и правил вывода, каждое из которых описывает, как формировать новое высказывание из исходных и уже построенных высказываний.

Аксиома – это высказывание, имеющее значение истины при любых значениях пропозициональных переменных, входящих в это высказывание.

Правилом вывода называют такое отношение между высказываниями, которое позволяет из множества посылок и аксиом делать выводы об истинности заключения.

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

Формальные символы, формулы, система аксиом и правила вывода составляют исчисление предикатов.

Аксиомы теории К исчисления предикатов

(14)хА(х) А(t) (закон универсальной конкретизации УК)

(15)А(t) хА(х) (закон экзистенционального обобщения ЭО) Аксиомы (14), (15) называют аксиомами Бернайса. В них A(x) – произвольная формула, содержащая свободную переменную x, и t – терм, свободный для x в A(x), т.е. при подстановке этого терма вместо переменной х не произойдет связывания свободных переменных терма t.