6. Исчисление предикатов и теории первого порядка

Вид материала

Исследование

Содержание Синтаксис и семантика языка логики предикатов. Интерпретация языка логики предикатов. В является логическим следствием А’ в предваренной форме 6.3 Метод резолюции в логике предикатов. Опровержение методом резолюций. G не выводима из множества формул S 6.4 Принцип логического программирования.

Подобный материал:

• Удк 519. 816 Способ представления термов в логике предикатов первого порядка. Алгоритм, 184.64kb.
• «Искусственный интеллект.», 86.69kb.
• Концепция языка Пролог и сферы его применения. Процедурная и декларативная трактовка, 31.15kb.
• Логика высказываний. Основные понятия и определения. Логические функции одной и двух, 6.36kb.
• Основы логического программирования Исчисление высказываний, 192.9kb.
• Б. Д. Плющенков 1/2 года I. Общая теория дифференциального уравнения (нелинейного), 16.96kb.
• Язык Пролог Пролог (Prolog), 180.88kb.
• Лекция №13. Метод  аналитической  аппроксимации, 37.73kb.
• Решение дифференциального уравнения первого и второго порядка методом Рунге-Кутта 4-го, 55.71kb.
• Вопросы к экзамену по курсу «Уравнения математической физики» (6 семестр), 55.2kb.

6. Исчисление предикатов и теории первого порядка.


6.1 Исчисление предикатов. Основные понятия и определения.


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

Предикат - повествовательное предложение, содержащее предметные переменные, определенные на соответствующих множествах. При замене переменных конкретными значе­ниями (элементами) этих множеств предложение обращает­ся в высказывание, т.е. принимает значение "истинно" или "ложно". Обозначение предиката, содержащего п перемен­ных (n-местного предиката): Р(х₁, х₂,..., х_n), при этом пред­полагается, что х₁  М₁, х₂ М₂, ..., х_n  М_n.

С помощью логических связок (и скобок) предикаты мо­гут объединяться в разнообразные логические формулы - предикатные формулы. Исследование предикатных формул и способов установления их истинности является основным предметом логики предикатов. Логика предикатов вместе с входящей в нее логикой высказываний является основой ло­гического языка математики. С ее помощью удается форма­лизовать и точно исследовать основные методы построения математических теорий. Логика предикатов является важным средством построения развитых логических языков и фор­мальных систем (формальных теорий).

Логика предикатов, как и логика высказываний, может быть построена в виде алгебры логики предикатов и исчис­ления предикатов. Здесь, как и в случае логики высказыва­ний, для знакомства с основными понятиями логики преди­катов воспользуемся языком алгебры, а не исчислений. Та­кой выбор обусловлен рядом причин:

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

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

n - местный предикат - это функция Р(х₁, х₂,..., х_n) от п переменных, принимающих значения из некоторых задан­ных предметных областей, так что х₁  М₁, х₂  М₂, ., х_n  М_n, а функция Р принимает два логических значения - "истинно" или "ложно" (обозначения: {И, Л}, {1, 0}). Таким образом, предикат Р(х₁,х₂,...,х_n) является функцией типа Р: М₁ x М₂ x ... x М_n → B, где множества М₁, М₂, ..., М_n назы­ваются предметными областями предиката; х₁, х₂,..., х_n - предметными переменными предиката; В - двоичное (би­нарное) множество: В = {И, Л} или {1,0}. Если предикат­ные переменные принимают значения на одном множестве, то Р: Мⁿ→В.

Соответствия между предикатами, отноше­ниями и функциями:

1. Для любых М и п существует взаимно однозначное соответствие между n -местными отношениями и п - местными предикатами Р(х₁, х₂,..., х_n), Р: Мⁿ→В:

• каждому n - местному отношению R соответствует пре­дикат Р(х₁, х₂,..., х_n) такой, что Р(a₁, a₂,..., a_n) = 1, если и только если (a₁, a₂,..., a_n)  R;

• всякий предикат Р(х₁, х₂,..., х_n) определяет отношение R такое, что (a₁, a₂,..., a_n)  R, если и только если Р(a₁, aх₂,..., a_n) = 1.

При этом R задает область истинности предиката Р.

2. Всякой функции f(х₁, х₂,..., х_n), f: Мⁿ → М, соответ­ствует предикат Р(х₁, х₂,..., х_n, х_n+1), Р: Мⁿ⁺¹→В, такой, что Р(a₁, a₂,..., a_n, a_n+1 ) = 1, если и только если f(a₁, aх₂,..., a_n) = a_n+1.

Понятие предиката шире понятия функции, поэтому обратное соответствие (от (n+1)-местного преди­ката к n - местной функции) возможно не всегда, а только для таких предикатов Р’ для которых выполняется условие, свя­занное с требованием однозначности функции.

1. Синтаксис и семантика языка логики предикатов.
   

Определим синтаксис логики предикатов первого порядка.

Классическое исчисление предикатов (первого порядка) - это формальная теория, в которой определены следующие компоненты:

1. Алфавит

связки основные  

дополнительные & 

служебные символы ( , )

кванторы всеобщности 

существования 

предметные константы a, b, ..., a₁, b₁, ...

переменные x, y, ..., x₁,y₁, ...

предметные предикаты P, Q, ...

функторы f, g, ...


2. Формулы имеют следующий синтаксис:

<формула> :: = <атом> |

<формула> |

(<формула>  <формула>)

<переменная><формула>|

< переменная >< формула >

<атом> :: = <предикат>(<список термов>)

<список термов> :: = <терм> | <терм>, <список термов>

<терм> :: = <константа> |

<переменная> |

