Главная | Обратная связь | Поможем написать вашу работу!

Семантические таблицы

Методы доказательств – это алгоритмические процедуры, следуя которым, можно установить, является ли формула тавтологией, и выполнимо ли множество формул.

В 1934 немецкий математик Генцен(1909-1945) доказал существование алгоритмических процедур, позволяющих установить тавтологичность формул, применяя сформулированные им правила вывода. Эти правила стали основой исчисления высказываний.

Используя теорию доказательства, Бет и Хинтикка в 1955 г. предложили алгоритм, устанавливающий, является ли составное высказывание тавтологией или нет, получивший название метода семантических таблиц Бета.

При помощи семантических таблиц Бета можно исследовать значение истинности данного высказывания. Семантическая таблица составного высказывания К строится индуктивно, исходя из семантических таблиц подформул, входящих в высказывание К.

Идея метода основывается на построении дерева, вершинами которого являются все подформулы данной формулы, для проверки логического значения всех подформул вплоть до атомов, называемых листьями, при всевозможных интерпретациях. Такое дерево воспроизводит таблицу истинности формулы. Однако часто нет необходимости строить все дерево до листьев: в некотором узле значение функции может быть определено сразу для всех листьев, которые могут быть построены из этого узла.

Пусть К–формула языка логики высказываний. Обозначим tK утверждение «К - истинно» и fK - утверждение: «К-ложно». При этом tK и fK называются помеченными формулами.

Семантическая таблица – это дерево, вершинами которого являются помеченная формула и ее помеченные подформулы.

Атомарные семантические таблицы – это семантические таблицы для элементарных булевых функций {&, Ú, ®, «, Ø, …}. Примеры атомарных семантических таблиц для произвольных формул s₁и s₂ представлены на Рис. 1.

Рисунок 1. Элементарные семантические таблицы

Семантическая таблица составного высказывания К – это граф, не имеющий циклов (дерево), с единственным корнем, в который помещается помеченная формула К. Каждая ветвь дерева интерпретируется как конъюнкция всех подформул, записанных в вершинах этой ветви. Семантическая таблица строится сверху вниз, исходя из индуктивного правила определения формулы: неделимые высказывания (литералы) – это атомы; из атомов строятся формулы с использованием логических связок. Каждая формула является результатом применения одно- или двуместной логической связки к образующим ее подформулам. Для этих связок выше определены атомарные семантические таблицы.

Процедура построения семантической таблицы состоит в следующем:

· Построение семантической таблицы для составного высказывания начинаем с того, что записываем помеченную формулу tK или fK в корень семантической таблицы.

· Если какая-то часть таблицы уже построена, находим в множестве висячих вершин (т.е. вершин графа, которым инцидентно единственное ребро) особые вершины и продолжаем построение атомарными семантическими таблицами для каждой из подформул. Вершина семантической таблицы называется особой, если она встречается как корень некоторой атомарной семантической таблицы. Если вершина обозначена помеченным атомом, она называется обычной.

· Ветвь семантической таблицы называется противоречивой, если в ней встречаются обычные вершины, содержащие помеченные формулы t P и f P для некоторого атома Р.

· Семантическая таблица называется замкнутой, если ни одна из ее ветвей не содержит особых вершин, которые не были бы продолжены в соответствии с атомарными семантическими таблицами ее подформул. В противном случае семантическая таблица называется незамкнутой.

· Семантическая таблица противоречива, если каждая ее ветвь противоречива. Если замкнутая семантическая таблица с корнем f K противоречива, а это означает, что мы пытались всеми возможными способами сделать высказывание К ложным и не сумели, то К – тавтология.

· Доказательством или выводом по Бету высказывания К называется замкнутая противоречивая семантическая таблица, в корне которой помещена помеченная формула f K.

· Замкнутая противоречивая таблица, имеющая в качестве корня t K, называется опровержением по Бету высказывания К.

· Говорят, что высказывание К доказуемо или выводимо по Бету, если оно имеет доказательство по Бету. Высказывание называется опровержимым по Бету, если существует опровержение К по Бету. Факт, что К доказуемо по Бету обозначается ├_В К.

В данном случае понятие выводимости отличается от аналогичного определения в теории булевых функций и означает общезначимость рассуждения. Чтобы избежать путаницы понятий, будем применять для обозначения тождественной истинности высказываний термин доказуемо.

Примеры

1. Доказать, что формула является противоречием.

Доказательством в этом случае будет опровержение по Бету, т.е. замкнутая семантическая таблица, в корень которой помещена формула, помеченная как истинная. Построение семантической таблицы приведено на рис. 2. Полученная замкнутая семантическая таблица (ЗСТ) оказалась противоречивой. Это означает, что мы пытались всеми возможными способами доказать истинность формулы и не сумели этого сделать. Следовательно, рассмотренная формула есть противоречие. В этом случае говорят, что формула не выводима по Бету.

