Функція або предикатний символ складається з термів – клас логічних понять, утворених константами або предметними змінними. Якщо f – n–місцевий функціональний символ, а t1,…tn – терми, то f(t1,…tn) –терм. Предикат – пропозиційна функція предметних змінних, заміна яких на сталі перетворює цю функцію на осмислене висловлювання. Предикат P(t1,…tn) – де P – n–місцевий предикатний символ, а t1,…tn –терми, є атомарною формулою ЛП першого порядку.
Квантори ((загальності), (існування))
– спеціальні символи, що для характеристики змінних. Діють на формулу, до якої
застосовуються. - відповідає за істинність
формули для всіх об’єктів, - хоча б для одного
об’єкта. Входження змінної х у формулу є зв’язаним, якщо х
є змінною квантора, що входить в цю формулу або діє на такий квантор. Інакше
входження є вільним. Змінні є вільними, якщо існують їх
вільні входження в формулу і зв’язаними, якщо існують зв’язані
входження.
(P(x,y)→x P(x) перше
входження х вільне, друге і третє зв’язані, у – вільна змінна)
Формула ЛП P(x) є вільною для змінної y, якщо в P відсутні вільні входження х, які підпадають під дію кванторів y або y. Підставити змінну у замість х у предикатну форму Р – значить замінити кожне вільне входження змінної х у Р входженням у. (Якщо P(x) має вигляд H(x,z)→y Q(y), то Р є вільною для у, якщо – H(x,z) y Q(x,y)), то Р не є вільною для у).
Вираз, який будується на основі атомарних формул, логічних відношень і кванторів, є ППФ ЛП.
Фразова форма – форма ЛП, де кожна фраза, це множина позитивних або негативних атомарних формул, поєднаних знаком . С початку розміщують позитивні фрази, потім негативні:
I1I2…InП1П2Пk = I1I2…In~(In+1In+2…In+k) = In+1In+2…In+k→ I1I2…In
Позитивні фрази є альтернативними висновками, негативні – необхідними умовами.
Квантори та ставлять перед формулою, якщо вона є істиною для якої-небудь змінної чи іншого об’єкта (Для кожного х існує хоча б одне значення у вхy [Q(x,y) P(x)], якщо вираз у [] істинний).
Нормальною формою у ЛП є попередньо нормальна форма (ПНФ). Формула, записана в ПНФ, має вигляд , де – префікс у вигляді або, а М –формула без кванторів.
Основні правила ЛП:
1. Правило узагальнення. Нехай Q-формула, що містить вільні входження змінної x і P(x) –формула. Тоді, якщо Q → P(x) є вивідною формулою (такою, що можна вивести з попередніх формул), то і Q →x P(x) є вивідною .
2. Правило зв’язування фактором існування. Нехай Q-формула, що не містить вільних входжень змінної x і P(x) –формула. Тоді, якщо P(x) → Q є вивідною формулою, то і x P(x)→ Q є вивідною .
3. Правило універсальної конкретизації. Нехай P(x) формула вільна для у. Тоді з x P(x) можна вивести P(y) підстановкою у P(x) замість змінної x змінної y.
4. Правило спеціалізації.Якщо деякому класу притаманна якась властивість, то будь-який об’єкт цього класу буде її мати: x P(x), аP(а).
5. Правило конкретизації для квантора існування. Нехай a – такий певний елемент, що коли формула x P(x) є істиною, то формула P(а) також буде істинною. Тоді x P(x), аP(а).
ПРАВИЛО РЕЗОЛЮЦІЇ
У загальному випадку метод резолюції – це логічний висновок, заснований на силогізмі, в основі якого є операції, подібні до імплікації.
Силогізм – це дедуктивний умовивід, де з двох суджень (посилань) дістають обумовлене третє судження (висновок).
Правило резолюції: якщо в будь-яких двох диз’юнктах А1 і А2 існує контрактна пара літер (L і ~L), то викресливши ці літери, можна побудувати диз’юнкцію з тих частин диз’юнктів А1 і А2, що залишаться.
Якщо аргументами виступають змінні (х,y), то вони уніфікуються з будь-якими константами.
Приклади:
Уважаемый посетитель!
Чтобы распечатать файл, скачайте его (в формате Word).
Ссылка на скачивание - внизу страницы.