Лекция 9 Исчисление высказываний Проверка выводимости правильных


с. 1
Лекция 9

Исчисление высказываний Проверка выводимости правильных умозаключений. Алгоритм Квайна. Правило резолюций. Алгоритм Вонга.
I Формальные системы (ФС)

A – алфавит имён



З – алфавит специальных разделительных знаков

ППФ – правильно построенные формулы из имён и знаков

А ППФ – формулы, которые называются аксиомами

ПВ – правила вывода на множестве ППФ вида «если , то »

Исчисление , такое что I конструктивно порождается из множества аксиом применением ПВ.



Пример 1. Формальные грамматики. , где A – терминальный алфавит; V – вспомогательный алфавит; Р – правила вывода, вида , где (все слова из объединённого алфавита); S – начальный вспомогательный символ (начало порождения) суть аксиома.

Грамматика G порождает (исчисляет) язык , который является множеством слов, выделенных для целей синтаксического описания моделей некоторых объектов (например, языка программирования ALGOL).


II. Формальная модель высказываний (язык высказываний)

  1. A – алфавит имён =.

  2. Z – алфавит знаков ={, &, , V, , , другие знаки логических операций, – скобки }.

  3. ППФ суть скобочные формулы из A и Z, построенные по определённым правилам, например – есть ППФ, а формула не является ППФ. Буквами A, B, C и т.д. обозначаются сложные ППФ.

  4. Семантика ППФ.

    1. Каждое суть атомарное высказывание. Например, р – «студент спит», q – «слоны живут в Африке»

    2. Каждое ППФ образует сложное высказывание, где знаком придаётся смысл логических связок между высказываниями.

– смысл: если А то В (из А следует В).

– смысл: А и В.

– смысл: А или В, но не оба вместе (разделённое или).

– смысл: А или В.

– смысл: А тождественно (эквивалентно) В.

– смысл: не А, другое обозначение –

Пример: р – студент спит, q – время идёт, r – лекция скучная.

Студент спит, а время идёт ~.

Студент спит, если лекция скучная – .


  1. Интерпретация ППФ.

    1. Каждому атомарному высказыванию приписывается значение .

    2. Каждой ППФ приписывается значение в зависимости от интерпретации связок как знаков операций. Интерпретация связок соответствует таблицам истинности ФАЛ.

Например:

А В


АВ

л л

л и

и л

и и

и

и

л

и




  1. Если при некоторой интерпретации ППФ истинна, то она называется выполнимой на данной интерпретации.

  2. Если ППФ выполнима (истинна) на всех наборах, то она называется тождественно истинной, либо тавтологией, либо общезначимой.

  1. Другие интерпретации ППФ.

а) Многозначные логики. Например, каждое атомарное высказывание из ППФ и сама ППФ получают значение из множестватроичная логика.

б) Правдоподобная логика. Введена Д. Пойа в книге «Математика и правдоподобные рассуждения». ППФ принимают значения из множества и интерпретируется как мера правдоподобности высказывания. Д. Пойа ввёл правила для вычисления правдоподобности сложенных высказываний по правдоподобности его составляющих.


III. Специальный вид высказываний – рассуждения или

умозаключения.

Рассуждение состоит из двух высказываний «p» и «S». р – высказывание – посылка, S – высказывание – следствие, формальная запись рассуждения – читается «из р следует S», или «если Р то S».Иногда высказывание S ещё называют заключением.


Какими свойствами наделяются правильные рассуждения? Должны соблюдаться следующие отношения:

а) если Р = «истина», то и S должна быть = «истина».

б) если Р = «ложь», то из «лжи» может следовать всё, что угодно, т.е. заключение S может быть и ложным и истинным.

в) из истинной посылки не должно следовать ложное заключение.

Все эти отношения определяют правильные или истинные рассуждения, как это показано в следующей таблице.

P

S

P/S


PS

л

л

правильное

И


л

и

правильное

И

и

л

не правильное

Л

и

и

правильное

И


Можно ввести такую интерпретацию правильного рассуждения: Если правильное, то и.
Правильно построенное рассуждение является тавтологией. В правильном рассуждении не может быть, чтобы посылка была истинной, а заключение ложным. Эта строка в таблице истинности правильного рассуждения отсутствует. Если является тавтологией, то говорят, что рассуждение построено в соответствии с логикой и является логическим законом, который не зависит от интерпретации, а определяется только структурой (ППФ) посылок и следствий.

IV. Логические законы (Аристотель 384–322 д.н.э.).

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

Напомним, что все логические законы должны быть тавтологиями. Иногда законы называются правилами вывода, которые определяют правильный вывод из посылок.


  1. Modus ponens (правило отделения) ; смысл: если верно, что из А следует В и А является истинным, то истинно В.

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

