Мова логіки предикатів
У визначеннях формальних мов. таких, як логічні мови або мови програмування, виділяють два основних аспекти: синтаксис і семантику. Синтаксис \ index<Синтаксис> визначає алфавіт. із символів якого будуються вирази мови, і правила, які виділяють з безлічі всіх слів в даному алфавіті правильно побудовані вирази. Для логічних мов такі вирази зазвичай називаються формулами, а для мов програмування - програмами. Семантика \ index<Семантика> займається визначенням сенсу, значення цих виразів. Для формул більшості логічних мов значенням є одне з істіностних значень. 1 (істина) або 0 (брехня), яке приписується формулою залежно від інтерпретації входять до неї символів мови. Наприклад, значення формул логіки висловлювань залежать від значень що входять до них булевих змінних. Значення формул визначається в цьому параграфі логіки предикатів будуть залежати від інтерпретації предикатів і функцій мови, а також від значень що входять до ці формули змінних.
Синтаксис: формули логіки предикатів
Формули мови логіки предикатів включають в себе символи (імена) предикатів з деякого Безліч, символи (імена) функцій з деякого безлічі, символи (імена) констант з деякого безлічі C =
Визначимо поняття терма даної сигнатури
Визначення 7.1. Терм. Термом називається вираз, що складається з змінних, ком, дужок і символів сигнатури, яке можна побудувати за такими правилами.
- Об'єктна змінна з Var є терм.
- Символ константи з C є терм.
- Якщо t1. tk - терми. а f (k) - символ функції з F. то f (t1. tk) є терм.
Терми. що не містять змінних, назвемо замкнутими.
Терми служать для завдання об'єктів. Замкнені терми задають об'єкти безпосередньо.
Тоді найпростіший спосіб поставити об'єкт - це вказати відповідну константу, наприклад, "Петро", "Джон", 0, 1, 47. Терм + (17, 25) задає об'єкт 42. терм лучшій_ друг (батько ( "Петро")) задає об'єкт - особа, яка є найкращим другом батька об'єкта "Петро". а терм зарплата (лучшій_ друг (батько ( "Петро"))) задає об'єкт число, яке представляє зарплату цієї особи. Значеннями змінних також є об'єкти. Тому терми зі змінними задають конкретні об'єкти при підстановці значень замість мінливих. Наведемо ще кілька прикладів термів даної сигнатури: x, батько (x), зарплата (лучшій_ друг (батько (батько (z)))), + (зарплата (лучшій_ друг (батько (z))), + (зарплата ( "Ольга ") 1000)), батько (5), + (батько (" Ольга ") 1000)). Відзначимо, що останні два терми побудовані відповідно до нашими правилами, але не зрозуміло, які об'єкти вони можуть задавати. Це залежить від визначення функції батько на числах і функції + на парах аргументів виду (Особа, Число). Часто під безліч об'єктів включають спеціальний об'єкт "ПОМИЛКА". який є значенням функцій на некоректних аргументах.
Вирази x +10, батько ( "Джон", "Петро"), + (100)>, лучшій_друг ( "Марія") термами даної сигнатури не є. (Визначте чому.)
Визначення 7.2. Атомна формула.
- Якщо t1 і t2 - терми. то вираз (t1 = t2) є атомної формулою.
- Будь-предикатний 0 місний символ з P є атомної формулою.
- Якщо P (k) (k> = 1) - предикатний k-місний символ з P. а t1. tk - терми. то вираз P (t1. tk) є атомної формулою.
Приклад 7.2. Розглянемо сигнатуру, в якій P = <живут_рядом (2). сын (2). дочь (2). родственники (2). человек (1). число (1). <= (2)>. а функції F і константи C визначені в прикладі вище.
Тоді такі вирази є атомними формулами. "Джон" = "Петро", "Петро" = 6, батько ( "Ольга") = "Петро", + (3,5) = + (1, + (6,1)), зарплата (лучшій_ друг (батько (z)) = 5000>, жівут_рядом ( "Джон", "Ольга"), син ( "Джон", "Ольга"), дочка ( "Ольга", x), родичі (лучшій_ друг ( "Джон"), батько (x)) і т.п.
Формули логіки предикатів будуються за такими правилами:
Визначення 7.3. Формула.
- Будь-яка атомна формула є формула.
- Якщо - формула, то - формула.
- Якщо і - формули, то вирази,, також є формулами.
- Якщо - формула, а - об'єктна змінна. то вираження і є формулами (в цьому випадку і називаються областю дії квантора або відповідно).
Поняття подформули для формул логіки предикатів визначається природним чином. По-перше, сама формула є своєї подформулой. По-друге, якщо формула має вигляд, або, то її подформуламі також є все подформули формули а якщо вона має вигляд, або, то її подформуламі також є все подформули формул і
Визначимо також поняття пов'язаних і вільних змінних формули. Входження змінної x в формулу називається пов'язаним. якщо воно входить в область дії деякого квантора або. В іншому випадку, воно називається вільним. Квантор () пов'язує в формулі () всі вільні входження змінної x в подформулу
Нехай в деякій сигнатуре є два двомісних предиката P (2). Q (2). Тоді у формулі
обидва входження x в подформулу пов'язані квантором, перше входження y є вільним, а друге - пов'язане квантором. Обидва входження x в подформулу пов'язані квантором.
Мінлива називається вільної (пов'язаної) у формулі, якщо у неї є хоч одне вільне (пов'язане) входження в цю формулу. Формула, яка не має вільних змінних. називається замкнутою. Відзначимо, що змінна може бути одночасно зв'язаною і вільною у цій формулі.
Приклад 7.3. Розглянемо приклади формул в сигнатурі з прикладу 7.2:
У цій формулі всі входження змінних x і y є пов'язаними і, отже, - замкнута формула. Змістовно, вона стверджує, що у кожної людини мається людина-сусід. Зрозуміло, що істинність цього твердження не залежить від імен змінних, використаних у формулі.
У формулі всі входження змінної y є пов'язаними, перше входження x також пов'язано, а друге входження x вільно, тому що не входить в область дії квантора. Таким чином x в є зв'язаною і вільною. Ця формула стверджує що є така людина, яка перебуває в родинних стосунках з усіма або не живе поруч з x і має зарплату> = 35. Ясно, що істинність цієї формули залежить від значення вільної змінної x.