Аксиоматические теории первого порядка

⇐ ПредыдущаяСтр 2 из 6Следующая ⇒

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

1. Язык:

1). Символы: служебные: ®, , (, ), ", $

предметные переменные: z, y, x, ...

вещественные переменные: a, b, c, ...

функциональные символы: f, g, h, ...

символы предикатов: P, Q, R, ...

2). Терм:

Константа или переменная есть терм.

Если t₁, t₂, ... t_n- термы, то f(t₁, t₂, ... t_n) - тоже терм.

3). Формула:

Если t₁, t₂,...t_n - термы, то Р(t₁, t₂,...t_n) - формула.

Если P, Q - формулы, то

(Р), P ® Q, P, " xP, $xP - также формулы.

2. Аксиомы:

1)-3) - соответствуют схемам аксиом логики высказываний.

4)" x A(x) ® A(t)

5)A(t) ® $x A(x)

где терм t свободен для x.

Терм t называется свободным для переменной x , если никакое свободное вхождение x в A не лежит в области действия никакого квантора " y, где y переменная, входящая в t.

Например, терм y свободен для переменной x в A(x), но не свободен для переменной x в " y A(x). Терм f(x, z) свободен для x в " yA(x, y) ® B(x), но не свободен для х в $z " yA(x, y) ® B(x).

3. Правила вывода:

1). A, A ® B ½ ¾ B ( m.p.)

2) B ® A(x) ½ ¾ B ® " x A(x)

3) A(x) ® B½ ¾ $x A(x) ® B

Вышеприведенное исчисление называют еще исчислением предикатов.

На практике, как правило, к этим аксиомам, называемым логическими аксиомами

(коль скоро они описывают логическую составляющую рассматриваемого " мира" ), добавляют еще аксиомы, описывающие конкретную " предметную область". Например, законы управления автоматическим регулятором или роботом.

Такие аксиомы называются собственными аксиомами теории, а сами теории - аксиоматическими теориями первого порядка или короче, теориями первого порядка.

Теории первого порядка неполны, но, как правило, непротиворечивы. (Хотя специалистов по искусственному интеллекту больше интересуют " локально-противоречивые системы". Однако, чем больше такой интерес, тем дальше они отходят от " классической математической логики" со всеми вытекающими последствиями).

Говоря о теориях первого порядка нельзя хотя бы не намекнуть на существование теорий более высоких порядков. Так, например, формула " P " x P (x) – уже не принадлежит к языку теорий первого порядка из-за квантора " P.

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

Метод предложен Дж. Робинсоном в 1965 году.

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

1. Язык метода резолюции - язык дизъюнктов:

2. Аксиомы только собственные.

3. Правило вывода - резолюция

Важное замечание. Доказательство корректности метода резолюции Дж. Робинсон выполнил с привлечением теории моделей, раздела математической логики, который в данном курсе не рассматривается. Поэтому мы воспользуемся " правдоподобными" рассуждениями, которыми изобиловали первые книги по языку Пролог (Prolog). А язык Пролог (Программирование с помощью Логики) - язык, основной представитель класс языков логического программирования, базируется как раз на методе резолюции!

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

Традиционный силлогизм: A ® B, B ® C ½ ¾ A ® C

Применительно к дизъюнктивной записи можно представить как

A Ú B A Ú B Ú D

B Ú C или " обобщенный" вариант B Ú C Ú E

A Ú C A Ú C Ú D Ú E

Унификация:

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

a(const)®xy(из той же области)

f(z)

Вывод здесь заключается в том, что в систему добавляется отрицание формулы (дизъюнкта! ), которую необходимо вывести. Вывод состоит в последовательном применении резолюции до получения пустого дизъюнкта ð. Это будет, с точки зрения интерпретации, означать, что не существует никакой модели («мира»), в которой бы была справедлива исходная система законов (дизъюнктов). А коль скоро доказательство выполняется методом от противного, то значит первоначальная формула (дизъюнкт) действительно выводима (и, значит, справедлива) в данной теории.

Пример 1: Можно сказать, что это прообраз или предельно упрощенный вариант «системы искусственного интеллекта».

