Удовлетворенность

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

В математической логике , выполнимость и действительность являются элементарными понятиями семантики . Формула является выполнимой , если это возможно , чтобы найти интерпретацию ( модель ) , что делает формулу верно. ^[1] Формула действительна, если все интерпретации делают ее верной. Противоположностями этих концепций являются неудовлетворительность и недействительность , то есть формула неудовлетворительна, если ни одна из интерпретаций не делает ее истинной и недействительнойесли такая интерпретация делает формулу ложной. Эти четыре понятия связаны друг с другом точно так же, как и квадрат оппозиции Аристотеля .

Четыре концепции могут быть применены ко всем теориям : теория является выполнимой (действительной), если одна (все) интерпретации делают каждую из аксиом теории истинной, и теория неудовлетворительна (недействительна), если все (одна) интерпретация делает ложной каждую из аксиом теории.

Также возможно рассматривать только те интерпретации, которые делают все аксиомы второй теории истинными. Это обобщение обычно называют выполнимостью по модулю теорий .

Вопрос о том, выполнимо ли предложение в логике высказываний, является разрешимой проблемой . В общем, вопрос о том, являются ли предложения в логике первого порядка выполнимыми, не разрешим. В универсальной алгебре и эквациональной теории методы переписывания терминов , замыкания конгруэнций и объединения используются, чтобы попытаться решить выполнимость. Решимость конкретной теории зависит от того, является ли теория свободной от переменных или от других условий. ^[2]

Снижение действительности до выполнимости [ править ]

Для классической логики , как правило, можно переформулировать вопрос о действительности формулы в формулу, предполагающую выполнимость, из-за отношений между концепциями, выраженными в приведенном выше квадрате оппозиции. В частности, φ действителен тогда и только тогда, когда ¬φ невыполнимо, то есть неверно, что ¬φ выполнимо. Другими словами, φ выполнимо тогда и только тогда, когда ¬φ неверно.

Для логики без отрицания, такой как положительное исчисление высказываний , вопросы валидности и выполнимости могут быть не связаны. В случае положительного исчисления высказываний проблема выполнимости тривиальна, поскольку выполнима каждая формула, в то время как проблема достоверности является ко-NP полной .

Пропозициональная выполнимость [ править ]

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

Выполнимость в логике первого порядка [ править ]

Выполнимость неразрешима, и на самом деле это даже не полуразрешимое свойство формул в логике первого порядка (FOL). ^[3] Этот факт связан с неразрешимостью проблемы валидности FOL. Вопрос о статусе проблемы действительности был впервые поставлен Дэвидом Гильбертом как так называемая Entscheidungsproblem . Универсальная справедливость формулы - это полуразрешимая проблема. Если бы выполнимость была также полуразрешимой проблемой, то проблема существования контрмоделей была бы такой же (формула имеет контрмодели, если и только если ее отрицание выполнимо). Таким образом, проблема логической достоверности была бы разрешимой, что противоречит теореме Чёрча – Тьюринга., результат отрицательного ответа на проблему Entscheidungsproblem.

Выполнимость в теории моделей [ править ]

В модельной теории , атомная формула выполнима , если существует совокупность элементов структуры , которые делают формулу верно. ^[4] Если A - структура, φ - формула, а a - набор элементов, взятых из структуры, которые удовлетворяют φ, то обычно пишут, что

A ⊧ φ [a]

Если φ не имеет свободных переменных, то есть если φ является атомарным предложением , и ему удовлетворяет A , то пишут

А ⊧ φ

В этом случае можно также сказать , что является моделью для ф, или , что φ является истинным в A . Если T - это набор элементарных предложений (теория), удовлетворяющий A , мы пишем

А ⊧ Т

Конечная выполнимость [ править ]

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

Тем не менее конечная выполнимость и выполнимость в общем случае не обязательно должны совпадать. Например, рассмотрим логическую формулу первого порядка, полученную как соединение следующих предложений, где и - константы : ${\ displaystyle a}$ ${\ displaystyle b}$

${\ Displaystyle R (а_ {0}, а_ {0})}$
${\ Displaystyle R (а_ {0}, а_ {1})}$
$\forall xy(R(x,y)\rightarrow \exists zR(y,z))$
$\forall xyz(R(y,x)\wedge R(z,x)\rightarrow x=z))$

