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

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

Правило вывода:

Это правило называется правилом резолюции, при этом С ₁ и С ₂ называются резольвируемыми (родительскими) предложениями, а - резольвентой. p и` p - контрарными литералами.

Заметим, что многие правила вывода являются частными случаями правила резолюции:

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