Проблема разрешимости в случае конечных областей.
Очевидно, что проблема разрешимости в случае конкретных областей разрешима. В этом случае кванторные операции можно заменить операциями & и и тем самым свести формулу логики предикатов к формуле алгебры логики, для которой проблема разрешимости разрешима.
Пример 1. Формула в области , состоящий из двух элементов, приводится к виду:
Проблема разрешимости для формул, содержащих в предваренной нормальной форме кванторы одного типа.
Определение 1. Формула логики предикатов называется замкнутой, если она не содержит свободных предикатных переменных.
Определение 2. Если формула логики предикатов F содержит свободные переменные , то формула называется замыканием общности формулы F,
формула называется замыканием существования формулы F.
Теорема 1
Если формула логики предикатов, содержащая только одноместные предикатные переменные, выполнима, то она выполнима на конечном множестве, содержащем не более элементов, где n-число различных предикатных переменных, входящих в рассматриваемую формулу.
Следствие
Если замкнутая формула , в которую входят только одноместные предикатные переменные , тождественно истинна на множестве из элементов, то она общезначима.
Решение проблемы для -формул и -формул.
Проблема разрешимости общезначимости для двух типов формул ЛП – - -формул и -формул: => и в этих случаях она сводится к тождественной истинности формул на конечных множествах.
Определение. Под -формулой понимается формула
, (*)
у которой в предваренной нормальной форме кванторная часть содержит только кванторы общности.
Do'stlaringiz bilan baham: |
