Статья в сборнике "Математические вопросы кибернетики" №1, Москва, 1988
Авторы:Марченков С.С.
О сложности проблемы разрешения для некоторых классов предикатных формул
Аннотация:
Рассматриваются классы A, B замкнутых формул узкого исчисления предикатов (без равенства). Класс A состоит из всех формул, которые содержат лишь одноместные предикатные символы и имеют в предваренной нормальной форме кванторный префикс ∀∃∃; формулы класса B имеют кванторный префикс вида ∀x∃y1∃y2∀z, содержат лишь двуместные предикатные символы и не содержат атомарных формул вида P(z,x), P(z,y1), P(z,y2). Через Sat(A) (соотв. Sat(B)) обозначается множество всех выполнимых формул класса A (класса B), а через DT(T(n)) - класс множеств, распознаваемых одноленточными детерминированными машинами Тьюринга за время T(n). Доказано, что для подходящих констант a>b>1 выполняются соотношения
Sat(A) ∈ DT(an/logn)\DT(bn/logn),
Sat(A) ∈ DT(aan/logn)\DT(bbn/logn).
Ключевые слова:
сложность проблемы разрешения, узкое исчисление предикатов