Пусть мир описывается двумя аксиомами:

Миша повсюду ходит за Леной А1." x(B(Л, x) ® B(M, x))

Лена в школе А2.B(Л, Ш)

Требуется доказать (ответить на вопрос)

Где Миша? А3. $х B(M, x)?

Вопрос (доказываемую формулу с добавленным знаком вопроса) $х B(M, x)?

преобразуем в. $х B(M, x) (отрицание вопроса). Далее

задвигаем отрицание за квантор, производим сколемизацию и

добавляем специальный «предикат ответа», который будет аккумулировать процесс унификации). В результате получаем дизъюнкт:

. B(M, x) Ú Отв(М, x)

Вся система (две аксиомы и вопрос) будет состоять из трех дизъюнктов:

Д1: B(Л, x) Ú B(M, x)

Д2: B(Л, Ш)

Д3: B(M, x) Ú Отв(M, x)

Вывод:

Резолюция Д1-Д2 дает Д4: B(M, Ш)

Резолюция Д4-Д3 дает Д5: ð Ú Отв(M, Ш)

То есть. предикат ответа (при получении пустого дизъюнкта) можно интерпретировать как «Миша в школе».(Интерпретация ответа в системе искусственного интеллекта остается за человеком).

Пример 2:

1. Если х является родителем y и y является родителем z, то х является прародителем z.

А1. " xyz(P(x, y) & P(y, z) ® P(x, z)

2. Каждый человек имеет своего родителя.

A2. " y$xP(x, y)

3. Существуют ли такие х и у, что х является прародителем у?

$xyP(x, y)?

Преобразуем аксиомы в дизъюнкты.

Д1. Ø Р(х, у) Ú Ø Р(у, z) Ú P(x, z)

Д2. P(f(y), y)

Д3.Ø P(x, y) Ú Отв(x, y)

Д1 - Д2: Д4: Ø Р(у, z) Ú P( f(y), z)

Д4 – Д2: Д5: P(f(f(y)), y)

Д5 – Д3: Д6: Ú P(f(f(х)), х)

Заметим, что каждая переменная имеет уникальное имя в пределах одного дизъюнкта. Переменные, названные одинаково в разных дизъюнктах - это разные переменные. Интерпретация результата лежит на человеке. Будем интерпретировать

f(х)- как быть родителем х. То есть f(f(х) - родитель родителя х. Следовательно, P(f(f(х)), х) – прародитель х - это родитель родителя х.

Логика предикатов

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

Если переменная одна, то предикат одноместный, две - двухместный и т.д.

Нульместный предикат, то есть предикат, не содержащий переменных - высказывание.

Операции:

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

Здесь уместно сделать важное содержательное замечание:

Язык предикатов - наиболее приближенный к естественным языкам формальный математический (логический) язык.

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

" - квантор общности. " x P(x) - " для всех х - P(x)".

$ - квантор существования. $x P(x) - " есть такие х, что P(x)".

( $! или $₁ - существует и притом единственный).

Кванторы связывают соответствующие переменные. Связанные переменные можно воспринимать как константы, а несвязанные переменные - свободные переменные -

как собственно переменные.

Содержательные примеры предикатов:

R(x) - х любит кашу (одноместный предикат).

" x R(x) - все любят кашу (нульместный предикат - высказывание).

$x R(x) - некоторые (есть такие) х любят кашу.

L(x, y) - х любит y (двухместный предикат).

$x" y L(x, y) - Существует x, который любит всех y.

" x ( C(x) ® O(x) ) - Все студенты C(x) отличники O(x).

$x ( C(x) & O(x) ) - Некоторые студенты C(x) отличники O(x).

Здесь есть повод поразмышлять об использовании операций ® и & в двух последних высказываниях.

Для конечных областей можно операции навешивания кванторов выразить через конъюнкцию и дизъюнкцию:

Пусть х Î {a₁, a₂, ..., a_n}

" x P(x) = P(a₁) & P(a₂) & ... & P(a_n).

$x P(x) = P(a₁) Ú P(a₂) Ú ... Ú P(a_n).

⇐ Предыдущая 123 4 5 6 Следующая ⇒