А В

P

S


л л

л и


и л

и и


л

л

л



и

л

и

л



и



Проверка тавтологии при помощи эквивалентных преобразований.






(А В) & А


Пример: Если лекция скучная, то студент спит. Лекция скучная.



Значит: студент спит.




В

  1. Modus tollens (отрицательный марус)

Формальная запись ;
Пример:

  1. Правило силлогизма ;

Формула высказывания

  1. Закон контрпозиции

  2. Все соотношения (тождества) алгебры логики суть тавтологии и поэтому являются логическими законами.

  3. Закон исключения третьего .

  4. Закон дистрибутивности и .

  5. Закон «гибельная дилемма»

Может быть доказана следующая теорема.

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

Например, – есть тавтология, т.к. обозначив

.

Для представления F в форме введём





.

V. Исчисление высказываний.


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

Формальная система, порождающая высказывания, которые являются тавтологиями и только их, называются исчислением высказываний (ИВ). Выше было показано, что любая формула высказываний (в том числе и тавтология) может быть приведена к структуре рассуждения (умозаключения), «если Р, то S».



Общезначимые



высказывания (тавтологии)

Формулы в ИВ считаются выводимыми из аксиом. В каждом выводе из тавтологий выводятся тавтологии. Обозначение: ; интерпретация: из выводимо .

Формальная система ИВ определяется:

Формулы – аксиомы являются тавтологиями. Правила вывода в виде также являются тавтологиями.

На сегодняшнее время известно 20 ИВ, которые отличаются друг от друга аксиомами (схемами аксиом) и правилами выводов. Все ИВ обладают 1) свойством полноты – (в них выводимы все тавтологии и только они) 2) набор аксиом обладает минимальной полнотой ( т.е. удаление хотя бы одной аксиомы из набора делает ИВ неполной).

Два примера:



  1. ИВ Уйтхеда и Рассела (19201930, Англия).

Аксиомы

А1. (А А) А – закон тавтологии

А2. А  (В А) – закон добавления

А3. (А В)(В А) – закон перестановки

А4. (А В)((С А)  (С В)) – закон суммирования

Правила вывода Р1: Подстановка А вместо В; Р2: Замена на эквивалентную формулу Р3: Modus ponens ⊦ В.



  1. ИВ Никоды (1952, США)

Единственная аксиома с операцией штрих Шеффера:

;

единственное ПВ: С.


VI. Методы и алгоритмы проверки выводимости.

Пусть задана совокупность ППФ , которая называется посылками (иногда гипотезами), и ППФ – . «» называется логическим следствием . или выводимой из А (записывается как ), если является тавтологией (тождественно истинным высказыванием).

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


  1. Алгоритм истинностных таблиц (АИТ) для F=AB.

АИТ сводится к последовательной подстановке всех возможных интерпретаций (наборов «истина» и «ложь») переменных, входящих в . Алгоритм останавливается, если значение ложь ( не выполнима, а значит не выводима из на всех интерпретациях); истина ( выполнима на всех интерпретациях, значит суть тавтология и А⊦. Такой алгоритм требует в наихудшем случае 2n подстановок (2n возможных интерпретаций), где «n» число переменных, входящих в формулу F.


  1. Алгоритм Квайна (Квайн. 1960 г. США)

Идея: при последовательных подстановках значений переменных можно уменьшить длину формулы, исходя из совокупности проведённых проверок истинности F, и тем самым сокращать число переменных для проверки.

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

Пример: Пусть необходимо проверить общезначимость формулы



Семантическое дерево. Каждое левое ребро дерева соответствует переменным, а каждое правое ребро – .

Каждая ветвь (например, самая левая) соответствует набору (pqr), самая правая. Дерево перечисляет все возможные элементарные конъюнкции.



  1. Положим для F (вершина ) , тогда

(напомним, что

(формула в вершине «1»)



  1. Положим для , тогда

.

(формула в вершине «2»)






  1. Спустимся до вершины . Положим для , тогда значение (формула в вершине «3»).

  2. Поднимемся к вершине , в положим , тогда (формула в вершине «4»).

Поднимемся к вершине и в положим , следуя нумерации вершин, находим, что . . Можно заметить характерное правило обхода вершин.

Такой алгоритм обхода вершин семантического дерева называется алгоритмом с возвратом (back tracking). На рисунке показан путь обхода семантического дерева. В процессе обхода вычисляется значение формулы F. Оказывается, что на всех наборах значений . Таким образом F является тавтологией.


3. Метод резолюций (Д.Робинсон, 1965 г., США).

Алгоритмы доказательства выводимости АB, построенные на основе этого метода, применяются во многих системах искусственного интеллекта, а также являются фундаментом, на котором построен язык логического программирования «Пролог».


Метод резолюций использует несколько принципов.

  1. Сведение к противоречию.

Пусть правильно построенное рассуждение с элементарными высказываниями .

Тогда, отсюда и .



  1. Представление формул для и в виде КНФ

, где Д и Д – дизъюнкты.

  1. Правило резолюций R для обработки совмещенного списка дизъюнктов.

Объединенный Д1 = С1 хi

список Д2 = С2 хi

дизъюнктов Д, ………….С1 Сj

входящих ….………

в P и Дj = Сj хi

…………. Оставшийся

Дm+n список

дизъюнктов

а) Каждый дизъюнкт из Д представим в виде , где «С» все остальные переменные, входящие в дизъюнкт, xi выделенная переменная с отрицанием, либо без отрицания . Из списка выделяется пара, как показано на рисунке, с общей переменной xi с отрицанием и без него.

б) По правилу резолюции (закону резолюции), который является тавтологией (доказательство этого факта можно сделать)



