Cтраница 4
Используя метод резолюций, докажите, что множество дизъюнктов в упражнении 14 к главе 4 невыполнимо. [46]
Его подход основан на том, что множество дизъюнктов S невыполнимо тогда и только тогда, когда оно принимает значение Л во всех интерпретациях на любых областях. Однако в силу невозможности рассмотрения всех интерпретаций, необходимо найти такую специальную область интерпретации, установив на которой факт невыполнимости множества дизъюнктов, можно было бы сделать вывод о невыполнимости его на других областях. Такая область получила название универсума Эрбрана. [47]
Если С-дизъюнкт, принадлежащий некоторому Е - про-тиворечивому множеству дизъюнктов, включающему х х и аксиомы рефлексивности для функций, причем множество S - С является Е - противоречивым, то S имеет линейное опровержение по правилам Э1 и У с верхним дизъюнктом С. [48]
Как будет видно впоследствии, нахождение доказательства для множества дизъюнктов эквивалентно построению семантического дерева. [49]
С помощью эрбрановских интерпретаций мы сводим проблему невыполнимости множества дизъюнктов к проблеме невыполнимости множества основных примеров этих дизъюнктов на эрбрановском универсуме. Так как в основные примеры дизъюнктов не входят переменные, выполнимость может быть доказана с помощью методов логики высказываний, таких как метод семантических таблиц и метод резолюций. [50]