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

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

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

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

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

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

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

Поляризация

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

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

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

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

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

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