Доказательство логических высказываний с помощью метода резолюций

Этот метод является полу конструктивным методом доказательства истинности логических клауз, в которых исполняются так называемый признак резолюций. Он соответствует аксиоме отношения порядка и вместе с тем образует эффективную конструктивную структуру. Его суть сводится к тому, что 2 посылочных дизъюнкции с противоположными тербами всегда можно склеить в один дизъюнкт, в котором противоположных тербов не будет: , где х, у – произвольные тербы или дизъюнкты, А и - противоположные тербы.

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

-не обязательно использовать все посылки, число которых может быть избыточным, а главное - получить 0.

ПРИМЕР:

Док-во. начнем с приведения ее в нормальное коньюктивное противоречие:

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

Получили 0 – истинность доказана.