2015-04-12
242
Равенство является атомом особого типа Терм = Терм или =(Терм, Терм). Равенство означает, что оба терма в атоме соответствуют одному и тому же объекту. Не следует путать предикат равенства с операцией присваивания. В следующей таблице раскрыт смысл равенства для различных термов, где X, Y обозначают константы, x, y – переменные, а F(x) – функция:
| X = Y | Истинно, если константы именуют один и тот же объект |
| x = Y | Истинно, если значение переменной равно константе |
| x = y | Истинно, если значения переменных совпадают |
| X = F(Y) | Истинно, если значение функции совпадает с константой |
| X = F(y) | |
| x = F(Y) | Истинно, если значение функции совпадает со значением переменной |
| x = F(y) |
Аксиомы, теоремы, факты и цели
В логике высказываний были введены понятия интерпретация, общезначимость, модель и выводимость. Аналогичные понятия есть и в логике предикатов. Аксиомами называют такие формулы, для которых среда является моделью при всех интерпретациях, или формулы, которые истинны при любых значениях входящих в них переменных. Аксиомы, являющиеся литералами (атомы с отрицанием или без), все аргументы которых константы, называют фактами. Аксиомы не являющиеся фактами называют правилами. Основная задача в логике предикатов – вывод на основании истинных фактов и правил целевых формул, называемых теоремами.
