В математической логике , выполнимость и действительность являются элементарными понятиями семантики . Формула является выполнимой , если это возможно , чтобы найти интерпретацию ( модель ) , что делает формулу верно. [1] Формула действительна, если все интерпретации делают ее верной. Противоположностями этих концепций являются неудовлетворительность и недействительность , то есть формула неудовлетворительна, если ни одна из интерпретаций не делает формулу истинной и недействительной.если такая интерпретация делает формулу ложной. Эти четыре понятия связаны друг с другом точно так же, как и квадрат оппозиции Аристотеля .
Четыре концепции могут быть применены ко всем теориям : теория является выполнимой (действительной), если одна (все) интерпретации делают каждую из аксиом теории истинной, и теория неудовлетворительна (недействительна), если все (одна) интерпретация делает одну из аксиом теории ложной.
Также возможно рассматривать только те интерпретации, которые делают все аксиомы второй теории истинными. Это обобщение обычно называют выполнимостью по модулю теорий .
Вопрос о том, выполнимо ли предложение в логике высказываний, является разрешимой проблемой . В общем, вопрос о том, являются ли предложения в логике первого порядка выполнимыми, не разрешим. В универсальной алгебре и эквациональной теории методы переписывания терминов , замыкания конгруэнций и объединения используются, чтобы попытаться решить выполнимость. Решимость конкретной теории зависит от того, является ли теория свободной от переменных или от других условий. [2]
Снижение действительности до выполнимости
Для классической логики , как правило, возможно переформулировать вопрос о действительности формулы в формулу, предполагающую выполнимость, из-за отношений между концепциями, выраженными в приведенном выше квадрате оппозиции. В частности, φ действителен тогда и только тогда, когда ¬φ невыполнимо, то есть неверно, что ¬φ выполнимо. Другими словами, φ выполнимо тогда и только тогда, когда ¬φ неверно.
Для логики без отрицания, такой как положительное исчисление высказываний , вопросы валидности и выполнимости могут быть не связаны. В случае положительного исчисления высказываний проблема выполнимости тривиальна, поскольку выполнима каждая формула, в то время как проблема достоверности является ко-NP полной .
Пропозициональная выполнимость
В случае классической логики высказываний выполнимость для пропозициональных формул разрешима. В частности, выполнимость - это NP-полная проблема, и это одна из наиболее интенсивно изучаемых проблем в теории сложности вычислений .
Выполнимость в логике первого порядка
Выполнимость неразрешима, и на самом деле это даже не полуразрешимое свойство формул в логике первого порядка (FOL). [3] Этот факт связан с неразрешимостью проблемы валидности FOL. Вопрос о статусе проблемы действительности был впервые поставлен Дэвидом Гильбертом как так называемая Entscheidungsproblem . Универсальная справедливость формулы - это полуразрешимая проблема. Если бы выполнимость была также полуразрешимой проблемой, то проблема существования контрмоделей была бы такой же (формула имеет контрмодели, если и только если ее отрицание выполнимо). Таким образом, проблема логической достоверности была бы разрешимой, что противоречит теореме Чёрча – Тьюринга , в результате которой формулируется отрицательный ответ на проблему Entscheidungs.
Выполнимость в теории моделей
В модельной теории , атомная формула выполнима , если существует совокупность элементов структуры , которые делают формулу верно. [4] Если A - структура, φ - формула, а a - набор элементов, взятых из структуры, которые удовлетворяют φ, то обычно пишут, что
- A ⊧ φ [a]
Если φ не имеет свободных переменных, то есть если φ является атомарным предложением , и ему удовлетворяет A , то пишут
- А ⊧ φ
В этом случае можно также сказать , что является моделью для ф, или , что φ является истинным в A . Если T - это набор элементарных предложений (теория), удовлетворяющий A , мы пишем
- А ⊧ Т
Конечная выполнимость
Проблема, связанная с выполнимостью, - это проблема конечной выполнимости , то есть вопрос о том, допускает ли формула конечную модель, которая делает ее истинной. Для логики, обладающей свойством конечной модели , проблемы выполнимости и конечной выполнимости совпадают, поскольку формула этой логики имеет модель тогда и только тогда, когда она имеет конечную модель. Этот вопрос важен в математической области теории конечных моделей .
Тем не менее конечная выполнимость и выполнимость в общем случае не обязательно должны совпадать. Например, рассмотрим логическую формулу первого порядка, полученную как соединение следующих предложений, где а также являются константами :
Полученная формула имеет бесконечную модель , но можно показать, что у него нет конечной модели (начиная с факта и следуя цепочке атомов, которые должны существовать в соответствии с третьей аксиомой, конечность модели потребовала бы существования петли, что нарушило бы четвертую аксиому, независимо от того, повторяется ли она на или на другом элементе).
Вычислительная сложность принятия решения о выполнимости для ввода формулы в данной логике может отличаться от принятия решения о конечной выполнимости; на самом деле для некоторых логик разрешима только одна из них .
Числовые ограничения
Числовые ограничения часто возникают в области математической оптимизации , где обычно требуется максимизировать (или минимизировать) целевую функцию с некоторыми ограничениями. Однако, если оставить в стороне целевую функцию, основная проблема простого решения, являются ли ограничения выполнимыми, может быть сложной или неразрешимой в некоторых условиях. В следующей таблице приведены основные случаи.
Ограничения | над реалами | над целыми числами |
---|---|---|
Линейный | 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 года . CS1 maint: обескураженный параметр ( ссылка )[ мертвая ссылка ]
- ^ Вилифрид Ходжес (1997). Более короткая модельная теория . Издательство Кембриджского университета. п. 12. ISBN 0-521-58713-1.
- ^ а б Александр Бокмайр; Фолькер Вайспфеннинг (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.