Линейная логика: различия между версиями
| [отпатрулированная версия] | [отпатрулированная версия] |
Содержимое удалено Содержимое добавлено
РоманСузи (обсуждение | вклад) Представление в виде исчисления секвенций |
РоманСузи (обсуждение | вклад) →Представление в виде исчисления секвенций: дополнение |
||
Строка 100:
== Представление в виде исчисления секвенций ==
Один из способов определения линейной логики — это [[исчисление секвенций]]. Буквы Γ и ∆ обозначают списки предложений <math>A_1, ..., A_n</math>, и называются '''''контекстами'''''. В
Структурное правило — перестановка. Задано соответственно левое и правое правила вывода:
<math>\cfrac{\Gamma, A, B, \Gamma' \vdash \Delta}{\Gamma, B, A, \Gamma' \vdash \Delta}\; \text{exL}\qquad \cfrac{\Gamma \vdash \Delta, A, B, \Delta'}{\Gamma \vdash \Delta, B, A, \Delta'}\; \text{exR}</math>
Тождество и [[Сечение (теория доказательств)|сечение]]:
<math>\cfrac{\ }{A \vdash A}\; \text{I}\qquad \cfrac{\Gamma \vdash \Sigma, A, \Delta \qquad \Gamma', A, \Sigma' \vdash \Delta'}{\Gamma, \Gamma', \Sigma' \vdash \Sigma, \Delta, \Delta'}\; \text{Cut}</math>
{{заготовка раздела}}
| |||