Лекция из курса Основы программирования на языке Пролог - часть 2
Если предикатный (функциональный) символ имеет n аргументов, он называется n-местным предикатным (функциональным) символом.
Термом будем называть выражение, образованное из переменных и констант, возможно, с применением функций, а точнее:
- всякая переменная или константа есть терм;
- если t1,...,tn — термы, а f — n-местный функциональный символ,то f(t1,...,tn) — терм;
- других термов нет.
По сути дела, все объекты в программе на Прологе представляются именно в виде термов.
Если терм не содержит переменных, то он называется основным или константным термом.
Атомная или элементарная формула получается путем применения предиката к термам, точнее, это выражение p(t1,...,tn), где p — n-местный предикатный символ, а t1,...,tn — термы.
Формулы логики первого порядка получаются следующим образом:
- всякая атомная формула есть формула;
- если A и B — формулы, а x — переменная, то выражения ¬A (читается «не A» или «отрицание A»), A ∧ B (читается «A и B»), A ∨ B (читается «A или B»), A → B (читается «A влечет B»), ∃хA (читается «для некоторого x» или «существует x») и ∀xA (читается «для любого x» или «для всякого x»)– формулы;
- других формул нет.
В случае если формула имеет вид ∀xA или ∃хA, ее подформула A называется областью действия квантора ∀x или ∃х соответственно. Если вхождение переменной x в формулу находится в области действия квантора ∀ x или ∃х, то оно называется связанным вхождением. В противном случае вхождение переменной в формулу называется свободным.
Чтобы не увеличивать чрезмерно объем лекции, мы не будем рассматривать полный список аксиом и правил вывода логики первого порядка.Те из них, которые пригодятся нам в дальнейшем, будут приведены в соответствующих местах.
Литералом будем называть атомную формулу или отрицание атомной формулы. Атом называется положительным литералом, а его отрицание — отрицательным литералом.
Дизъюнкт — это дизъюнкция конечного числа литералов. Если дизъюнкт не содержит литералов, его называют пустым дизъюнктом и обозначают посредством символа ?.