Мегаобучалка Главная | О нас | Обратная связь  


Метод резолюций в логике высказываний




Поможем в ✍️ написании учебной работы
Поможем с курсовой, контрольной, дипломной, рефератом, отчетом по практике, научно-исследовательской и любой другой работой

 

Рассмотрим вначале логику высказываний. Напомним, что литералом мы называли атомарную формулу или ее отрицание, дизъюнктом – дизъюнкцию литералов. Дизъюнкт может состоять из одного литерала. На дизъюнкт мы иногда будем смотреть, как на множество литералов, т.е. не будем различать дизъюнкты, которые получаются один из другого с помощью коммутативности и ассоциативности дизъюнкции, а также идемпотентности. Последнее означает, например, что дизъюнкты XÚØYÚX и XÚØY равны. Нам понадобится особый дизъюнкт – пустой, т.е. дизъюнкт, не содержащий литералов. Его мы будем обозначать "квадратиком" □. Будем считать, что пустой дизъюнкт ложен при любой интерпретации. Это означает, что формула F&□ равносильна □, а формула FÚ□ равносильна F. Пустой дизъюнкт есть фактически то же самое, что и атомарная формула 0, но в контексте метода резолюций принято использовать □.

 

Определение. Литералы L и ØL называются противоположными.

 

Метод резолюций в логике высказываний основан на правиле резолюций.

 

Определение. Правилом резолюций в логике высказываний называется следующее правило: из дизъюнктов ХÚF и ØXÚG выводим дизъюнкт FÚG.



Например, из дизъюнктов ØXÚYÚZ и XÚØY выводим дизъюнкт YÚZÚØY. Обратим внимание на то, что в первых двух дизъюнктах есть еще одна пара противоположных литералов. Условимся, что можно применять правило резолюций не обязательно к самым левым литералам (поскольку мы не различаем дизъюнкты, отличающиеся порядком записи литералов). Тогда правило резолюций, примененное к Y и ØY, даст ØXÚZÚX. Условимся еще о следующем: в дизъюнктах не писать повторяющиеся литералы и не писать □, если есть другие литералы.

 

Определение. Пусть S – множество дизъюнктов. Выводом из S называется последовательность дизъюнктов

 

D,D2,...,Dn

 

такая, что каждый дизъюнкт этой последовательности принадлежит S или следует из предыдущих по правилу резолюций. Дизъюнкт D выводим из S, если существует вывод из S, последним дизъюнктом которого является D.

Например, если S={ØXÚYÚZ, ØYÚU, X}, то последовательность

D1=ØXÚYÚZ,

D2=ØYÚU,

D3=ØXÚZÚU,

D4=X,

D5=ZÚU –

вывод из S. Дизъюнкт ZÚU выводим из S.

 

Применение метода резолюций основано на следующем утверждении, которое называется теоремой о полноте метода резолюций.

 

Теорема. Множество дизъюнктов логики высказываний S невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт.

 

Доказательство. Докажем вначале достаточность.

Отметим, что правило резолюции сохраняет истинность.

Это означает, что если j(ØXÚF)=1 и j(XÚG)=1 для некоторой интерпретации j, то j(FÚG)=1. Действительно, пусть j(ØXÚF)=1 и j(XÚG)=1. Тогда если j(F)=1, то и j(FÚG)=1. Если же j(F)=0, то j(ØX)=1, поскольку j(ØXÚF)=1. Но в этом случае j(X)=0 и j(G)=1, так как j(XÚG)=1. Если же j(G)=1, то и j(FÚG)=1.

Пусть из S выводим пустой дизъюнкт. Предположим противное: множество S выполнимо, т.е. существует интерпретация y, при которой все дизъюнкты из S истинны. Выводимость пустого дизъюнкта из S означает, что существует последовательность дизъюнктов D1,…,Dn=□, каждый дизъюнкт которой принадлежит S или получается из предыдущих по правилу резолюции. Если дизъюнкт Dj из этой последовательности принадлежит S, то по предположению y(Dj)=1. Если же он получается из предыдущих по правилу резолюций, то также y(Dj)=1, поскольку правило резолюций сохраняет истинность. При i=n получаем, что y(□)=1. Противоречие показывает, что предположение о выполнимости множества S – ложное предположение. Следовательно, S невыполнимо. Достаточность доказана.

Докажем необходимость. Доказательство проведем индукцией по следующему параметру: d(S)=сумма числа вхождений литералов в дизъюнкты из S минус число дизъюнктов.

Пусть множество дизъюнктов S невыполнимо. Если пустой дизъюнкт принадлежит S, то он выводим из S (вывод в этом случае состоит из одного пустого дизъюнкта) и необходимость теоремы доказана. Будем считать в силу этого, что □ÏS. При этом предположении каждый дизъюнкт содержит хотя бы один литерал и поэтому d³0.

База индукции: d(S)=0. Если d(S)=0, то все дизъюнкты состоят из одного литерала. Поскольку множество S невыполнимо, то в нем должна найтись пара противоположных литералов X и ØX. В таком случае пустой дизъюнкт выводим из S, соответствующий вывод содержит три дизъюнкта: X, ØX, □.

