Cтраница 3
Предположим, что 5 - множество обычных дизъюнктов и дизъюнкт С выводим из 5 обычной резолюцией. Тогда существует дизъюнкт С, выводимый из S ограниченной т-ре-золюцией и такой, что Set ( С) С. Напомним, что граница больше или равна единице. [31]
Ранее мы установили, что множество дизъюнктов S невыполнимо тогда и только тогда, когда оно принимает значение ложь при всех интерпретациях на любых областях. Однако в силу невозможности рассмотрения подобных интерпретаций хорошо было бы найти такую специальную область интерпретации, установив на которой факт невыполнимости множества дизъюнктов, можно было бы сделать вывод о невыполнимости этого множества на любых других областях интерпретаций. Такая область, к счастью, имеется, и она называется универсумом Эрбрана. [32]
Теорема 3.1. Пусть S - невыполнимое множество дизъюнктов, представленное С-графом. [33]
Минимальная модель теории ( или множество общих дизъюнктов) Т - это модель М теории Т, обладающая следующим свойством: не существует меньшей модели N теории Т, совпадающей с М на высказываниях-умолчаниях. [34]
Необходимость математического препроцессора для обработки множества дизъюнктов становится очевидной, если рассмотреть задачи, классическим примером которых может служить задача о восьми ферзях. Более того, любая задача, требующая выполнения некоторых математических действий для проверки истинности условий, не может быть оптимально решена без такого препроцессора, а в некоторых случаях решение вообще невозможно. [35]
Допустим, У - интерпретация множества дизъюнктов над некоторым множеством функциональных и предикатных символов, a D - область интерпретации У. [36]
В процессе работы программы к множеству перечисленных дизъюнктов не было добавлено ни одного нового. [37]
В отличие от этого, каждое множество дизъюнктов, содержащее пустой дизъюнкт, не может быть подтверждено никаким истинностным означиванием, так как П неподтверждаем. [38]
Теорема 8.1. Пусть S - некоторо множество дизъюнктов, а / ( - множество аксиом равенства для S. [39]
Так как i / j - множество основных дизъюнктов и каждый L - получен из В - использованием единичной резолюции и единичной парамодуляции, то ясно, что мы можем получить из S единичное опровержение. Это завершает наше доказательство. [40]
Узел N в псевдосемантическом дереве для множества S дизъюнктов называется опровергающим узлом, если имеется основной частный случай С некоторого дизъюнкта из S такой, что I ( N) [) C противоречиво, но ни для какого предшественника N узла N нет основного частного случая С дизъюнкта из S такого, что I ( N) [) C противоречиво. [41]
Следующий пример показывает, что существует множество дизъюнктов LDL, которое вообще не имеет модели. [42]
Таким образом, для установления невыполнимости множества дизъюнктов необходимо образовать множества Si, 82, , Sn фундаментальных примеров дизъюнктов и последовательно проверять их на ложность. Теорема Эрбрана гарантирует, что если множество дизъюнктов S невыполнимо, то данная процедура обнаружит такое п, что Sn является ложным. [43]
Когда предложение у представлено в виде множества дизъюнктов, нам приходится работать с переменными и сколемовскими функциями. [44]
Докажите при помощи метода резолюций, что множество дизъюнктов в этом примере невыполнимо. [45]