Функція або предикатний символ складається з термів – клас логічних понять, утворених константами або предметними змінними. Якщо 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 = I1
I2
…
In
~(In+1
In+2
…
In+k)
= In+1
In+2
…
In+k→
I1
I2
…
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).
Ссылка на скачивание - внизу страницы.