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