Intuitionistic BV

Matteo Acclavio

doi:10.1007/978-3-032-06085-3_22

2026-01-01

Matteo Acclavio *

Lutz Straßburger

DOI：10.1007/978-3-032-06085-3_22

原文链接

查看原文

摘要

En 中文

我们提出了一种逻辑IBV，它是BV的一种直觉主义版本，其意义在于其对MLL连接词的限制恰好是IMLL，即MLL的直觉主义版本。对于该逻辑，我们给出了一种深度推理证明系统，并证明了消解规则消除。我们还表明，通过放弃新非交换序列连接词的结合性而得到的IBV逻辑是一种直觉主义变体，即最近引入的逻辑NML的直觉主义变体。对于这种称为INML的逻辑，我们给出了一种无消解规则的序列演算。

Keyword:

SYSTEM