пара дизъюнктов редуцировалась в дизъюнкт .

в) Образуется новый список дизъюнктов из дизъюнктов. (оставшийся список дизъюнктов). Такой список называется редуцированным. Очевидно, что размерность редуцированного списка по сравнению с исходным уменьшилась на «1».

г) далее правило R применяют к редуцированному списку дизъюнктов.

д) Останов наступает, когда в списке остаются только два дизъюнкта вида и , либо применение R невозможно.

Список дизъюнктов редуцировался в КНФ

В этом случае говорят, что S логически следует из Р или S выводимо из Р.

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

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


  1. Алгоритм проверки выводимости правильного построенного умозаключения Вонга (Wong, 1960, США)

(1960 г. Гарвард).
Выводимость P из S означает, что из множества посылок

множество следствий.

Это соответствует логической формуле или более детально



, где .

Правильно построенному рассуждению (умозаключению) должна соответствовать тавтология .

Каждая и суть ППФ, построенная из связок &, , , .

называется строкой Вонга.

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

Пусть дана строка Вонга

левая часть правая часть

строки строки


  1. Замена импликации в строке на ДНФ:

В Рi и Sj, там, где встречается знак «».

…⊦… строка с «»

…⊦… строка ДНФ

  1. Избавление от знака отрицания « » переносом из одной части строки в другую.

а) , добавление к правой части.

редуцированная строка Вонга.

б) Р добавление к левой части



Р,А редуцированная строка Вонга.

Перенос любой переменной в левую (правую) часть строки всегда вызывает её «отрицание».

Пример: Избавление от знака отрицания.

а) Строка Вонга [(, B) ⊦ (C)] редуцируется в строку

[(B) ⊦ (А, C)] ⊦ (С) – строка Вонга интерпретируется как логическая формула . Редуцированная строка Вонга [] и соответствующая формула .

Правило редуцирования строки Вона является тождественно истинным преобразованием. Доказательство тождественности двух выражений.



Таким образом, если из выводима С, то из В выводима

б) редуцируется в С] и соответственно


  1. Расщепление на строки (левой и правой части строки Вонга).

а) S ; расщепление левой части
S; S

б) ; расщепление правой части



;

Выводимость (тавтология, тождественная истинность каждой строки должна быть доказана).

Пример: а) ; расщепление – и ; ;


  1. Замена логических связок на «,» (правило перечисления).

Строка Вонга


редуцируется в строку





  1. Критерий доказательства вывода.

В результате освобождения строки Вонга от логических связок имеем

, т.е. строка Вонга имеет вид:

.

Если в левом списке и правом списке найдутся одинаковые переменные, то из P выводимо S (P .S).

На самом деле, по правилу 2) переноса переменной и «навешивания» на её знака отрицания.

Строка и , преобразованная по правилу 2) будет иметь вид

и далее при замене «,» на логическую связку «» в , где получаем, что и поэтому . Преобразовав строку РS в соответствующую импликацию PS и подставив S1, получим . Таким образом доказана выводимость S из Р.

Примеры:

а) Постулируется выводимость (закон «modus ponens»).

Строка Вонга .

по правилу 1) преобразуется

по правилу 5) содержит в левой и правой части одинаковые переменные. Выводимость доказана.

б) Постулируется выводимость (закон «контрпозиции»).

по правилу 1) .

по правилу 3) расщепление левой части строки и .

по правилу 2) А и В

по правилу 5) Строки А и В в левых и правых частях содержат одинаковые переменные. Выводимость из доказана.








с. 1

скачать файл

Смотрите также: