Лекция из курса Основы программирования на языке Пролог - часть 2

Если предикатный (функциональный) символ имеет n аргументов, он называется n-местным предикатным (функциональным) символом.

Термом будем называть выражение, образованное из переменных и констант, возможно, с применением функций, а точнее:

1. всякая переменная или константа есть терм;
2. если t1,...,tn — термы, а f — n-местный функциональный символ,то f(t1,...,tn) — терм;
3. других термов нет.

По сути дела, все объекты в программе на Прологе представляются именно в виде термов.

Если терм не содержит переменных, то он называется основным или константным термом.

Атомная или элементарная формула получается путем применения предиката к термам, точнее, это выражение p(t1,...,tn), где p — n-местный предикатный символ, а t1,...,tn — термы.

Формулы логики первого порядка получаются следующим образом:

1. всякая атомная формула есть формула;
2. если A и B — формулы, а x — переменная, то выражения ¬A (читается «не A» или «отрицание A»), A ∧ B (читается «A и B»), A ∨ B (читается «A или B»), A → B (читается «A влечет B»), ∃хA (читается «для некоторого x» или «существует x») и ∀xA (читается «для любого x» или «для всякого x»)– формулы;
3. других формул нет.

В случае если формула имеет вид ∀xA или ∃хA, ее подформула A называется областью действия квантора ∀x или ∃х соответственно. Если вхождение переменной x в формулу находится в области действия квантора ∀ x или ∃х, то оно называется связанным вхождением. В противном случае вхождение переменной в формулу называется свободным.

Чтобы не увеличивать чрезмерно объем лекции, мы не будем рассматривать полный список аксиом и правил вывода логики первого порядка.Те из них, которые пригодятся нам в дальнейшем, будут приведены в соответствующих местах.

Литералом будем называть атомную формулу или отрицание атомной формулы. Атом называется положительным литералом, а его отрицание — отрицательным литералом.

Дизъюнкт — это дизъюнкция конечного числа литералов. Если дизъюнкт не содержит литералов, его называют пустым дизъюнктом и обозначают посредством символа ?.

Содержание  Назад  Вперед