Преобразование логики первого порядка в CNF без экспоненциального увеличения

Question

При попытке решить логические задачи на компьютере обычно сначала конвертируют их в CNF, потому что лучшие алгоритмы решения ожидают ввода CNF.

Для логики высказываний правила учебника для этого преобразованияпросто, но если вы примените их как есть, результатом будет один из очень редких случаев, когда программа сталкивается с double экспоненциальным потреблением ресурсов, не будучи специально созданным для этого:

a <=> (b <=> (c <=> ...))

с N переменными генерирует 2 ^ 2 ^ N предложений, одно экспоненциальное увеличение при преобразовании эквивалентности в AND / OR, а другое при распределении OR в AND.

Решение этой проблемы состоит в переименовании подтерминов.Если мы переписаем вышеприведенное как что-то вроде

r <=> (c <=> ...)
a <=> (b <=> r)

, где r - это свежий символ, который определен равным подтерму - в общем, нам может понадобиться O (N) таких символов -экспоненциальных взрывов можно избежать.

К сожалению, это сталкивается с проблемой, когда мы пытаемся расширить ее до логики первого порядка.Используя нотацию TPTP, где ? означает «существует», а переменные начинаются с заглавных букв, рассмотрим

a <=> ?[X]:p(X)

По общему признанию, этот случай достаточно прост, так что нет реальной необходимости переименовывать подтерм, но необходимоиспользуйте простой случай для иллюстрации, поэтому предположим, что мы используем алгоритм, который просто автоматически переименовывает аргументы оператора эквивалентности;эта точка обобщается на более сложные случаи.

Если мы попробуем описанный выше трюк и переименуем подтерм ?, мы получим

r <=> ?[X]:p(X)

Экзистенциальные переменные преобразуются в символы Сколема, поэтомукак

r <=> p(s)

Исходная формула затем расширяется до

(~a | r) & (a | ~r)

, что по построению эквивалентно

(~a | p(s)) & (a | ~p(s))

Но это не правильно!Предположим, что мы не сделали переименование, а просто расширили первоначальную формулу, как было, мы получили бы

(~a | ?[X]:p(X)) & (a | ~?[X]:p(X))
(~a | ?[X]:p(X)) & (a | ![X]:~p(X))
(~a | p(s)) & (a | ~p(X))

, что критически отличается от версии, которую мы получили с переименованием.

проблема в том, что эквивалентность требует как положительной, так и отрицательной версий каждого аргумента, но применение отрицания к терминам, которые содержат универсальные или экзистенциальные кванторы, структурно изменяет эти термины;вы не можете просто инкапсулировать их в определение, а затем применить отрицание к определенному символу.

В результате этого, когда у вас есть эквивалентность, а аргументы могут содержать такие квантификаторы, вам действительно нужно повторяться через каждый аргументдважды, один раз для положительной версии, один раз для отрицательной.Этого достаточно, чтобы вернуть экзистенциальный взрыв, которого мы надеялись избежать путем переименования.Насколько я понимаю, эта проблема не связана с тем, как работает конкретный алгоритм, а с характером задачи.

Итак, мой вопрос:

Учитывая входную формулу, которая можетсодержат произвольную вложенность эквивалентности и квантификаторов, есть ли какой-нибудь алгоритм, который будет корректно превращать это в CNF с полиномиальным, а не экспоненциальным числом предложений?

Answer 1

Как вы заметили, экзистенциал, такой как pXp (X), равен , а не , фактически эквивалентен сколомизированному выражению p (S).Его отрицание ¬∃Xp (X) не эквивалентно ¬p (S), но ∀Y.¬p (Y).

Возможные подходы, позволяющие избежать экспоненциального увеличения:

• Преобразуйте экзистенциалы, такие как pXp (X), в универсалии, такие как ¬Yp (Y), или наоборот, чтобы у вас была каноническая форма.Сколемизируйте на более позднем этапе.
• Помните, когда вы конвертируете, что ваш p ​​(S) - это сколемизированный экзистенциал, а его отрицание равно ∀Y.¬p (Y).
• Определение терминов, эквивалентныхдля универсалий и экзистенциалов, таких, что a представляет ∀Yp (Y), а ¬a затем представляет ¬Yp (Y), или, что то же самое, ∃X.¬p (X).
• Используйте симметрию булевых дуалов, так что те же преобразования применяются при замене AND и OR, законов Де Моргана и эквивалентности между экзистенциалами и отрицательными универсалиями, чтобы восстановить симметрию между разложениями r и ~ r.Отрицания в преобразовании между универсалиями и экзистенциалами и в законах де Моргана нейтрализуют друг друга, а двойственность переключения И и ИЛИ означает, что вы можете повторно использовать результат слева, чтобы снова сгенерировать результат справа механически?

Учитывая, что вам все равно нужно поддерживать операторы ALL и NOT ALL, это не должно создавать никаких новых проблем.Просто канонизируйте и используйте тот же подход, что и для универсального.

Если вы решаете, перейдя на SAT, ваши термины могут также представлять универсалы.Итак, в вашем примере вы пытаетесь заменить a на r, но вы все равно можете использовать ~a, эквивалентный отрицательному универсальному.

В ваших выражениях.вы все равно будете использовать (~a | r) & (a | ~r), но увеличите ~r до правильного, а не неправильного значения.Этот пример тривиален, так как это просто ~a, но вы обычно определяете r как эквивалент более сложного преобразования, и в этом случае вам нужно помнить, что представляют собой r и ~r.На самом деле это не простое механическое преобразование выражения Skolemized.

В этом примере я не уверен, почему проблема в том, что (~a | r) & (a | ~r) эквивалентно (~a | r) & (a | ~a), что упрощает до (~a | r).Это не собирается дать вам экспоненциальный взрыв?Когда вы переводите обратно в логику предикатов первого порядка, сделайте правильный перевод.

Обновление

Спасибо за разъяснение, что проблема была в чате.Как мне кажется, я понимаю, что у вас есть эквивалент с левой и правой сторонами, который содержит другие вложенные эквивалентности, и вы хотите расширить как эквивалентность, так и ее отрицание.Проблема в том, что, поскольку отрицание не имеет симметричной формы, вам нужно дважды повторять за каждую вложенную эквивалентность в дереве, один раз при расширении эквивалентности и один раз при расширении его отрицания?

Вы должны определить преобразованиекоторый генерирует отрицательное расширение из положительного расширения за линейное время и разделяет и завоевывает выражения, содержащие вложенные эквивалентности, используя это.Похоже, это то, что вы сделали после преобразования ~ p (S).

Для этого вы вспомните, что ¬Xp (X) эквивалентно ∀X.¬p (X), и наоборотнаоборот.Затем, если вы расширили p (x) до нормальной формы в виде союзов и дизъюнкций, законы де Моргана позволяют превратить выражение типа ¬ (a ∨ ¬b) в ¬a ∧ b.Внутреннее преобразование квантификатора и внешнее преобразование Де Моргана нейтрализуют друг друга.Наконец, двойственное значение любой булевой эквивалентности остается в силе, когда вы заменяете каждый ∨ и ∧ на другой, а любой атом a или ¬а на его инверсию.

Итак, пока я могу делать ошибку, особенно в 1AM, мне кажется, что вам нужно двойственное преобразование, которое заменяет:

• внешнее ∃ для ∀ и наоборот
• ∧ для ∨ и наоборот
• Каждый член t с ¬t и наоборот

Примените это к расширению положительной эквивалентности для генерацииотрицательный двойной по времени, пропорциональный его длине, без дальнейшей рекурсии.