Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

Элементарную формулу (атом) или атом с отрицанием называют литерой или литералом в логике предикатов. Литерал считается позитивным, если он не имеет отрицания и негативным, если содержит отрицание. Дизъюнкция литер или одна литера называется элементарной суммой в ло­ гике предикатов. Матрицу предваренной нормальной формы часто представ­ ляют в виде конъюнкции элементарных сумм, и эта конъюнкция называется конъюнктивной нормальной формой (к.н.ф.) в логике предикатов. § 10. Проблема разрешимости логики предикатов Проблема разрешимости логики предикатов состоит в следующем: ука­ зать единый способ (алгоритм), позволяющий для каждой формулы А за конеч­ ное число действий выяснить, является ли А логически общезначимой или нет. Имея такой способ, мы одновременно получим и способ узнавать, будет ли данная формула выполнимой или нет. В самом деле, имея эту возможность, можно вместо заданной формулы А (для которой требуется выяснить выполни­ мость) выяснять будет ли —А логически общезначимой или нет. Если —А логи­ чески общезначима, то А противоречие (логически ложна), следовательно, А невыполнима. Если —А не является логически общезначимой, то А выполнима. В логике высказываний ставилась задача: выяснить для произвольной формулы за конечное число действий является ли она тавтологией или нет. Эта проблема в логике высказываний решалась очень просто, например, с помощью таблиц истинности. В логике предикатов в общем случае проблема разрешения или проблема выполнимости не разрешима. Но проблема имеет решения при некоторых ограничениях. Имеют место следующие теоремы. Теорема 2.10. Проблема разрешимости логики предикатов не имеет решения. Теорема 2.11. Проблема разрешимости логики предикатов имеет решение для формул, содержащих только нульместные или (и) одноместные предикат­ ные буквы. Теорема 2.12. Проблема разрешимости логики предикатов имеет решение для формул, предваренная нормальная форма которых имеет вид: \/xi Vx2 ...VxkByi Зу2 ... Ву„, в, \ J Y Y только Vxi только 3yj где В формула без кванторов. Формула логики предикатов считается чистой, если она не содержит функциональные символы и предметные постоянные (последние можно счи­ тать нуль-аргументными функциональными буквами). Теорема 2.12. Проблема выяснения логически общезначимости формул логики предикатов разрешима для класса чистых формул, которые в предва­ ренной нормальной форме имеют префикс одного из следующих видов: \/Xi VX2 ...VxkByi Зу2 ... Ву„, 50