Шаг индукции: d(S)>0. Предположим, что для любого множества дизъюнктов Т такого, что d(Т)<d(S) необходимость теоремы доказана. Пусть

 

S={D1,D2,…,Dk-1,Dk}.

 

Так как d(S)>1, то в S существует хотя бы один неодноэлементный дизъюнкт. Будем считать, что это дизъюнкт Dk, т.е. Dk=LÚDk′, где L – литерал и Dk′¹□. Наряду с множеством дизъюнктов S рассмотрим еще два множества дизъюнктов

 

S1={D1,D2,…,Dk-1,L},

S2={D1,D2,…,Dk-1,Dk/}.

 

Ясно, что S1 и S2 невыполнимы и что d(S1)< d(S) и d(S2)<d(S). По предположению индукции из S1 и S2 выводим пустой дизъюнкт. Пусть

 

A1,A2,…,Ai,…,Al-1,Al=□ (1)

 

вывод пустого дизъюнкта из S1 и

 

B1,B2,…,Bj,…Bm-1,Bm=□ (2)

 

вывод пустого дизъюнкта из S2.

Если в первом выводе не содержится дизъюнкта L, то эта последовательность дизъюнктов будет выводом из S и необходимость теоремы доказана. Будем считать, что L содержится в первом выводе, пусть Ai=L. Аналогично предполагаем, что Bj=Dk′.

Если дизъюнкт Е получается из дизъюнктов Е1 и Е2 по правилу резолюций, то будем говорить, что Е непосредственно зависит от Е1 (и от Е2). Транзитивное замыкание отношения непосредственной зависимости назовем отношением зависимости (Другими словами, E зависит от Е/, если существуют дизъюнкты Е1,…,Еn такие, что E=E1,…,En=E/ и Е1 непосредственно зависит от Е2,…,En-1 непосредственно зависит от En).

Преобразуем второй вывод следующим образом: к дизъюнкту Bj и всем дизъюнктам, которые от него зависят, добавим литерал L. Новая последовательность дизъюнктов

 

 

B1,B2,…,Bj/=Dk/ÚL, B/j+1 ,…,Bm/ (3)

 

будет выводом из S. Если дизъюнкт Bm не зависит от Bj, то Bm/ =□. Это означает, что из S выводим пустой дизъюнкт и необходимость теоремы доказана. Предположим, что Bm зависит от Bj. Тогда Bm/=L. Преобразуем теперь первый вывод: на место дизъюнкта Ai (равного L) в этой последовательности подставили последовательность (3). Получим последовательность

 

A1,…,Ai-1,B1,…,Bj/,B/j+1,…,Bm/=L,Ai+1,…,Al=□.

 

Эта последовательность является выводом пустого дизъюнкта из множества дизъюнктов S. Следовательно, если множество S невыполнимо, то из S выводим пустой дизъюнкт.

Теорема доказана.

 

Для доказательства того, что формула G является логическим следствием множества формул F1,…,Fk метод резолюций применяется следующим образом. Сначала составляется множество формул T={F1,…,Fk,ØG}. Затем каждая из этих формул приводится к конъюнктивной нормальной форме и в полученных формулах зачеркиваются знаки конъюнкции. Получается множество дизъюнктов S. И, наконец, ищется вывод пустого дизъюнкта из S. Если пустой дизъюнкт выводим из S, то формула G является логическим следствием формул F1,…,Fk. Если из S нельзя вывести □, то G не является логическим следствием формул F1,…,Fk.

 

Проиллюстрируем сказанное на примере. Покажем, что формула G=Z является логическим следствием формул F1=ØXÚY®X&Z, F2=ØY®Z. Сформируем множество формул T={F1,F2,ØG}. Приведем формулы F1 и F2 к КНФ (формула ØG сама имеет эту форму). Мы получим, что

 

F1 равносильна X&(ØYÚZ),

F2 равносильна (YÚZ).

 

 

Тогда множество дизъюнктов S равно

 

{X, ØYÚZ, YÚZ, ØZ}.

 

Из множества S легко выводится пустой дизъюнкт:

 

ØYvZ, ØZ, ØY, YÚZ, У, □.

 

Следовательно, формула G является логическим следствием формул F1, и F2.

 

 




Читайте также:
Как распознать напряжение: Говоря о мышечном напряжении, мы в первую очередь имеем в виду мускулы, прикрепленные к костям ...
Как построить свою речь (словесное оформление): При подготовке публичного выступления перед оратором возникает вопрос, как лучше словесно оформить свою...



©2015-2020 megaobuchalka.ru Все материалы представленные на сайте исключительно с целью ознакомления читателями и не преследуют коммерческих целей или нарушение авторских прав. (1669)

Почему 1285321 студент выбрали МегаОбучалку...

Система поиска информации

Мобильная версия сайта

Удобная навигация

Нет шокирующей рекламы



(0.02 сек.)
Поможем в написании
> Курсовые, контрольные, дипломные и другие работы со скидкой до 25%
3 569 лучших специалисов, готовы оказать помощь 24/7