Алгебра предикатів. Квантори

Приклад.

На множині М = {a, d} задамо предикат Р₁ (х, у) та Р₂ (х, у). Розглянемо дві формули:

А₁⁽²⁾ (х₁, х₂) & А₁⁽²⁾ (х₁, х₃);              (1)

А₁⁽²⁾ (х₁, х₂) & А₁⁽²⁾ (х₂, х₃).               (2)

Якщо областю  інтерпретації слугує множина М і формула А₁⁽²⁾ інтерпретується як предикат Р₁, то формули (1) і (2) є рівносильними в цій інтерпретації, оскільки набувають значення 1 тільки на двох наборах вільних змінних: áа, а, аñ та ád, d, dñ.

Якщо областю  інтерпретації є множина М, але формула А₁⁽²⁾ інтерпретується як предикат Р₂, то формули (1) і (2) – нерівносильні, оскільки в наборі áа, d, dñ формула (1) набуває значення 1, а формула (2) – значення 0.

Формули (" х₁) А₁⁽¹⁾ (х₁) й ($ х₁) А₁⁽¹⁾ (х₁) є рівносильними на одноелементній множині. Справді, якщо область інтерпретації – одноелементна множина, то який би предикат не взяти як інтерпретацію А₁⁽¹⁾ на цій множині, він набуває тільки одного значення: 1 або 0. У першому випадку обидві формули набувають значення 1, у другому – 0, і, отже, вони  є рівносильними на цій множині. З іншого боку, на двоелементній множині {a, b} ці формули – нерівносильні. Досить як інтерпретацію А₁⁽¹⁾  розглянути предикат Р такий, що Р(а) = 1, Р(b) = 0. Наведемо кілька правил переходу від одних формул до інших, рівносильних їм (у всіх інтерпретаціях).

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

1. Винесення квантора за дужки.

 Нехай, А(х) містить вільну змінну х, формула В не містить змінної х й обидві вони задовольняють п. 3 означення формул. Тоді

($ х)( А(х)& В) º ($ х) А(х)& В;

(" х)( А(х)& В) º (" х) А(х)& В;

($ х)( А(х)Ú В) º ($ х) А(х)Ú В;

(" х)( А(х)Ú В) º (" х) А(х)Ú В;

Доведемо  першу з цих рівностей (інші доводяться аналогічно).

Нехай, х_і,1 ,...,х_і,n   - усі вільні змінні формули ($ х)( А(х)& В). Тоді вони ж будуть усіма  вільними змінними формули ($ х) А(х)& В.

Розглянемо  довільну інтерпретацію з множиною М. Нехай, áа₁, ..., а_nñ, а_і є М – довільний набір значень вільних змінних х_і,1 ,...,х_і,n . Оскільки формула В не  містить вільної змінної х, можна визначити значення цієї формули в наборі áа₁, ..., а_nñ (точніше, в його частині, що стосується вільних змінних формули В). Якщо  Вê_á а_{1, ....,}а_nñ = 0 , то  (($ х) А(х)& В) _á а_{1, ....,}а_nñ = 0 і для будь-якого елемента а з множини М у наборі значень áа₁, ..., а_nñ своїх вільних змінних х, х_і,1 ,...,х_і,n формула  А(х)& В  набуває значень 0. Звідси  ($ х) А(х)& В½_á а_{1, ....,}а_nñ = 0. Якщо   Вê_< а_{1, ....,}а_{n >} =1 , то для будь-якого елемента а з множини М у наборі значень áа, а₁, ..., а_nñ формули А(х)& В й А(х) набувають однакових істинностей. Звідси,  (($ х) А(х)& В)½_á а_{1, ....,}а_nñ = ($ х) А(х)½ _á а_{1, ....,}а_nñ = ($ х) А(х)& В½_á а_{1, ....,}а_n.

Зазначимо, що коли не вимагати, щоб формула В не містила змінної  х, то  будуть справджуватися тільки дві рівносильності:

(" х) (А(х)) & В(х) º (" х) А(х) & (" х) В(х);

($ х) (А(х) Ú В(х)) º ($ х) А(х) Ú ($ х) В(х).

2. Переставлення однойменних кванторів.

 Для кванторів $ та" маємо

(" у) (" х) А(х, у) º  (" х) (" у) А(х, у);

($ у) ($ х) А(х, у) º  ($ х) ($ у) А(х, у).

3. Зв’язок кванторів із запереченням.

Нехай, А – формула, що містить вільну змінну х. Тоді справджуються рівносильності:

Ø (" х) А(х) º ($ х) Ā(х)

Ø ($ х) А(х) º (" х) Ā(х)

Приклад.

Розглянемо такі формули:

1. А₁⁽¹⁾ (х₁) Ú А₂⁽²⁾ (х₁, х₂).
2. (" х₁)  А₁⁽¹⁾ (х₁) & ($ х₂) Ā₂⁽²⁾(х₂, х₃).
3. (" х) А₁⁽¹⁾ (х₁) ® ($ х₂) Ā₁⁽¹⁾(х₂).

Лише перші дві формули є зведеними.

Теорема1.[2, стор. 155-158]

Для будь-якої формули існує рівносильна їй зведена формула, причому множини вільних і зв’язаних змінних цих формул збігаються.

Така зведена формула  називається зведеною формою заданої  формули.

Користуючись рівносильностями логіки висловлень, легко вказати  формулу, рівносильну заданій, що містить із логічних символів тільки &, Ú, ¯. Тому будемо вважати, що формули, які розглядаються, містять тільки ці логічні символи.

Доведемо це твердження методом індукції за довжиною формули. При n=1 формула є атомарною і, отже, зведеною.

Припустимо, що для формул, довжина яких менша від n, твердження теореми справджується. Доведемо його для формули F завдовжки n. Позначимо довжину формули F через .

Формула F має вигляд: або .

Випадок1. Оскільки , за індуктивним припущенням існують зведені формули та формули G й H відповідно, і множини вільних та зв’язних змінних формул і G, й H збігаються. Тоді - формула, . Звідси - зведена форма формули із тією самою множиною вільних і зв’язаних змінних, що й .

Випадок2. Він аналогічний випадку 1.

Випадок3. Тут формула G може мати такий вигляд:

3.1) ;

3.2) ;

3.3) ;

3.4) ;

3.5) ;

Випадок3.1. Тут , де . За індуктивним припущенням існують зведені формули та , рівносильні та відповідно, і множини вільних та зв’язаних змінних формул і , і збігаються. Тоді - зведена форма формули з тією самою множиною вільних змінних.

Випадок3.2. Він аналогічний випадку 3.1.

Випадок3.3. Тут , де . Застосовуючи індуктивне припущення до формули , дістаємо зведену форму формули з тією самою множиною вільних та зв’язаних змінних.

Випадок3.4. Тут , де . За індуктивним припущенням існує зведена формула , рівносильна формулі , з тією самою множиною вільних та зв’язаних змінних. Тоді - зведена форма формули .

Випадок3.5. Він аналогічний випадку 3.3.

Випадок4. Формула має довжину . За індуктивним припущенням існує зведена форма цієї формули з тією самою множиною вільних та зв’язаних змінних. Тоді - зведена форма формули .

Випадок5. Він аналогічний випадку 4. Теорему доведено.

Зведена формула називається нормальною, якщо вона не містить символів кванторів або всі символи кванторів записані попереду (тобто логічні символи і символи предикатів знаходяться в області дії кожного квантора).

Приклад. Розглянемо такі формули:

1. - нормальна формула.
2. - зведена формула, що не є нормальною.

 

Теорема2.[2, стор. 158-161]

Для будь –  якої зведеної формули існує рівносильна  їй нормальна формула тієї самої довжини.

І ця формула(нормальна формула тієї самої довжини) називається нормальною формулою заданої зведеної формули.

Доведення проведемо  методом індукції за довжиною n формули. При n=1 формула є атомарною і, отже, нормальною.

Припустимо, що твердження теореми справджується для всіх формул, довжина яких менша від n. Нехай F - формула завдовжки n. Тоді формула F має вигляд: або .

Випадок1. За умовою - зведена формула. Тоді та також є зведеними формулами, довжина яких менша від n. За індуктивним припущенням існують рівосильні їм нормальні формули та відповідно, де . Якщо формули й не містять символів кванторів, то - нормальна форма завдовжки n формули .

Нехай, наприклад, формула  містить символ квантора. Тоді має вигляд:  , де (випадок коли має вигляд , є аналогічним). Якщо змінна х входить в формулу , то тільки як зв’язана (інакше порушується означення формули). Застосувавши правило перейменування зв’язаних змінних, перейдемо до формули , рівносильної і такої, що не має змінної х. Очевидно, - зведена формула тієї самої довжини, що й . За правилом винесення квантора за дужки .

Оскільки  , за індуктивним припущенням існує рівносильна нормальна їй формула тієї самої довжини. Тоді - нормальна форма формули тієї самої довжини.

Випадок2. Він аналогічний випадку 1.

Випадок3. Оскільки формула - зведена, є атомарною формулою, і тоді - нормальна формула.

Випадок4. Тут - зведена формула, . За індуктивним припущенням існує рівносильна їй нормальна формула тієї самої довжини. Тоді - нормальна форма формули завдовжки n.

Випадок5. Він аналогічний випадку 4. Теорему доведено.

Теорема3.[2, стр. 161-162]

Для будь –  якої формули існує рівносильна  їй нормальна формула.

 

6. Реалізація програми на перевірку істинності відношень предиката

Постановка  задачі для програми

Задача побудована таким чином, що користувач повинен  вести довільний предикат, який може містити лише дозволені символи ('+' '-' '=' '<' '>' '<>' '<=' '>=' '*' '/'), а також довільні числа і результат програми повинен видати користувачу інформацію щодо істинності введеного предиката.

Опис програми

Дана програма написана на мові С++(консольне виконання), у програмному середовищі «Visual Studio 2012». В даній програмі реалізується алгоритм перевірки на істинність введеного предиката.

Логіка даної  програми полягає в наступному:користувач вводить предикат довільної довжини із дозволених символів('+' '-' '=' '<' '>' '<>' '<=' '>=' '*' '/'), а також довільних чисел із множини натуральних чисел (N), і серед введеного предиката програма робить пошук, спочатку усіх знаків множення та ділення, та виконує дані операції між числами, до яких даний операнд відноситься, а після цього усі інші дії. І так виконавши усі математичні операції програма перевіряє на істинність відношень, які задані в предикаті, який був заданий користувачем. В результаті користувач отримує висновок про істинність предиката.

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

Код програми

#include <iostream>//Бiблiотека для вводу/виводу

#include <string>//Бiблiотека для роботи зi стрiчками

using namespace std;

 

//Опис  функцiй

void printInterface();/*Вивiд iнтерфейсу програми*/

void getNumbersNearOperand(int i, int move1, int move2, char *myString, char *get2, char* get1, int forGet2, int forGet1, int *k2, int *k1, int *numOne, int *numTwo);/*Отримуємо числа бiля арифметичних дiй i бiля '<' '>' '='*/

void getNumbersNearSpecialOperand(int i, int move1, int move2, char *myString, char *get2, char* get1, int forGet2, int forGet1, int *k2, int *k1, int *numOne, int *numTwo);/*Отримуємо числа бiля '<=' '=>' '<>'*/

int checkCorrectness(char *myString, char *spec, int *isCorrect);/*Перевiряє на присутнiсть недопустимих символiв*/

void checkForPresentSpec(char *myString, char *spec, int *isCorrect);/*Перевiряє на присутнiсть вiдношення у предикатi*/

void doAllMultiplication(char *myString, char *get1, char *get2, char *get3, int *k1, int *k2, int numOne, int numTwo, int *forGet1, int *forGet2, int *forGet3, int move1, int move2);/*Виконуємо усi дiї множення у предикатi*/

void doAllDivision(char *myString, char *get1, char *get2, char *get3, int *k1, int *k2, int numOne, int numTwo, int *forGet1, int *forGet2, int *forGet3, int move1, int move2);/*Виконуємо усi дiї дiлення у предикатi*/

void doAllSum(char *myString, char *get1, char *get2, char *get3, int *k1, int *k2, int numOne, int numTwo, int *forGet1, int *forGet2, int *forGet3, int move1, int move2);/*Виконуємо усi дiї додавання у предикатi*/

void doAllDifference(char *myString, char *get1, char *get2, char *get3, int *k1, int *k2, int numOne, int numTwo, int *forGet1, int *forGet2, int *forGet3, int move1, int move2);/*Виконуємо усi дiї вiднiмання у предикатi*/

void checkCorrectOfOperands(char *myString, int numOne, int numTwo, int *k1, int *k2, int *forGet1, int *forGet2, int *forGet3, int move1, int move2, char *get1, char *get2);/*Перевiряємо на iстиннiсть вiдношення*/

 

void main()

{

setlocale(LC_ALL,"Ukrainian");/*Пiдключення української мови*/

 

//Оголошення змiнних

int forGet1=0, forGet2=0, forGet3=0;

int move1=0,move2=0, k1=0,k2=0;

char get1[10],get2[10],get3[10];

int numOne=0, numTwo=0;

char spec[] = "><=-+/*";

int isCorrect=0;

char myString [256];

 

printInterface();

 

//Ввiд стрiчки  та перевiрка її на допустимiсть  символiв

do

{

cin.getline(myString,255);

isCorrect = 1;

checkCorrectness(myString, spec, &isCorrect);

}

while(isCorrect==0);

 

//Послiдовний виклик  функцiй, призначення яких описано  вище

checkForPresentSpec(myString, spec, &isCorrect);

 

doAllMultiplication(myString, get1, get2, get3, &k1, &k2, numOne, numTwo, &forGet1, &forGet2, &forGet3, move1, move2);

doAllDivision(myString, get1, get2, get3, &k1, &k2, numOne, numTwo, &forGet1, &forGet2, &forGet3, move1, move2);

doAllSum(myString, get1, get2, get3, &k1, &k2, numOne, numTwo, &forGet1, &forGet2, &forGet3, move1, move2);

doAllDifference(myString, get1, get2, get3, &k1, &k2, numOne, numTwo, &forGet1, &forGet2, &forGet3, move1, move2);

 

checkCorrectOfOperands(myString, numOne, numTwo, &k1, &k2, &forGet1, &forGet2, &forGet3,

move1, move2, get1, get2);

 

//Затримка консольного  вiкна

system("pause");

}