Сосредоточенное доказательство - Focused proof

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

Говорят, что последовательное исчисление обладает свойством фокусировки, когда сфокусированные доказательства завершены для некоторого завершающего условия. За Система LK, Система ЖЖ, и Система LL, единообразные доказательства - это сфокусированные доказательства, в которых всем атомам приписана отрицательная полярность.^[2] Было показано, что многие другие секвенциальные исчисления обладают свойством фокусировки, особенно вложенные последовательные исчисления как классических, так и интуиционистских вариантов модальной логики в S5 куб.^[3][4]

Единые доказательства

В последовательном исчислении для интуиционистский По логике, единообразные доказательства можно охарактеризовать как те, в которых восходящее чтение выполняет все правые правила перед левыми. Как правило, единообразные доказательства не являются полными для логики, т. Е. Не все последовательности или формулы допускают единообразное доказательство, поэтому рассматриваются фрагменты там, где они полны, например, потомственный Харроп фрагмент Интуиционистский логика. Из-за детерминированного поведения в качестве механизма контроля, определяющего язык программирования парадигма логическое программирование.^[1] Иногда единый поиск корректуры реализуется в варианте исчисления последовательностей для данной логики, где управление контекстом осуществляется автоматически, тем самым увеличивая фрагмент, для которого можно определить язык логического программирования.^[5]

Сфокусированные доказательства

Первоначально принцип фокусировки был классифицирован посредством различия между синхронной и асинхронной связкой в Линейная логика то есть связующие, которые взаимодействуют с контекстом, и те, которые не взаимодействуют, как следствие исследования логическое программирование. Сейчас они становятся все более важным примером контроля над редуктивная логика, и может значительно улучшить процедуры поиска доказательств в промышленности. Основная идея фокусировки состоит в том, чтобы идентифицировать и объединить недетерминированные выборы в доказательстве, чтобы доказательство можно было рассматривать как чередование отрицательных фаз (где с энтузиазмом применяются обратимые правила) и положительных фаз (где приложения других правила ограничены и контролируются).^[3]

Поляризация

Согласно правилам исчисления секвенций формулы канонически помещаются в один из двух классов, называемых положительный и отрицательный например, в LK и LJ формула ${\displaystyle \phi \lor \psi }$ положительный. Единственная свобода - над атомами, которым свободно назначается полярность. Для отрицательных формул доказуемость инвариантна при применении правила права; и, соответственно, доказуемость положительной формулы инвариантна относительно применения левого правила. В любом случае можно безопасно применять правила в любом порядке к наследственным подформулам той же полярности.

В случае применения правила правого к положительной формуле или правила левого правила к отрицательной формуле могут возникнуть недопустимые последовательности, например, в LK и LJ нет доказательства секвенции ${\displaystyle B\lor A\implies A\lor B}$ начиная с правильного правила. Исчисление допускает принцип фокусировки если когда исходный редукт был доказуем, то наследственные редукты той же полярности также доказуемы. То есть можно взять на себя обязательство сосредоточиться на разложении формулы и ее подформул одной полярности без потери полноты.

Сфокусированная система

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

Позволять ${\displaystyle \uparrow }$ и ${\displaystyle \downarrow }$ обозначают изменение полярности, причем первые делают формулу отрицательной, а вторые - положительной; и назовите формулу нейтральной стрелкой. Напомним, что ${\displaystyle \lor }$ положительна, и рассмотрим нейтральную поляризованную секвенцию ${\displaystyle \downarrow \uparrow \phi \lor \psi \implies \uparrow \phi \lor \psi }$, который интерпретируется как фактическая секвенция ${\displaystyle \phi \lor \psi \implies \phi \lor \psi }$. Для таких нейтральных секвенций сфокусированная система вынуждает делать явный выбор, на какой формуле сосредоточиться, что обозначается ${\displaystyle \langle \,\rangle }$. Для выполнения поиска лучше всего выбрать левую формулу, так как ${\displaystyle \lor }$ положительно, действительно (как обсуждалось выше) в некоторых случаях нет доказательств, когда акцент делается на правильной формуле. Чтобы преодолеть это, некоторые целенаправленные исчисления создают точку возврата, так что фокусировка на правильном дает ${\displaystyle \downarrow \uparrow \phi \lor \psi \implies \langle \phi \lor \psi \rangle ,\uparrow \phi \lor \psi }$, который по-прежнему ${\displaystyle \phi \lor \psi \implies \phi \lor \psi }$. Вторая формула справа может быть удалена только после того, как сфокусированная фаза завершится, но если поиск по проверке застрянет до того, как это произойдет, секвенция может удалить сфокусированный компонент, тем самым вернувшись к выбору, например, ${\displaystyle \downarrow \uparrow B\lor A\implies \langle A\rangle ,\uparrow A\lor B}$ должен быть доставлен в ${\displaystyle \downarrow \uparrow B\lor A\implies \uparrow A\lor B}$ поскольку никакой другой редуктивный вывод сделать нельзя. Это псевдосокращение, поскольку оно имеет синтаксическую форму сокращения справа, но фактической формулы не существует, то есть в интерпретации доказательства в сфокусированной системе секвенция имеет только одну формулу справа.

Рекомендации

1. Миллер, Дейл; Надатур, Гопалан; Пфеннинг, Франк; Щедров, Андре (1991-03-14). «Единые доказательства как основа для логического программирования». Анналы чистой и прикладной логики. 51 (1): 125–157. Дои:10.1016 / 0168-0072 (91) 90068-В. ISSN  0168-0072.
2. Лян, Чак; Миллер, Дейл (2009-11-01). «Фокусировка и поляризация в линейной, интуиционистской и классической логике». Теоретическая информатика. Абстрактная интерпретация и логическое программирование: в честь профессора Джорджо Леви. 410 (46): 4747–4768. Дои:10.1016 / j.tcs.2009.07.041. ISSN  0304-3975.
3. Чаудхури, Каустув; Марин, Соня; Штрасбургер, Лутц (2016), Якобс, Барт; Лёдинг, Кристоф (ред.), «Сфокусированные и синтетические вложенные последовательности», Основы программной науки и вычислительных структур, Берлин, Гейдельберг: Springer Berlin Heidelberg, 9634, стр. 390–407, Дои:10.1007/978-3-662-49630-5_23, ISBN  978-3-662-49629-9
4. Чаудхури, Каустув; Марин, Соня; Штрасбургер, Лутц (2016). "Модульные ориентированные системы доказательства для интуиционистской модальной логики". Марк Хербстритт: 18 страниц. Дои:10.4230 / LIPICS.FSCD.2016.16.
5. Армелин, Пабло А .; Пим, Дэвид Дж. (2001), «Групповое логическое программирование», Автоматическое мышление, Берлин, Гейдельберг: Springer Berlin Heidelberg, стр. 289–304, Дои:10.1007/3-540-45744-5_21, ISBN  978-3-540-42254-9