Рисунок 2. Опровержение по Бету

2. Пусть K=(AÅB)&((A®B)&(B®A)). Доказать, что эта формула тождественно ложна.

В этом случае опровержением по Бету является замкнутая противоречивая семантическая таблица, в корень которой помещена формула, помеченная как истинная, Рис. 3.

3. Предположим, что истинны высказывания:

1. Джордж любит Марию, или Джордж любит Екатерину;

2. Если Джордж любит Марию, то он любит Екатерину.

Кого же Джордж любит?

Обозначим символом М высказывание «Джордж любит Марию» и символом К высказывание «Джордж любит Екатерину». Тогда высказывание (1) эквивалентно МÚК, а высказывание (2) эквивалентно М®К. Обозначим A=(MÚK)&(M®K). По условию примера предполагается, что А истинно. Мы хотим узнать, любит ли Джордж Екатерину, т.е., верно ли tK. Докажем от противного, т.е. предположим, что он ее не любит, т.е. верно fK. Построим семантическую таблицу с корнем fK, рис. 4.

Для примера 3 и сделанного предположения семантическая таблица оказалась противоречивой. Т.е. Джордж любит Екатерину.

Если бы мы построили семантическую таблицу с помеченной формулой fM в корне, рис. 4, то непротиворечивую таблицу мы бы не получили и, следовательно, не смогли бы определить, любит Джордж Марию или нет!

Метод резолюций

Метод резолюций-наиболее эффективный способ алгоритмического доказательства, как в логике высказываний, так и в логике предикатов. Именно этот метод построения доказательств составляет основу языка логического программирования ПРОЛОГ. Доказательство в методе резолюций, как и в методе семантических таблиц Бета, строится путем опровержения. Но он более удобен для написания логических программ в языке программирования, который устроен почти так же, как язык логики высказываний. Предложенный в 1965 году Дж. Робинсоном метод резолюций позволяет выявить противоречивость множества формул с помощью систематической процедуры последовательного построения логических следствий из двух формул этого множества, приводящей к появлению противоречия в виде пустой резольвенты, если рассматриваемое множество формул невыполнимо.

В теории булевых функций доказывается, что произвольная булева функция, не равная тождественно единице, может быть представлена в совершенной конъюнктивной нормальной форме (СКНФ), которая является конъюнкцией всех конституент нуля данной функции. Определена также процедура приведения СКНФ к минимальной конъюнктивной нормальной форме (МКНФ). Конъюнктивная нормальная форма (КНФ) может быть также построена путем применения равносильных преобразований к формуле, являющейся суперпозицией над произвольным множеством логических связок.

Введем некоторые дополнительные понятия.

2. Литерал – это произвольный атом или его отрицание.

3. Дизъюнкт -это дизъюнкция конечного множества литералов. Конъюнктивная нормальная форма является конъюнкцией конечного множества дизъюнктов различных рангов и может быть представлена в теоретико-множественном виде как множество, элементами которого являются множества литералов каждого из дизъюнктов КНФ. Это множество литералов также называется дизъюнктом. Дизъюнкт, который не содержит ни одного литерала, называется пустым и является всегда неподтверждаемым. Пустой дизъюнкт обозначается значком . Пустой дизъюнкт по определению ложен и означает противоречие: он вносит противоречие в наш мир, делая его неподтверждаемым.

Для обозначения произвольных секвенций вида Ф├R используется также имя клауза. Любую подформулу клаузы можно представить дизъюнктом, который, в свою очередь, называется предложением. Если в множестве формул S все формулы являются дизъюнктами, его можно представить в теоретико-множественной форме

Множество дизъюнктов соответствует представленному в КНФ высказыванию

