stringtranslate.com

Круговое исчисление

Цирквенты можно рассматривать как коллекции секвенций с возможными общими элементами.

Исчисление Cirquent — это исчисление доказательств , которое манипулирует конструкциями в стиле графа , называемыми cirquent , в отличие от традиционных объектов в стиле дерева, таких как формулы или секвенции . Cirquent бывают разных форм, но все они имеют одну основную характерную черту, отличающую их от более традиционных объектов синтаксической манипуляции. Эта черта — возможность явно учитывать возможное совместное использование подкомпонентов между различными компонентами. Например, можно написать выражение, в котором два подвыражения F и E , хотя ни одно из них не является подвыражением другого, все равно имеют общее вхождение подвыражения G (в отличие от двух разных вхождений G , одного в F и одного в E ).

Обзор

Подход был предложен Г. Джапаридзе [1] как альтернативная теория доказательств, способная «укротить» различные нетривиальные фрагменты его логики вычислимости , которые в противном случае сопротивлялись всем попыткам аксиоматизации в рамках традиционных теоретико-доказательных рамок. [2] [3] Термин «цикл» происходит от CIRcuit+seQUENT, поскольку простейшая форма циклов, хотя и напоминает схемы, а не формулы, может рассматриваться как набор односторонних секвенций (например, секвенций заданного уровня дерева доказательств в стиле Генцена), где некоторые секвенции могут иметь общие элементы.

Циркуент для комбинации ресурсов «два из трех», невыразимый в линейной логике

Базовая версия циклического исчисления [1] сопровождалась « абстрактной семантикой ресурсов » и утверждением, что последняя была адекватной формализацией ресурсной философии, традиционно связанной с линейной логикой . Основываясь на этом утверждении и на том факте, что семантика индуцировала логику, которая была более сильной, чем (аффинная) линейная логика, Джапаридзе утверждал, что линейная логика была неполной как логика ресурсов. Более того, он утверждал, что не только дедуктивная сила, но и выразительная сила линейной логики были слабыми, поскольку она, в отличие от циклического исчисления, не смогла охватить повсеместное явление совместного использования ресурсов. [4]

Линейная логика понимает отображаемую формулу как левый контур, тогда как классическая логика как правый контур

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

Среди более поздних применений исчисления циклов было его использование для определения семантики для чисто пропозициональной независимости-дружественной логики . [5] Соответствующая логика была аксиоматизирована В. Сюем. [6]

Синтаксически, циклические исчисления являются системами глубокого вывода с уникальной особенностью совместного использования подформул. Было показано, что эта особенность обеспечивает ускорение для некоторых доказательств. Например, были построены аналитические доказательства полиномиального размера для пропозиционального ящика. [4] Для этого принципа в других системах глубокого вывода были найдены только квазиполиномиальные аналитические доказательства. [7] Известно, что в системах резолюции или аналитических системах в стиле Генцена принцип ящика имеет только доказательства экспоненциального размера. [8]

Ссылки

  1. ^ ab G.Japaridze, «Введение в исчисление циклов и абстрактную семантику ресурсов». Журнал логики и вычислений 16 (2006), стр. 489–532.
  2. ^ Г.Джапаридзе, «Укрощение рекуррентностей в логике вычислимости посредством циклического исчисления, часть I». Архив журнала «Математическая логика» 52 (2013), страницы 173–212.
  3. ^ Г.Джапаридзе, «Укрощение рекуррентностей в логике вычислимости посредством циклического исчисления, часть II» Архив журнала «Математическая логика» 52 (2013), страницы 213–259.
  4. ^ ab Джапаридзе, Георгий (2008), «Углубление кругового исчисления», Журнал логики и вычислений , 18 (6): 983–1028, arXiv : 0709.1308 , doi : 10.1093/logcom/exn019, MR  2460926
  5. ^ Г.Джапаридзе, «От формул к контурам в логике вычислимости». Логические методы в информатике 7 (2011), выпуск 2, статья 1, стр. 1–55.
  6. ^ Сюй, Вэньян (2014), «Пропозициональная система, индуцированная подходом Джапаридзе к IF-логике», Logic Journal of the IGPL , 22 (6): 982–991, arXiv : 1402.4172 , doi : 10.1093/jigpal/jzu020, MR  3285333
  7. ^ А. Дас, «О принципах классификации и связанных с ними принципах в глубоком выводе и монотонных системах».
  8. ^ А. Хакен, «Неразрешимость разрешения». Теоретическая информатика 39 (1985), стр. 297–308.

Дальнейшее чтение

Внешние ссылки