Полученная формула имеет бесконечную модель , но можно показать, что у нее нет конечной модели (начиная с факта и следуя цепочке атомов, которая должна существовать в соответствии с третьей аксиомой, конечность модели потребует существования цикла , что нарушит четвертую аксиому, независимо от того, повторяется ли он на другом элементе или на другом). $R(a_{0},a_{0}),R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ $R(a,b)$ $R$ $a_{0}$

Вычислительная сложность принятия решения о выполнимости для ввода формулы в данной логике может отличаться от принятия решения о конечной выполнимости; на самом деле для некоторых логик разрешима только одна из них .

Числовые ограничения [ править ]

Числовые ограничения часто возникают в области математической оптимизации , где обычно требуется максимизировать (или минимизировать) целевую функцию с некоторыми ограничениями. Однако, если оставить в стороне целевую функцию, основная проблема простого решения, являются ли ограничения выполнимыми, может быть сложной или неразрешимой в некоторых условиях. В следующей таблице приведены основные случаи.

Ограничения	над реалами	над целыми числами
Линейный	PTIME (см. Линейное программирование )	NP-полный (см. Целочисленное программирование )
Нелинейный	разрешимый	неразрешимая ( десятая проблема Гильберта )

Источник таблицы: Bockmayr and Weispfenning . ^[5]^{: 754}

Для линейных ограничений более полная картина представлена в следующей таблице.

Ограничения по:	рациональные	целые числа	натуральные числа
Линейные уравнения	PTIME	PTIME	НП-полный
Линейные неравенства	PTIME	НП-полный	НП-полный

Источник таблицы: Bockmayr and Weispfenning . ^[5]^{: 755}

См. Также [ править ]

2-выполнимость
Проблема логической выполнимости
Выполнимость схемы
21 NP-полная задача Карпа
Срок действия
Удовлетворение ограничений
Удовлетворительный

Заметки [ править ]

^ См, например, Boolos и Джеффри, 1974, глава 11.
^ Франц Баадер ; Тобиас Нипков (1998). Перезапись терминов и все такое . Издательство Кембриджского университета. С. 58–92. ISBN 0-521-77920-0.
^ Байера, Кристель (2012). «Глава 1.3 Неразрешимость ВОЛС» (PDF) . Конспект лекции - Продвинутая логика . Technische Universität Dresden - Институт технических компьютерных наук. С. 28–32 . Проверено 21 июля 2012 года . ^{[ мертвая ссылка ]}
^ Wilifrid Ходжес (1997). Более короткая модельная теория . Издательство Кембриджского университета. п. 12. ISBN 0-521-58713-1.
^ a b Александр Бокмайер; Фолькер Вайспфеннинг (2001). «Решение числовых ограничений». В Джоне Алане Робинсоне; Андрей Воронков (ред.). Справочник Automated Reasoning Том I . Elsevier и MIT Press. ISBN 0-444-82949-0. (Elsevier) (MIT Press).

Ссылки [ править ]

Булос и Джеффри, 1974. Вычислимость и логика . Издательство Кембриджского университета.

Дальнейшее чтение [ править ]

Даниэль Кренинг ; Офер Стрихман (2008). Процедуры принятия решений: алгоритмическая точка зрения . Springer Science & Business Media. ISBN 978-3-540-74104-6.
А. Биер; M. Heule; Х. ван Маарен; Т. Уолш, ред. (2009). Справочник по выполнимости . IOS Press. ISBN 978-1-60750-376-7.

[1] См, например, Boolos и Джеффри, 1974, глава 11.

[2] Франц Баадер ; Тобиас Нипков (1998). Перезапись терминов и все такое . Издательство Кембриджского университета. С. 58–92. ISBN 0-521-77920-0.

[3] Байера, Кристель (2012). «Глава 1.3 Неразрешимость ВОЛС» (PDF) . Конспект лекции - Продвинутая логика . Technische Universität Dresden - Институт технических компьютерных наук. С. 28–32 . Проверено 21 июля 2012 года . ^{[ мертвая ссылка ]}

[4] Wilifrid Ходжес (1997). Более короткая модельная теория . Издательство Кембриджского университета. п. 12. ISBN 0-521-58713-1.

[BockmayrWeispfenning2001-5] Александр Бокмайер; Фолькер Вайспфеннинг (2001). «Решение числовых ограничений». В Джоне Алане Робинсоне; Андрей Воронков (ред.). Справочник Automated Reasoning Том I . Elsevier и MIT Press. ISBN 0-444-82949-0. (Elsevier) (MIT Press).

[1]