ПРОБЛЕМА РАЗРЕШЕНИЯ ЛП неразрешима - доказал А.Черч (т.е. установил, что искомый алгоритм не возможен).
Формула логики предикатов называется ВЫПОЛНИМОЙ, если она истинна для некоторой области _О_ и некоторых предикатов, на ней определенных.
Формула логики предикатов называется ТОЖДЕСТВЕННО ИСТИННОЙ ДЛЯ ОБЛАСТИ _О_, если она истинна для данной области _О_ и для всех предикатов, на ней определенных.
Формула логики предикатов называется ТОЖДЕСТВЕННО ИСТИННОЙ или просто истинной, если она истинна для всякой области _О_ и для всяких предикатов.
Формула называется ложной или НЕВЫПОЛНИМОЙ, если ни для какой области ни при каких заменах предикатов не является истинной.