Правила резолюции для исчисления предикатов

Для применения правила резолюции нужны контрарные литералы в резольвируемых предложениях. Пусть С ₁ и С ₂ - два предложения в исчислении предикатов. Правило вывода называется правилом резолюции в исчислении предикатов, если в предложениях С ₁ и С ₂ существуют унифицируемые контрарные литералы p ₁ и p ₂, т.е. такие, что , причем атомарные формулы p ₁ и p ₂ являются унифицируемыми наиболее общим унификатором . В этом случае резольвентой предложений С ₁ и С ₂ является предложение , полученное из предложения применение унификатора .

Понятие унификатора. Если в формулу А вместо переменных х ₁,…., х _n подставить соответствующие формулы В ₁,…, В _n, то получится формула В, которая называется частным случаем формулы А; т.е. . При этом формула подставляется вместо всех вхождений переменной . Набор подстановок называется унификатором.

Формула С называется совместным частным случаем формул А и В, если С является частным случаем формулы А и одновременно частным случаем формулы В при одном и том же наборе подстановок, т.е. когда:

.

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