Предваренная нормальная формула (ПНФ)

Предваренной (или пренексной) формулой называется формула вида

j: Q₁(x₁)Q₂(x₂)…Q_n(x_n) s,

где Q_iÎ{", $} кванторы, s - формула без кванторов. Выражение (Q₁(x₁)Q₂(x₂)…Q_n(x_n)) называется префиксом формулы j, а s - матрицей предваренной нормальной формы, если она находится в конъюнктивной нормальной форме (КНФ). Таким образом, в предваренной формуле все кванторы находятся в начале формулы. Бескванторная формула также считается предваренной.

Теорема о предваренной форме. Для всякой формулы А существует предваренная формула В и А~В (А равносильна В).

Процедура приведения произвольной формулы логики предикатов к предваренной нормальной форме включает следующие шаги:

Преобразование формул, устраняющее логические связки ® и «.

Пронесение отрицания вглубь подформул, чтобы отрицания находились только над атомами.

Вынесение кванторов за скобки в порядке их следования в формуле с учетом общезначимых эквивалентностей логики предикатов.

При необходимости переименование связанных переменных в подформулах во избежание коллизии переменных.

Представление полученной бескванторной формулы в КНФ.

Пример приведения формулы логики предикатов к ПНФ.

Следующим шагом является преобразование предложения j в универсальное предложение j*, которое содержит только кванторы общности, находится в предваренной форме и выполнимо тогда и только тогда, когда выполнимо j. Кванторы в префиксе ПНФ должны следовать в том порядке, в каком они встречаются в формуле.

Кванторы можно выносить в разном порядке, так что вид кванторной приставки зависит от способа получения предваренной формы. (?)

Дата добавления: 2014-11-08; просмотров: 1119; Нарушение авторских прав

Мы поможем в написании ваших работ!