Интеллектуальные системы (стр. 2 )

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

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

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

1.  AÚB=BÚA, AÙB=BÙA (коммутативность);

2.  (AÚB)ÚС=AÚ(BÚС), (AÙB)ÙС=AÙ(BÙС) (ассоциативность);

3.  (AÚB)ÙС=(AÙС)Ú(BÙC), (AÙB)ÚС=(AÚС)Ù(BÚC) (дистрибутивность);

4.  AÙA=A, AÚA=A (идемпотентность);

5.  ØØA=A (двойное отрицание);

6.  Ø(AÙB)=ØAÚØB, Ø(AÚB)=ØAÙØB (законы де Моргана);

7.  AÙT=A, AÚT=T (свойство истинны);

8.  AÙF=F, AÚF=A (свойство лжи);

9.  AÙØA=F (закон противоречия), AÚØA=T (закон исключения третьего);

10.  (AÚB)ÙA = A, (AÙB)ÚA = A (законы поглощения).

Всякое выражение исчисления высказываний может быть приведено либо к дизъюнктивной, либо к конъюнктивной нормальной форме (с использованием правил 1-10 или составления таблицы истинности).

Формула F находится в конъюнктивной нормальной форме тогда и только тогда, когда она имеет вид: FºF1Ù…ÙFn, n³1, где каждая из Fi, 1³i³n есть дизъюнкция литер.

Формула F находится в дизъюнктивной нормальной форме тогда и только тогда, когда она имеет вид: FºF1Ú…ÚFn, n³1, где каждая из Fi, 1³i³n есть конъюнкция литер.

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

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

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

Функции могут являться аргументами предикатов, а предикаты — нет. Количество переменных списка переменных функции или предиката называется их арностью (местностью). Формально рассматриваются 0-арные предикаты и функции. Функции с 0-й арностью (без аргументов) являются аналогами констант. Предикат с 0-й арностью (без аргументов) эквивалентен высказыванию.

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

Кроме того, в логике предикатов вводятся кванторы: квантор всеобщности (") и существования ($). С помощь их производится связывание переменных в логических формулах, в результате чего их арность уменьшается (на число кванторов). После связывания всех переменных в логических формулах образуется предложение (обычное высказывание). Так, ("x)A(x) – означает высказывание, состоящее в том, что для любого элемента x имеет место высказывание A(x); ($x)A(x) – означает высказывание, состоящее в том, что существует хотя бы один такой элемент x, для которого имеет место высказывание A(x).

Приоритет операций в логике предикатов убывает в следующем порядке: ", $, Ø, Ù, Ú, ®, «.

Справедливы следующие свойства кванторов, вытекающие из их смысла:

1.  ("x)A(x)®A(t);

2.  A(t) ®($x)A(x), где терм t свободен для переменной x в логической формуле A;

3.  Ø("x)A(x) = ($x)ØA(x), Ø($x)A(x) = ("x)ØA(x);

4.  ("x)(A(x)ÙB(x)) = ("x)A(x)Ù("x)B(x), ($x)(A(x)ÚB(x)) = ($x)A(x)Ú($x)B(x);

5.  ("x)("y)A(x, y)=("y)("x)A(x, y), ($x)($y)A(x, y) = ($y)($x)A(x, y);

6.  ("x)(A(x)ÙC)=("x)A(x)ÙC, ("x)(A(x)ÚC)=("x)A(x)ÚC;

7.  ($x)(A(x)ÙC) = ($x)A(x)ÙC, ($x)(A(x)ÚC) = ($x)A(x)ÚC;

8.  C®("x)A(x) = ("x)(C®A(x)), C®($x)A(x) = ($x)(C®A(x));

где формула C не содержит никаких вхождений переменной x.

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

2. Вывод в логических моделях

Проблема доказательства в логике состоит в нахождении истинностного значения заключения В, если предполагается истинность исходных посылок A1, А2, ..., Аn, что записывается в виде: А1, А2,... , Аn|- В. Знак |- в доказательствах и выводах следует читать «верно, что» или «можно вывести».

Семантический метод доказательства. Перечислить все атомы, входящие в формулы А1, А2,... , Аn, В, и составить таблицу истинности для всевозможных комбинаций значений этих атомов. Затем следует осуществить просмотр полученной таблицы, чтобы проверить, во всех ли ее строках, где формулы A1, A2, ..., An имеют значения «истина», формула В также имеет значение «истина».

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

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

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

Правило замены: если А«В (A = B), то А можно заменить на В в любом вхождении в формулу С, не меняя ее значения, причем замену не обязательно осуществлять во всех вхождениях.

Для обозначения тавтологий используется символ |=, который читается «общезначимо» или «всегда истинно», например: |=AÙ(A®B)®B.

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

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

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

1.  Устраняются операции эквивалентности и импликации:

А«В = (А®В)Ù(В®А); A®B = ØAÚB.

2.  Операция отрицания продвигается внутрь формул с помощью законов де Моргана:

Ø(АÙВ) = ØAÚØB; Ø(AÚB) = ØAÙØB.

3.  Для приведения логических формул к дизъюнктивной форме используют: AÚ(BÙQ) = (AÚB)Ù(AÚC).

4.  Для приведения логических формул к конъюнктивной форме используют: AÙ(BÚQ) = (AÙB)Ú(AÙC).

Умозаключение принимает форму:

A1, A2,…, AN |- B1; B2;…; BM,

где Ai – дизъюнкты литералов, а Bj – конъюнкты литералов. Это утверждение интерпретируется как высказывание, согласно которому если все высказывания A1, A2,…, AN верны, то будет верно хотя бы одно из высказываний B1, B2,…,BM.

5.  Составляем множество логических формул: A1, A2,…, AN, ØB1, ØB2,…, ØBM, где каждая логическая формула A1, A2,…, AN, ØB1, ØB2,…, ØBM является дизъюнктом литералов.

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

Правило резолюции: pÚq, rÚØq|- pÚr.

Частные случаи правила резолюции:

pÚq, Øq|- p;

q, Øq |- F.

Результат применения правила резолюции называют резольвентой. В последнем случае резольвента называется пустой (nil).

В логике предикатов имеют место следующие правила вывода:

1.  A, A®B |- B; B®A(x) |- B®("x)A(x); A(x)®B |- ($x)A(x)®B;

2.  ($x)(A(x)ÙB(x)) |- ($x)A(x)Ù($x)B(x), ("x)A(x)Ú("x)B(x) |- ("x)(A(x)ÚB(x));

3.  ("x)A(x)®C |- ($x)(A(x)®C), ($x)A(x)®C |- ("x)(A(x)®C),

где формула C не содержит никаких вхождений переменной x.

Этапы метода резолюций в логике предикатов.

В логике предикатов первого порядка для всякой формулы A, все переменные в которой связаны, существует эквивалентная ей формула A¢ в предваренной форме:

A¢ = (Q1x1)… (Qnxn)A²(x1,…., xn),

где Q1, …, Qn – некоторые кванторы, а A² - бескванторная формула.

Если C1, C2, …, Ck – дизъюнкты литералов, а x1,…, xm – различные переменные, содержащиеся в Ci (1≤i≤k), то формула вида ("x1)…("xm)(C1Ù…ÙCk) называется сколемовской нормальной или клаузальной формой.

Для доказательства общезначимости формулы F1, F2, …., Fn |- G по методу резолюций следует доказать противоречивость F1ÙF2Ù….ÙFnÙØG. Для этого последнюю формулу преобразуют к сколемовской нормальной форме. Преобразование осуществляется в 7 стадий.