<функтор>(<список термов>)

При этом должны быть выполнены следующие контекстные условия: в терме f(t₁, ..., t_n) функтор f должен быть n-местным. В атоме (или атомарной формуле) P(t₁, ..., t_n) предикат P должен быть n – местным.

Далее вставка 6А

Вхождения переменных в атомарную формулу называются свободными. Свободные вхождения переменных в формулах А и В остаются свободными и в формулах А и А  В. Вхождения переменной x в формулы x A и x A называются связанными. Вхождения других переменных (отличных от x), которые были свободными в формуле А, остаются свободными. Формула, не содержащая свободных вхождений переменных, называется замкнутой.

Формулы вида A и A, где A - атом, называются литеральными формулами (или литералами).

В формулах x A и x A подформула A называется областью действия квантора по x.

Обычно связки и кванторы упорядочивают по приоритету следующим образом: , , , , , . Лишние скобки при этом опускают.

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

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

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

Интерпретация языка логики предикатов.

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

Интерпретация I (прикладного) исчисления предикатов  с областью интерпретации (или носителем) M - это набор функций, которые сопоставляют

• каждой предметной константе a элемент носителя, I(a): (a)M;
  
• каждому n-местному функтору f конкретную функцию на М , I(f): Mⁿ  M;
  
• каждому n-местному предикату P конкретное отношение в области интерпретации М, I(P) : Р^п→0,1.
  

Если s^*(P) = И, то говорят, что формула P выполнена на s.

Формула A выполнена на s тогда и только тогда, когда формула A не выполнена на s.

Формула A  B не выполнена на s тогда и только тогда, когда формула A истинна, а В ложна.

Далее вставка 6В

Формула называется истинной в данной интерпретации I, если она выполнена на любом наборе s элементов M. Формула называется ложной в данной интерпретации I, если она не выполнена ни на одном наборе s элементов M.

Интерпретация называется моделью множества формул , если все формулы из  истинны в данной интерпретации.

Всякая замкнутая формула истинна или ложна в данной интерпретации. Открытая (то есть не замкнутая) формула A(x, y, z, ...) истинна в данной интерпретации тогда и только тогда, когда ее замыкание x y z ... A(x, y, z, ...) истинно в данной интерпретации. Это обстоятельство объясняет, почему собственные аксиомы прикладных теорий обычно пишутся в открытой форме.

Общезначимость

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


Логическое следование и логическая эквивалентность.

Формула В является логическим следствием формулы А (обозначение: А  В), если формула В выполнена на любом наборе в любой интерпретации, на котором выполнена формула А. Формулы А и В логически эквивалентны (обозначение: А = В), если они являются логическим следствием друг друга. Имеют место следующие логические следования и эквивалентности:

1.  x A(x) =  x A(x),  x A(x) =  x A(x),

2.  x (A(x) & B(x)) =  x A(x) &  x B(x),  x (A(x)  B(x)) =  x A(x)   x B(x),

3.  x (A(x) & B(x))   x A(x) &  x B(x),  x A(x)   x B(x)   x (A(x)  B(x)),

4.  x  y A(x, y) =  y  x A(x, y),  x  y A(x, y) =  y  x A(x, y),

5.  x (A(x) & C) =  x A(x) & C,  x (A(x)  C) =  x A(x)  C,

6.  x (A(x) & C) =  x A(x) & C,  x (A(x)  C) =  x A(x)  C,

7. C   x A(x) =  x (C  A(x)), C   x A(x) =  x (C  A(x)),

8.  x A(x)  C   x (A(x)  C),  x A(x)  C  x (A(x)  C)

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

Для всякой формулы А существует логически эквивалентная ей формула А’ в предваренной форме:


,

где - некоторые кванторы, а - бескванторная формула.


6.3 Метод резолюции в логике предикатов.

Далее вставка 6С

Правило резолюции для исчисления предикатов.

Другими словами, при применении правила резолюции нужны контрарные литералы в резольвируемых предложениях. Пусть С₁ и С₂ - два предложения в исчислении предикатов. Правило вывода



называется правилом резолюции в исчислении предикатов, если в предложениях С₁ и С₂ существуют унифицируемые контрарные литералы P₁ и P₂, то есть C₁ = P₁  и C₂ = P₁ , причем атомарные формулы P₁ и P₂ являются унифицируемыми наиболее общим унификатором .В этом случае резольвентой предложений C₁ и C₂ является предложение ( ), полученное из предложения  применением унификатора .


Опровержение методом резолюций.

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

S├ G.

Каждая формула множества S и формула G (отрицание целевой теоремы) независимо преобразуются в множества предложений. В полученном совокупном множестве предложений C отыскиваются резольвируемые предложения, к ним применяется правило резолюций и резольвента добавляется в множество до тех пор, пока не будет получено пустое предложение. При этом возможны три случая:

1. Среди текущего множества предложений нет резольвируемых. Это означает, что теорема опровергнута, то есть формула G не выводима из множества формул S.
   
2. В результате очередного применения правила резолюции получено пустое предложение. Это означает, что теорема доказана. то есть S├ G.
   

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


6.4 Принцип логического программирования.

Далее вставка 6D

5. Формы представления логических формул.
   

Далее вставка 6E1-6E2


6.5 Вопросы для самопроверки.

1) Что такое исчисление предикатов?

2) Дать основные понятия исчисления предикатов.

3) В чем заключается метод резолюции в логике высказываний и в логике предикатов?

4) Чем отличается логика высказываний от логики предикатов?

5) Записать на языке предикатов:

а) все аспиранты учатся;

б) некоторые спортсмены отличники;

в) для любого числа можно найти большее число.