Главная » SQL, Базы данных » ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ

0

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

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

■     Распределительные законы.

f AND ( g OR h ) ≡  ( f AND g ) OR ( f AND h ) f OR ( g AND h ) ≡  ( f OR g ) AND ( f OR h )

■    Законы де Моргана.

NOT ( f AND g ) ≡  ( NOT f ) OR ( NOT g )

NOT ( f OR g ) ≡  ( NOT f ) AND ( NOT g )

Здесь f, g и h — произвольные логические выражения.

Теперь обратимся к логике как таковой. Логику можно рассматривать как формальный метод проведения рассуждений. Поскольку метод проведения рассуждений формализован, он может использоваться для решения формальных задач, таких как проверка допустимости фактического параметра путем исследования лишь структуры этого фактического параметра в виде стандартной последовательности шагов (например, в которой не уделяется никакого внимания смыслу самих этих шагов). В частности, поскольку это — формальный метод, он может быть автоматизирован (иными словами, запрограммирован) и поэтому его выполнение можно возложить на некоторый механизм.

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

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

Термы

Начнем этот раздел с предположения, что имеется некоторая коллекция объектов, называемых константами, применительно к которым мы можем высказывать утверждения различного рода. В терминах баз данных эти константы представляют собой значения из соответствующих доменов, а утверждениями могут быть, например, логические выражения, такие как "3 > 2". Определим  терм как утверждение, которое включает такие константы2 и соответствует приведенным ниже требованиям:

а)  либо не включает никаких логических операторов (см. следующий подраздел), ли бо заключено в круглые скобки;

б)  в результате вычисления недвусмысленно принимает значение либо TRUE, либо

FALSE.

Например,   все   следующие   утверждения   являются   термами:   "Поставщик    S1 находится в Лондоне", "Поставщик S2 находится в Лондоне" и "Поставщик S1 поставляет деталь Р1" (при обычно используемых нами значениях данных они принимают значения, соответственно, TRUE, FALSE и TRUE). В отличие от этого, следующие утверждения не являются термами, поскольку они не  принимают недвусмысленно значение TRUE или FALSE: "Поставщик S1 поставляет деталь р" (где р — переменная) и "Поставщик S5 будет поставлять деталь Р1 когда-то в будущем".

Формулы

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

<formula>

::=   <term>

| NOT  <term>

I <terra> AND  <formula>

I <fcerm>  OR  <formula>

| <term>

<formula>

<term>

::=    <atomic  formula>

| (  <formula>  )

Формулы вычисляются в соответствии с истинностными значениями составляющих их термов, с применением обычных таблиц истинности для логических операторов (AND, OR и т.д.). Из этого следуют приведенные ниже выводы.

2 Точнее, содержит имена таких констант или, иными словами, литералы. В основной части литературы различие между этими понятиями практически не учитывается.

1.  Показанная в определении структуры формулы <formula> атомарная формула

<atomic formula> — это логическое выражение, которое не содержит логиче ских операторов и не заключено в круглые скобки.

2.  Символ " ⇒ " представляет собой логический оператор, известный под названием

логической импликации. Выражение f   ⇒   g определено как логически эквива

лентное выражению (NOT f)   OR g.

Примечание. Для обозначения этого оператора в главе 8 и в других предыдущих главах использовалась конструкция" IF. ..   THEN…  END IF".

3.  В целях сокращения количества круглых скобок, необходимых для регламентации желаемого порядка вычисления, применяются обычные правила приоритета для

логических операторов (NOT, затем AND, затем OR, затем ⇒ ).

4.  Высказывание представляет собой просто формулу <formula>, составленную в соответствии с приведенным выше определением (термин формула используется для того, чтобы в этом и следующем разделах применялась единообразная терми нология).

Правила вывода

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

╞ f   ⇒ g

Здесь f и g — формулы, а символ ╞ может рассматриваться  как  обозначающий "всегда справедливо то, что"; обратите внимание на то, что некоторый подобный символ требуется для того, чтобы мы могли формировать метаутверждения (т.е. утверждения об утверждениях). Ниже приведены некоторые примеры правил логического вывода.

1.    ╞ ( f  AND  g   )    ⇒   f

2.    ╞ f  ⇒   (   f   OR  g   )

3.    ╞ ( (   f    ⇒  g   )   AND   ( g  ⇒ h )                                        )  ⇒   (   f  ⇒   )

4.    ╞ ( f   AND   (   f    ⇒  g   )    )     ⇒  g

Примечание. Последнее правило является особенно важным. Оно называется  правилом modus ponens (или правилом отделения). Неформально это правило гласит, что если высказывание f является истинным и из f следует д, то д также должно быть истинным. Например, допустим, что приведенные ниже формулыа) и б) обе являются истинными.

а)  У меня нет денег.

б)  Если у меня денег, то я должен зарабатывать на жизнь мытьем посуды. Из этого можно сделать вывод, что истинной является также формула в).. в)  Я должен зарабатывать на жизнь мытьем посуды.

Продолжим описание правил логического вывода.

