Целенаправленное доказательство

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

Говорят, что секвенциальное исчисление обладает свойством фокусировки, когда сфокусированные доказательства завершены для некоторого завершающего условия. Для Системы LK , Системы LJ и Системы LL унифицированные доказательства — это целенаправленные доказательства, в которых всем атомам присвоена отрицательная полярность. Было показано, что многие другие секвенциальные исчисления обладают свойством фокусировки, особенно вложенные секвенциальные исчисления как классического, так и интуиционистского вариантов модальной логики в кубе S5 .

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

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

Целенаправленные доказательства

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

поляризация

По правилам секвенциального исчисления формулы канонически относят к одному из двух классов, называемых положительными и отрицательными , например, в ЛК и ЖЖ формула $\phi \lor \psi$ является положительным. Единственная свобода распространяется на атомы, которым свободно присваивается полярность. Для отрицательных формул доказуемость инвариантна при применении правила правильного; и, двойственно, для положительных формул доказуемость инвариантна относительно применения левого правила. В любом случае можно безопасно применять правила в любом порядке к наследственным подформулам одной и той же полярности.

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

Целенаправленная система

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

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