Цирковое исчисление
Цирквентное исчисление — это доказательственное исчисление , которое манипулирует графа конструкциями в стиле , называемыми цирквентами , в отличие от традиционных объектов древовидного типа, таких как формулы или секвенции . Цирквенты бывают разных форм, но все они имеют одну общую характерную особенность, отличающую их от более традиционных объектов синтаксических манипуляций. Эта функция заключается в возможности явного учета возможного совместного использования подкомпонентов между различными компонентами. Например, можно написать выражение, в котором два подвыражения F и E , хотя ни одно из них не является подвыражением другого, все же имеют общее вхождение подвыражения G (в отличие от двух разных вхождений G , одного в F и один в E ).
Обзор [ править ]
Подход представил Г. Джапаридзе. [1] как альтернативная теория доказательства, способная «приручить» различные нетривиальные фрагменты его логики вычислимости , которые в противном случае сопротивлялись всем попыткам аксиоматизации в рамках традиционных теоретико-доказательных структур. [2] [3] Происхождение термина «цирквент» — CIRcuit+seQUENT, поскольку простейшая форма циркуляторов, хотя и напоминает схемы , а не формулы, может рассматриваться как совокупность односторонних секвенций (например, секвенций данного уровня Генцена). -дерево доказательства), где некоторые секвенции могут иметь общие элементы.
Базовая версия циркуляторного исчисления [1] сопровождалось « абстрактной семантикой ресурсов » и утверждением, что последняя является адекватной формализацией философии ресурсов, традиционно связанной с линейной логикой . Основываясь на этом утверждении и на том факте, что семантика порождает логику, более сильную, чем (аффинная) линейная логика, Джапаридзе утверждал, что линейная логика является неполной как логика ресурсов. Более того, он утверждал, что не только дедуктивная, но и выразительная сила линейной логики слаба, поскольку она, в отличие от циркуляторного исчисления, не смогла уловить повсеместное явление совместного использования ресурсов. [4]
Ресурсная философия циркулярного исчисления рассматривает подходы линейной логики и классической логики как две крайности: первая вообще не допускает какого-либо совместного использования, а во второй «разделяется все, что можно разделить». Таким образом, в отличие от циркулярного исчисления, ни один из подходов не допускает смешанных случаев, когда некоторые идентичные подформулы являются общими, а некоторые нет.
Среди более поздних применений цирквентного исчисления было его использование для определения семантики чисто пропозициональной логики, дружественной к независимости . [5] Соответствующая логика была аксиоматизирована В. Сюем. [6]
Синтаксически циркуляторные исчисления представляют собой системы глубокого вывода с уникальной особенностью совместного использования подформул. Было показано, что эта функция обеспечивает ускорение некоторых доказательств. Например, полиномиального размера для пропозициональной ячейки. аналитические доказательства были построены [4] только квазиполиномиальные аналитические доказательства. В других системах глубокого вывода для этого принципа были найдены [7] Известно, что в разрешающих или аналитических системах типа Генцена принцип «ячейки» имеет только доказательства экспоненциального размера. [8]
Ссылки [ править ]
- ^ Jump up to: Перейти обратно: а б Г.Джапаридзе, « Введение в циркуляторное исчисление и семантику абстрактных ресурсов ». Журнал логики и вычислений 16 (2006), стр. 489–532.
- ^ Г.Джапаридзе, « Укрощение повторений в вычислимой логике посредством циркуляторного исчисления, Часть I ». Архив математической логики 52 (2013), страницы 173–212.
- ^ Г.Джапаридзе, «Укрощение повторений в вычислимой логике с помощью циркуляторного исчисления, Часть II » Архив математической логики 52 (2013), страницы 213–259.
- ^ Jump up to: Перейти обратно: а б Джапаридзе, Георгий (2008), «Углубление циркуляторного исчисления», Journal of Logic and Computation , 18 (6): 983–1028, arXiv : 0709.1308 , doi : 10.1093/logcom/exn019 , MR 2460926
- ^ Г.Джапаридзе, « От формул к цирквентам в вычислимой логике ». Логические методы в информатике 7 (2011), выпуск 2, статья 1, стр. 1–55.
- ^ Сюй, Вэньян (2014), «Система высказываний, вызванная подходом Джапаридзе к логике ЕСЛИ», Logic Journal of the IGPL , 22 (6): 982–991, arXiv : 1402.4172 , doi : 10.1093/jigpal/jzu020 , MR 3285333
- ^ А. Дас, « О ячейке и связанных с ней принципах в глубоком выводе и монотонных системах ».
- ^ А. Хакен, « Неразрешимость разрешения ». Теоретическая информатика 39 (1985), стр. 297–308.
Дальнейшее чтение [ править ]
- М.Бауэр, « Вычислительная сложность исчисления высказываний ». Логические методы в информатике 11 (2015), выпуск 1, статья 12, стр. 1–16.
- И. Межиров и Н. Верещагин, О семантике абстрактных ресурсов и логике вычислимости . Журнал компьютерных и системных наук 76 (2010), стр. 356–372.
- В.Сюй и С.Лю, « Надежность и полнота системы циркуляторного исчисления CL6 для вычислимой логики ». Логический журнал IGPL 20 (2012), стр. 317–330.
- В.Сюй и С.Лю, « Система циркуляторного исчисления CL8S в сравнении с системой исчисления структур SKSg для логики высказываний ». В: Количественная логика и мягкие вычисления. Гоцзюнь Ван, Бинь Чжао и Юнмин Ли, ред. Сингапур, World Scientific, 2012, стр. 144–149.
- В. Сюй, Система кругового исчисления с кластеризацией и ранжированием . Журнал прикладной логики 16 (2016), стр. 37–49.
Внешние ссылки [ править ]
СМИ, связанные с исчислением Цирквента, на Викискладе?
