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

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

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.

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

Метод предложен Дж. Робинсоном в 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(х)), х) – прародитель х - это родитель родителя х.