Пусть D1 и D2 дизъюнкты, L – атом. Резольвентой двух дизъюнктов (D1ÚL) и (D2ÚØL) называется дизъюнкт (D1ÚD2). (КНФÚ().

Правило резолюции (или резолюция) гласит, что из истинности двух дизъюнкций, одна из которых содержит литерал, а другая — его отрицание, следует (выводима) формула, являющаяся дизъюнкцией исходных формул без упомянутого литерала и его отрицания.

Рассмотрим следующие дизъюнкты:

C₁={A₁,…, A_k, ØB₁,…, ØB_l},

C₂={D₁,…,D_k, ØF₁,…,ØF_l},

где A₁,…, A_k, B₁,…, B_l, D₁,…, D_k, F₁,…, F_l - атомы. Предположим, что А₁ совпадает с F₁. Тогда можно переписать эти дизъюнкты следующим образом:

C₁={A₁} È где - ={A₂,…, A_k, ØB₁,…, ØB_l},

C₂= {ØA₁}È , где ={D₁,…, D_k, ØF₂,…,ØF_l }.

Тогда резольвентой С₁ и С₂ является дизъюнкт .

Можно считать, что исходные дизъюнкты С₁ и С₂ «вступают в противоречие», так как содержат один и тот же литерал, входящий в эти дизъюнкты с отрицанием и без отрицания. Устранение противоречия приводит к получению нового дизъюнкта, который и «разрешает конфликт». Своим названием метод обязан этому разрешению (to resolve – разрешать). Определим формально метод резолюций.

Пусть С₁ и С₂ – дизъюнкты, L – такой литерал, что LÎC₁ и ØLÎC₂. Тогда резольвентой дизъюнктов С₁ и С₂ называется дизъюнкт

D=(C₁\{L}) È (C₂\{ØL}). Говорят, что дизъюнкты С₁ и С₂ резольвируют.

Резольвентой двух дизъюнктов C₁={P, Q} и C₂={ØP, ØФ} является дизъюнкт D={Q, ØФ}.

Если имеется множество, содержащее более двух дизъюнктов, то можно ввести понятие множества резольвент.

Пусть S={C₁, …, C_n}. Множество R(S)=SÈ{D | D резольвента дизъюнктов C_i, C_j, 1 £ i, j £ m, m³n} называется резольвентой множества дизъюнктов S. Резольвировать могут не только исходные дизъюнкты, но и полученные резольвенты.

Применение такого правила становится интуитивно понятным, если записать дизъюнкты в классической формулировке логики высказываний:

Пусть исходные высказывания: (ØAÚB), (AÚC); заключение(BÚC). Метод резолюции основан на использовании тавтологии

что проверяется непосредственным преобразованием или таблицей истинности.

Действительно, выполним преобразования:

Следовательно, полученное заключение справедливо. Т.е. дизъюнкт (BÚC) выводим из данных посылок: (ØАÚВ), (АÚС) ├ (ВÚС).

Пусть S={C₁, C₂, …, C_k} - множество дизъюнктов. Резолютивный вывод из S есть такая последовательность C₁, C₂, …, C_m дизъюнктов, что "i: C_i ÎS или является резольвентой пары дизъюнктов, предшествующих C_i. Вывод пустого дизъюнкта называется опровержением S.

Основная теорема логического вывода утверждает, что если формула R выводима из множества формул F₁, F₂,…,F_k, то формула Ф= ложна. Если при этом формулы F₁, F₂,…,F_k, R представлены в виде дизъюнктов, то, присоединяя к ним все возможные резольвенты этих дизъюнктов, в случае невыполнимости формулы Ф получим пустую резольвенту, что означает противоречивость множества Ф.

Доказательство методом резолюции является аналогом доказательства от противного. В утверждении о следовании из множества посылок некоторого заключения производят замену этого заключения его отрицанием. Затем каждую посылку и отрицание заключения представляют в виде множества дизъюнктов и применяют к полученному множеству дизъюнктов метод резолюции.

Пусть S – множество дизъюнктов:

Применяя к этому множеству дизъюнктов резолюцию столько раз, сколько возможно, получим резольвенту S:

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

Примеры

1. Используя метод резолюций, покажем, что множество формул

противоречиво.

Рассмотрим резолютивный вывод:

1. AÚBÚC;

2. AÚBÚ ;

6. -резольвента 1 и 2;

7. А - резольвента 3 и 6.

8. -резольвента 4 и 5;

9. -резольвента 7 и 8.

Следовательно, множество S противоречиво.

2. Используя метод резолюций, покажем, что истинна секвенция

Для доказательства достаточно показать, что соответствующее этой секвенции множество дизъюнктов противоречиво. Если секвенция истинна, то ее отрицание ложно. Представим соответствующую отрицанию секвенции формулу в КНФ, выполнив преобразования.

Соответствующее теоретико-множественное представление формулы имеет вид: Применим к этому множеству дизъюнктов метод резолюций:

5. -резольвента 1 и 4;

6. -резольвента 3 и 5;

7. -резольвента 3 и 2;

8. -резольвента 7 и 6.

Доказано, что отрицание секвенции ложно. Следовательно, исходная секвенция истинна.

Процедуру поиска всех возможных резольвент можно организовать по-разному, и разные стратегии в среднем будут включать различное число шагов до получения результата. Одной из наиболее эффективных является стратегия движения «от цели». Под «целью» понимают заключение высказывания. При этом на первом шаге для получения резольвенты выбирают целевой дизъюнкт и в множестве фактов – такой дизъюнкт, который содержит отрицание цели. Далее поступают аналогичным образом с полученной резольвентой до тех пор, пока не будет получен пустой дизъюнкт. Метод резолюций гарантирует получение его, если исходное множество дизъюнктов противоречиво. Эта стратегия особенно эффективна в языках логического программирования, где только небольшое число фактов общей базы данных действительно имеет отношение к заданному вопросу.

⇐ Предыдущая 1 234 5 6 7 8 9 10 Следующая ⇒