5.    ╞  (   f  ⇒   (   g ⇒ h   )    )    ⇒   (    (f  AND g   )    ⇒ h   )

6.    ╞  (    (   f   OR  g   )   AND   (   NOT  g   OR  h   )    )   ⇒   (   f   OR  h   )

Примечание. Последнее из этих правил также относится к числу особенно  важных. Оно называется правилом резолюции. Дополнительная информация о нем  приведена в следующем подразделе, "Доказательства", а также в разделе 24.4.

Доказательства

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

. . ., fn (предпосылок3), что можно представить в символическом виде, как  показано ниже.

fl,   f2,    . . . ,   fn g

Это символическое обозначение можно прочитать так: "Формула g может быть получена путем дедуктивного логического вывода (или, проще говоря,  может быть логически выведена) из формул fl, f2, . . ., fn". Обратите внимание на использование еще одного металингвистического символа, "├". Основной метод проведения такого доказательства известен под названием прямого логического вывода. Прямой логический вывод заключается в том, что правила логического вывода неоднократно применяются к предпосылкам, к формулам, дедуктивно выведенным из этих предпосылок, к формулам, дедуктивно выведенным из этих формул и т.д., до тех пор, пока не будет дедуктивно выведено заключение. Иными словами, процесс логического вывода, образно выражаясь, "разворачивается в прямом направлении в виде сплошной цепочки" от предпосылок до заключения. Но есть также несколько описанных ниже вариантов этого основного подхода.

1.           Принятие предпосылки. Если g имеет форму р ⇒ q, принять р в качестве допол

нительной предпосылки и показать, что q может быть дедуктивно выведена из за

данных предпосылок и р.

2.           Обратный логический вывод. Вместо попытки доказать, что р ⇒ q, доказать про тивоположное утверждение, NOT q ⇒ NOT p.

3.           Приведение к абсурду. Вместо того, чтобы доказывать непосредственно, что р  ⇒ q,

принять предположение, что р и NOT q одновременно являются истинными, и вы

вести из этого противоречие.

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

Рассмотрим метод резолюции более подробно, поскольку он имеет широкое  применение (в частности, он обобщается также на случай исчисления  предикатов, как будет показано в разделе 24.4).

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

следующие две формулы: f OR g и NOT g OR h, то можно исключить g и NOT g, чтобы вывести приведенную ниже упрощенную формулу:

3Вформальнойлогикевместотерминапредпосылкаприменяетсятакжетерминпосылка,илигипотеза.

f   OR  h

В частности, если дано, что f OR g и NOT g (т.е. можно принять, что h имеет значение TRUE), ТО МОЖНО вывести f.

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

А  ⇒ (   В   ⇒  С   ) ,   NOT  D  OR  А,   В   ├   D   ⇒  С

Здесь А, в, с и D — формулы. Начнем с того, что примем отрицание заключения в качестве дополнительной предпосылки, а затем запишем каждую предпосылку на отдельной строке следующим образом:

А  ⇒    (   В   ⇒   С   )

NOT  D  OR A

В

NOT    (   D   ⇒   С   )

Эти четыре строки неявно соединены друг с другом операторами "AND".

Теперь преобразуем каждую отдельную строку в конъюнктивную нормальную форму, т.е. в форму, состоящую из одной или нескольких формул, соединенных друг с другом операторами AND, притом что каждая отдельная формула содержит (возможно) операторы NOT и OR, но не операторы AND (CM. главу 18). Безусловно, вторая и третья строки уже находятся в этой форме. Для того чтобы преобразовать в нее остальные две строки, вначале удалим все вхождения оператора " ⇒ " (используя определение этого  оператора в

терминах NOT и OR), затем по мере необходимости применим распределительные законы

и законы де Моргана (см. начало этого раздела). Кроме того, можно удалить  лишние круглые скобки и пары смежных операторов NOT (которые отменяют друг друга). Четыре приведенные выше строки принимают следующий вид.

NOT AOR NOT В OR С

NOT DOR A

В

D ANDNOT С

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

NOT A OR NOT В OR С

NOT D OR A

В

D NOT С

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

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

NOT  D  OR  NOT  В  OR

С   В D  NOT  С

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

Теперь снова применим это правило и для этого снова выберем первые две строки

(при этом происходит резолюция формул NOT в и в); полученный результат показан ниже.

NOT   D   OR   С

D

NOT   С

Снова выберем первые две строки (NOT D и D) и получим следующий результат.

с

NOT   С

Опять же, применим это правило (с и NOT с); окончательный результат представляет собой пустое множество высказываний (которое обычно отображается следующим образом: [ ]); такой результат в соответствии с общепринятым соглашением рассматривается как противоречие. Таким образом, желаемый результат доказан путем приведения к абсурду.

Источник: Дейт К. Дж., Введение в системы баз данных, 8-е издание.: Пер. с англ. — М.: Издательский дом «Вильямс», 2005. — 1328 с.: ил. — Парал. тит. англ.

По теме:

  • Комментарии