ЛМвИИ (1086253), страница 10
Текст из файла (страница 10)
Если это не удается, то взять вкачестве допущения (дополнительной гипотезы) отрицание последнего консеквента ивывести противоречие.• Если главным знаком формулы является конъюнкция, то сначала доказываются вкачестве теорем члены конъюнкции. Например, доказать формулу А^В:1. А - теорема;2. В - теорема;3. А^В - из 1 и 2 по П1 (см. ниже).4. ├А^В по определению вывода на основе 1 — 3.Для приведенного выше примера будем иметь две гипотезы:c→d и ¬d.Заметим сразу, что правила (первого рода), приведенные в §1.5 правомерны и длялогики предикатов первого порядка, только надо иметь в виду, что литеры в этих правилахпредставляют предикатные формулы. Специфика же для логики предикатов первого порядкапривносит дополнительные правила, связанные с квантификацией переменных.
Не будем вы-.писывать эти формулы вновь, но будем иметь в виду, что при анализе предикатных формулссылка на правило с меткой Пi соответствует правилу Вi. Здесь же мы выпишем правила,специфические для логики предикатов первого порядка:П14. Отрицание квантора существования: ¬∃хА(х)├∀х¬А(х)П15. Удаление квантора общности: ∀xA(x)├A(t), где А(t) - результат правильнойподстановки терма t вместо x;П16. Введение квантора существования: A(t)├∃xA(x), где A(t) - результат правильнойподстановки терма t вмесго х;П17. Введение квантора общности: А(х)├∀yA(y), где А(y) - результат правильнойподстановки переменной y вместо x.П18. Удаление квантора существования: ∃уА(у)├А(x), где А(х) - результат правильнойподстановки переменной х вместо y в A(y);П19.
Правило дедукции: (Г, А├В) ├ (Г├А→В),П20. Доказательство от противного: (Г, ¬A├B^¬B)├(Г├A);П21. Сведение к абсурду: (Г, ¬А├В^¬В)├(Г├¬А).Правила П1- П18 являются правилами первого рода, правила П19 - П21 - правилавторого рода.Приведем пример использования правил для доказательства выводимости.
Для началазавершим приведенный пример. Итак, доказать (вывести) теорему(c→d)→(¬d→¬c).1. c→d - гипотеза;2. ¬d - гипотеза;3. ¬c - из 1 и 2 по П7.Получили множество формул {c→d, ¬d}, из которого последовал вывод ¬с, т.е.4. {c→d, ¬d}├¬с;5. (c→d├(¬d→¬c) из 4 по П19;6. ├(c→d)→(¬d→¬c) из 5 по П19.Следует сделать существенное замечание по поводу применения правил П13 - П18. Впрямом выводе необходимо отслеживать правильность подстановок переменных, связанных исвободных. Это в значительной степени усложняет доказательство выводимости и, главное,делает проблематичным использование для машинной реализации.
В то время как описанный вследующем параграфе способ преобразования формул к приведенной нормальной форме ианализ множества формул на выводимость с помощью метода резолюции лишен этогонедостатка, а убедительным примером реализуемости вывода на основе метода резолюцииявляется язык логического программирования Пролог.2.4. Получение дизъюнктов.Принцип резолюции работает со специфическим подмножеством языка первогопорядка, который будем называть языком дизъюнктов. В этом разделе дадим конструктивноеопределение дизъюнкта (т.е.
фактически опишем, как получать дизъюнкты).Формула вида Q1x1...Qn xn (M), где каждые Qi xi есть либо ∀xi , либо ∃хi , a M -формула,не содержащая кванторов, называется формулой в предваренной нормальной форме.При преобразовании формулы в предваренную нормальную форму можновоспользоваться следующими основными равносильностями:¬∀xP(x) ≡ ∃x¬P(x),(2.1)¬∃хР(х) ≡ ∀х¬Р(х),(2.2)¬∀x¬P(x) ≡ ∃xP(x),(2.3)¬∃х¬Р(х) ≡ ∀хР(х),(2.4)Пусть R - формула, не содержащая переменной х, тогда∀xR ≡ R,(2.5)∃xR ≡ R,(2.6)∀xP(x)vR ≡ ∀x(P(x)vR),(2.7)∀xP(x)^R ≡ ∀x(P(x)^R),(2.8)∃xP(x)vR ≡ ∃x(P(x)vR),(2.9)∃xP(x)^R ≡ ∃x(P(x)^R).(2.10)Законы (2.7), (2.9) и (2.8), (2.10) можно обобщить законами:(Qx)P(x)vR ≡ (Qx)(P(x)vR),(2.9а)(Qx)P(x)^R ≡ (Qx)(P(x)^R),(2.10a)∀xP(x)^∀xR(x) ≡ ∀x(P(x)^R(x)),(2.11)∃xP(x)v∃xR(x) ≡ ∃x(P(x)vR(x)),(2.12)∀xP(x) ≡ ∀yP(y),(2.1З)∃xP(x) ≡ ∃yP(y).(2.14)Формулы (13) и (14) имеют место при условии, что x и у принимают свои значения изодной и той же области.∀xP(x)v∀xR(x) ≢ ∀x(P(x)vR(x)),(2.15)∃xP(x)^∃хR(x) ≢ ∃x(P(x)^R(x)),(2.16)Поскольку каждая связанная переменная в формуле может рассматриваться как местодля подстановки, то следует в этих формулах одно из вхождений х переименовать, например, наz.
Пусть выбрана переменная z, которая не встречается в Р(x), тогда формулы (2.15) и (2.16)принимают вид:∀xP(x)v∀xR(x) ≡ ∀x∀z(P(x)vR(z)),(2.17)∃xP(x)^∃xR(x) ≡ ∃x∃z(P(x)^R(z)),(2.18)В общем случае имеем Q1x1...Qn xn(Q1x)P(x)v(Q2x)R(x) ≡ (Q1x)(Q2z)(P(x)vR(z)),(2.17a)(Q1x)P(x)^(Q2x)R(x) ≡ (Q1x)(Q2z)(P(x)^R(z)),(2.18a)∃x∀yP(x, y) ≢ ∃y∀xP(x, y),(2.19)∃x∀yP(x, y) ≢ ∀y∃xP(x, y).(2.20)Далее, та часть формул, которая не имеет кванторов, приводится к конъюнктивнойнормальной форме с использованием алгебраических преобразований для операций ¬, ^(&), v,→, ↔.Приведем алгоритм преобразования формул в предваренную нормальную форму.Шаг 1.
Исключаем логические связки → и ↔, используя законыP↔R ≡ (P→R)^(R→P),P→R ≡ ¬PvR.Шаг 2. Используем законы▪ двойного отрицания: ¬(¬P) ≡ P;▪ законы де Моргана:¬(PvR) ≡ ¬P^¬R,¬(P^R) ≡ ¬Pv¬R;▪ для внесения отрицания внутрь формулы используем:¬∀xP(x) ≡ ∃x¬P(x),¬∃хР(х) ≡ ^∀¬Р(х).Шаг 3. Переименование связанных переменных.Шаг 4. Используем законы (2.9а), (2.10а), (2.11), (2.12), (2.17a) и (2.18a).Шаг 5. Используем закон дистрибутивности, заменяя формулы вида(А^В)vC на (AvC)^(BvC);Av(B^C) на (AvB)^(AvC).И, наконец, чтобы избавиться от кванторов, используется процедура сколемизации,которая состоит в следующем: кванторы просматриваются слева направо до первого кванторасуществования ∃, при этом• если в кванторной приставке Q1x1...Qnxn квантор ∃xi не имеет левее себя кванторов ∀xj,то везде в формуле М переменная xi заменяется на некоторую неопределеннуюконстанту;• если в кванторной приставке квантор ∃xi стоит правее кванторов ∀xj1, …, ∀xjK (k<n), товезде в формуле M переменная хi заменяется на некоторую неопределеннуюфункцию fiC (xj1, …, xjK),• после исключения всех кванторов существования кванторы общности простоотбрасываются.
Считается, что все оставшиеся переменные связаны кванторамиобщности, поэтому их отбрасывание не влечет неоднозначностей в понимании формул.Элементарные дизъюнкции, полученные в результате выполнения описанных вышепроцедур, называются дизъюнктами.Примеры.1. Пусть задано множество X целых чисел x , y ∈ X и введем предикат Р(у, y),устанавливающий отношение "больше" между двумя числами.
Тогда на заданном множестведля ∀x существует y такое, что у>х, т.е. справедлива истинность предиката Р(y, х): ∀x∃yP(y, x).В соответствии с приведенным выше алгоритмом сколемизации имеем: P(fC(x), ). Тогдана основании веденного в примере определения предиката сколемовская функция в частностиможет иметь вид: fC(х)=х+1.2.
Получить дизъюнкты для формулы∃x(∃yP(x, y)v∃zQ(x, z)→∃vR(x,v)).Избавимся от импликации:∃x(¬(∃yP(x, y)v∃zQ(x, z))v∃vR(x, v)) = ∃x(¬∃yP(x, y)^¬∃zQ(x, z)v∃vR(x, v) =∃x(∀y¬P(x, y)^∀z¬Q(x, z)v∃vR(x, v))Вынесем кванторы в начало формулы:∃x∀y, z∃v(¬P(x, y)^¬Q(x, z)vR(x, v)).Отметим, что это один из множества допустимых вариантов вынесения кванторов.Здесь возможно получение кванторной приставки ∃x∀z, y∃v и даже ∃x, v∀y, zПолученную на предыдущем шаге формулу приводим к конъюнктивной нормальнойформе:∃x∀y, z∃v((¬P(x, y)vR(x, v)) ^ (¬Q(x, z)vR(x, v))).И, наконец, выполняем сколемизацию:(¬P(aC, y)vR(aC, fC(y, z)))^(¬Q(aC, z)vR(aC, fC(y, z))).
В результате получаем двадизъюнкта, которые обычно записываются через запятую:(¬P(aC, y)vR(aC, fC(y, z))) и (¬Q(aC, z)vR(aC, fC(y, z))).2. Получить дизъюнкты для формулы:∀x∃yP(x, y)^¬∃y∀zR(y, z) = ∀x∃yP(x, y)^∀y∃z¬R(y, z) =∀x∃yP(x, y)^∀v∃z¬R(v, z) = ∀x∃y∀v∃z(P(x, y)^¬R(v, z)) = P(x, f1C(x))^¬R(v, f2C(x, y)).В результате имеем два дизъюнктаP(x, f1C(x)) и R(v, f2C(x, y)).2.5. Теорема Эрбрана.Если формула в языке первого порядка невыполнима, т.е. не имеет интерпретации, тоневыполнимым является и множество дизъюнктов, полученное из этой формулы (т.е.
нетинтерпретации, которая удовлетворяла бы одновременно всем дизъюнктам множества).Справедливо также и обратное утверждение.Практически нереально рассматривать все возможные интерпретации на всехвозможных множествах. Тем не менее можно ограничить, не уменьшая общности рассуждений,как перечень рассматриваемых множеств, так и перечень возможных интерпретаций на этихмножествах.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
