Relating Sequent Calculi for Bi-intuitionistic Propositional Logic
双直觉主义逻辑是直觉主义逻辑的保守推广，具有一个与蕴涵有关的联结对偶。它有时被认为是经典逻辑的一个对称构造子系统。本文比较了双直觉命题逻辑中的三种推理演算：（1）基本标准式推理演算，它将蕴涵右推理和蕴涵左推理的前提分别限制为单结论;（2）Gore等人的嵌套序列演算，其中一个完整的类的削减被封装到特殊的“unnest”规则和（3）削减自由标记的逻辑的Kripke语义派生的演算。我们表明，这些演算可以相互转化，并讨论了不可消除的削减标准风格的微积分。
2011-01-28 cs.LO
A Bi-nested Calculus for Intuitionistic K: Proofs and Countermodels
本文为直觉主义模态逻辑 IK 提出无标签双嵌套矢列演算，支持判定、由失败证明直接构造有限反模型，并可模拟现有嵌套与标签演算。
2025-05-13 cs.LO
Cut-Elimination and Proof Search for Bi-Intuitionistic Tense Logic
我们考虑了双直觉逻辑与时态逻辑Kt的传统模态的扩展。从理论上证明，这种扩展是简单地通过扩展现有的双直觉逻辑的演算与显示逻辑中使用的模态的典型推理规则。事实证明，由此产生的演算LBiKt似乎比文献中考虑的大多数直觉时态或模态逻辑更基本，特别是Ewald和Simpson研究的那些，因为它没有假设菱形和盒子模态算子之间的任何先验关系。我们恢复Ewald的直觉时态逻辑和Simpson的直觉模态逻辑的模块化扩展LBiKt与额外的结构规则。演算LBiKt是以显示演算的一种变体形式来公式化的，使用一种称为嵌套序列的序列形式。切割消除证明LBiKt，使用类似的技术，在显示结石。与显示演算一样，LBiKt的推理规则是“浅”规则，也就是说它们作用于嵌套表达式中的顶级公式。演算LBiKt不适合向后证明搜索，因为存在某些称为“显示假设”的结构规则和任意结构上的压缩规则。我们表明，这些结构规则可以在另一个演算，DBiKt，它使用深度推理，允许一个应用推理规则在任意深度的嵌套的嵌套的。我们证明了LBiKt和DBiKt之间的等价性，并概述了DBiKt的证明搜索策略。我们还给出了一个Kripke语义，并证明了LBiKt是健全的语义，但完整性仍然是一个开放的问题。然后我们讨论LBiKt的各种扩展。
2010-06-29 cs.LO
A cut-free sequent calculus for the bi-intuitionistic logic 2Int
本文的目的是引入一个双直觉的代数演算，并给出其结构规则的可容许性证明。我将介绍的演算，称为SC2Int，是双直觉主义逻辑2Int的一个微积分。这种逻辑的演算代表了一种双边主义的推理，因为它们不仅内化了验证或可证明性的过程，而且内化了证伪或所谓的对偶可证明性方面的对偶过程。2Int的自然演绎演算的一个范式定理已被证明，本文想证明SC 2Int的一个割消定理，即如果成功，这将推广已有的结果.
2020-09-23 cs.LO math.LO
A Proof-Theoretic View of Basic Intuitionistic Conditional Logic (Extended Version)
本文从证明论角度研究基本直觉主义条件逻辑，为IntCK引入嵌套演算、为CCKbox引入矢列演算，并在此基础上定义带might算子的保守扩张CCK，给出其模型类、公理化及若干扩张结果。
2025-07-03 cs.LO
Combining First-Order Classical and Intuitionistic Logic
本文从证明论的角度研究了Humberstone（1979）和del Cerro and Herzig（1996）研究的直觉主义和经典命题逻辑组合C+J的一阶展开。C+J同时具有经典蕴涵和直觉蕴涵，而我们的一阶扩展在C+ J中增加了经典和直觉全称量词以及一个存在量词.本文为我们的一阶直觉逻辑和经典逻辑的结合提供了一个多后继的代数演算G（FOC+J）.我们的正则演算G（FOC+J）将直觉蕴涵和直觉全称量词的正确规则的上下文限制在特定形式的公式中。为了保证子公式的性质，建立了割消定理。作为推论，G（FOC+J）在一阶直觉逻辑和经典逻辑上都是保守的。通过一个典范模型论证证明了G（FOC+J）的强完备性.
2022-04-14 cs.LO
Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)
证明演算是一种类型化的证明演算，它利用证明和反驳概念之间的对偶性为经典命题逻辑提供计算解释。在这项工作中，我们将扩展Euda-Euda，以包括经典的二阶逻辑，通过将参数多态性和存在类型。该系统具有良好的计算性能，如类型保持，汇合，和强规范化，这是建立在通过reductionalargument。我们确定了一个句法限制的证明，其特点正是直观的片段的二阶dupda-dupta，我们研究规范的结果。
2022-10-13 cs.LO
Calculi for Intuitionistic Normal Modal Logic
本文给出了一个按名称调用和一个按值调用的项演算，它们都与直觉模态逻辑IK的盒片段有Curry-Howard对应关系。显示了结石的强归一化性和汇合性。此外，我们还定义了一个从按值调用演算到按名称调用演算的CPS转换，并证明了它的可靠性和完备性。
2016-06-10 cs.LO cs.PL
Normalization by Evaluation for the Lambek Calculus
Lambek的句法演算是直觉非交换线性逻辑乘法片段的演绎系统。作为资源的细粒度演算，它有许多应用，主要是在自然语言的形式化计算研究中。本文给出了逻辑连接词间具有乘法单位和合取的Lambek演算中导子的β-η-长范式演算。归约为范式遵循求值归一化（NbE）策略：（i）在Lambek演算的Kripke模型中求值导出;（ii）从所获得的语义值中提取范式。NbE算法的实现需要在正公式的Kripke解释中存在一个强单子，类似于具有虚假性和析取的直觉命题逻辑的扩展。NbE算法也可以通过对相关子结构逻辑的演算的微小变化来实例化，例如乘法和对偶直觉线性逻辑（MILL和DILL）。
2022-04-14 cs.LO
A new calculus for intuitionistic Strong Löb logic: strong termination and cut-elimination, formalised
本文为直觉主义强Löb逻辑提出新相继式演算，实现强终止的向后搜索与句法消割，并在Coq中形式化验证。
2023-09-01 cs.LO math.LO
An analytic calculus for intuitionistic belief
直觉主义信念已经被阿特莫夫（Artemov）和普罗托波佩斯库（Protopescu）公理化为直觉主义命题逻辑的扩展，通过分配方案K和共反射$A\rightarrow\Box A$。通过这种方式，信念被解释为验证的结果，并且它适合于具有认知模态的直觉主义命题逻辑的扩展的Brouwer-Heyting-Kolmogorov解释。本文研究了直觉信念的自然演绎系统$\mathsf{IEL}^{-}$的结构性质。重点讨论了微积分的解析性，首先证明了正规化定理和子公式性质。从这些，逻辑的可判定性和一致性遵循作为推论。最后，用纯证明论的方法建立了析取性质、$\Box$ -素性和反射规则的可容许性。
2021-06-27 cs.LO math.LO
Intuitionistic Euler-Venn Diagrams (extended)
本文给出了关于Heyting代数的Euler-Venn图的一个直观的解释。与经典的Euler-Venn图相比，我们以不同的方式处理阴影区和缺失区，以具有合取、析取和直观含义的图形表示。我们提出了这种语言的一个无割演算，并证明了它是可靠的和完备的。此外，我们还证明了截割、弱化和收缩规则是可容许的。
2020-02-07 cs.LO
Intuitionistic Monotone Modal Logic: Proof Theory and Semantics
Free University of Bozen-Bolzano（博尔扎诺自由大学）；University of Bern（伯尔尼大学）
研究直觉主义单调模态逻辑IM，通过构造性邻域模型刻画其自然扩展族，提出基于经典单调模态逻辑M的结构演算，证明IM的可判定性，揭示M与K的构造性和直觉主义变体之间的类比。
2026-07-01 cs.LO math.LO
Loop-Checking and Counter-Model Extraction for Intuitionistic Tense Logics via Nested Sequents
Technische Universität Dresden（德累斯顿工业大学）
本文提出一种新的嵌套序列证明搜索方法，用于直觉时序逻辑，支持有限反模型提取。通过引入基于同态的回路检查方法，限制了证明搜索中推导的高度。由于某些推理规则不可逆，算法构建的是称为'计算树'的广义结构，展示了如何从计算树中提取证明和反模型。
2026-03-31 cs.LO
A linear proof language for second-order intuitionistic linear logic
本文提出一种带加法与标量乘法的多态线性λ演算，作为二阶直觉主义线性逻辑的证明语言，并在语法层面证明了线性性结果。
2024-01-25 cs.LO math.LO
Intuitionistic BV (Extended version)
Sussex University（萨塞克斯大学）；INRIA Saclay（法国国家信息与自动化研究所萨克雷中心）
本文提出直觉BV逻辑，其限制在MLL连接词时恰好为IMLL。给出了深层推理证明系统并展示了割消除，同时展示了去掉新非交换序列连接词结合性的逻辑为最近引入的NML逻辑的直觉变体。
2026-04-24 cs.LO
Fixed-point elimination in the Intuitionistic Propositional Calculus (extended version)
Heyting代数（即直觉命题演算的代数模型）上的单调多项式的最小和最大不动点总是存在的，即使这些代数不是完全格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉主义逻辑的$μ$ -演算是平凡的，每个$μ$ -公式等价于一个不动点自由公式。本文给出了公式的最小不动点和最大不动点的公理化，以及计算等价于给定$μ$ -公式的不动点自由公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每一个单调公式通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。我们从算法中提取出这样的n的上界，这取决于公式的大小。对于某些公式，我们证明了这些上界是多项式的和最优的。
2018-03-05 cs.LO math.LO
Curry-Howard-Lambek Correspondence for Intuitionistic Belief
本文介绍了一个自然演绎演算的直觉主义逻辑信念$\mathsf{IEL}^{-}$，它很容易变成一个模态$λ$演算给出了一个计算语义的演绎$\mathsf{IEL}^{-}$。利用这种解释，还证明了$\mathsf{IEL}^{-}$具有良好的证明理论性质。演绎和类型化的条款之间的对应关系，然后扩展到一个类别语义的身份证明$\mathsf{IEL}^{-}$显示这样一个模态的一般结构的信念在直觉框架。
2020-12-15 cs.LO math.LO
An Algebraic Extension of Intuitionistic Linear Logic: The $L_!^S$-Calculus and Its Categorical Model
Université de Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所、洛林研究与信息学院）；Universidad Nacional de Quilmes, DCyT（基尔梅斯国立大学、计算机与信息技术系）；Universidad de Buenos Aires, DC, FCEyN（布宜诺斯艾利斯大学、计算系、经济与理学院）；Universidad de Buenos Aires-CONICET, ICC（布宜诺斯艾利斯大学-阿根廷国家科学研究委员会、计算中心）；Universidad de la República–MEC, PEDECIBA（共和国大学-教育部、PEDECIBA）；Universidad de la República, IMERL, FIng（共和国大学、IMERL、工程学院）
本文提出$L_!^S$-演算作为直觉线性逻辑的证明语言，通过标量乘法和项加法实现线性性的语法表达，并在范畴模型中提供语义解释。
2025-09-22 cs.LO math.CT
Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents
本文利用线性嵌套框架设计了一种新的直觉模糊逻辑--一阶Gödel逻辑的无割演算LNIF。线性嵌套序列-这是嵌套序列限制线性结构-证明是一个很好的证明理论的形式主义直觉模糊逻辑。我们发现，演算LNIF具有非常理想的证明理论的性质，如可逆的所有规则，结构规则的容许性，和句法切割消除。
2020-10-04 cs.LO math.LO
Fixed-point elimination in the intuitionistic propositional calculus
这是现有文献的一个结果，最小和最大的单调多项式的不动点Heyting代数，即直觉命题演算的代数模型总是存在的，即使这些代数是不完整的格。原因是这些极值不动点可由IPC的公式定义。因此，基于直觉逻辑的$μ$ -演算是平凡的，每个$μ$ -公式等价于一个不动点自由公式。本文给出了公式的最小不动点和最大不动点的公理化，以及计算等价于给定$μ$ -公式的无不动点公式的算法。最大不动点的公理化是简单的。最小不动点的公理化比较复杂，特别是每个单调公式都通过Kleene迭代在有限步内收敛到它的最小不动点，但迭代次数没有统一的上界。我们从算法中提取出这样的n的上界，这取决于公式的大小。对于某些公式，我们证明了这些上界是多项式的和最优的。
2016-01-04 cs.LO math.CT math.LO
On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems
本文展示了如何从命题直觉逻辑和一阶直觉逻辑的常量域的标记演算中导出嵌套演算，从而将标记演算的一般结果与嵌套序列的更精细形式联系起来。从标记演算中提取嵌套演算是通过消除标记推导中的结构规则来实现的。提取过程的每个方面都是有动机的和详细的，表明每个嵌套演算从其相关的标记演算继承了有利的证明理论属性。
2020-02-03 cs.LO math.LO
The Vanilla Sequent Calculus is Call-by-Value (Fresh Perspective)
本文证明最小直觉主义逻辑中最基本的相继式演算（香草式）可自然地解释为按值调用求值，通过建立与已知形式主义的互模拟实现。
2024-11-05 cs.LO cs.PL
Taming Complexity in Intuitionistic Modal Logic: The Case of FIK and Its Shallow Calculus
Institute of Computer Science Czech Academy of Sciences（捷克科学院计算机科学研究所）；LIS Aix-Marseille University, CNRS（艾克斯-马赛大学CNRS LIS实验室）
针对直觉主义模态逻辑FIK，提出浅层嵌套矢列演算，通过证明切消可容许性，将判定问题复杂度降至EXPSPACE，显著低于IK的猜想非初等复杂度。
2026-07-01 cs.CC cs.LO
Connectivity at the crossroad of intuitionistic and classical polarizations in linear logic
Université Paris Cité（巴黎西岱大学）；Università Roma Tre（罗马三所大学）；University of Sussex（萨塞克斯大学）
研究扩展线性逻辑证明结构正确性标准的性质，提出对证明结构的几何限制使其成为充分性质，引入VMELL片段，将!演算项翻译为证明网，分解λ演算翻译，证明消去切割模拟!归约并给出!演算项的证明网特征。
2026-07-23 cs.LO
Sequent Calculus in the Topos of Trees
中野的“后来”模态，受到哥德尔-洛布可证明性逻辑的启发，已被应用于类型系统和程序逻辑中，以捕获保护递归。Birkedal等人通过树的拓扑的内部逻辑来模拟这种模态。我们证明了该逻辑的命题片段的语义可以由线性逆良基直觉Kripke框架给出，因此该逻辑是直觉模态逻辑KM和中间逻辑LC的结合。因此，我们称这种逻辑为$\mathrm{KM}_{\mathrm{lin}}$。通过将蕴涵分解为静态蕴涵和非自反蕴涵的策略，给出了$\mathrm{KM}_{\mathrm{lin}}$的一个可靠的无割完备蕴涵演算。我们的演算提供了确定性和终止向后证明搜索，产生的逻辑和其有效性问题的coNP-完全性的可判定性。我们的演算和决策过程可以被限制为降低线性，从而捕获KM。
2015-04-17 cs.LO
Nested Sequents for Intuitionistic Multi-Modal Logics: Cut-Elimination and Lyndon Interpolation
本文提出了一种单结论嵌套序列表演算，用于直觉多模逻辑，并证明了切消性和Lyndon插值性质。
2025-11-27 cs.LO math.LO
Modality Definition Synthesis for Epistemic Intuitionistic Logic via a Theorem Prover
我们推导出一个Prolog定理证明器的直觉主义认知逻辑开始，我们扩展与操作符定义提供嵌入在直觉主义命题逻辑（{ \bf IPC}）的微积分{ \bf G4 IP}。借助一个候选定义公式生成器，我们发现的公理和定理的阿特莫夫和Protopescu的{ \em直觉主义认知逻辑}（{ \bf IEL}）持有和预期的非定理公式失败的认知运营商。我们比较了嵌入{ \bf IEL}在{ \bf IPC}与同样发现成功嵌入Dosen的双重否定模态，判断不足以作为一个认识算子。最后，我们讨论了失败的{ \em必要性规则}，否则成功的{ \bf S4}嵌入和分享我们的想法的直觉解释这些差异的背景下，Brouwer-Heyting-Kolmogorov语义的直觉推理和知识获取的认识和alethic模态。保留字：认知直觉逻辑，命题直觉逻辑，基于Prolog的定理证明器，逻辑系统的自动综合，定义公式生成算法，模态逻辑嵌入直觉逻辑。
2019-09-14 cs.LO
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
本文提出了一种“模态线性逻辑”，它将直觉模态逻辑S4（IS 4）用线性逻辑来表示，建立了从IS 4到它的Girard翻译的S4-版本。它对模态逻辑的扩展是非-这是微不足道的，因为S4模态和指数模态的简单组合导致两种模态之间的不期望的相互作用。为了解决这个问题，我们引入了一个扩展的直觉乘法指数线性逻辑与模态相结合的S4模态和指数模态，并表明它承认从IS 4的声音翻译。通过Curry-Howard对应，我们进一步得到了Pfenning和Davies为分阶段计算所提出的模态微积分的交互几何机器语义。
2019-04-24 cs.LO
Universal Proof Theory: Feasible Admissibility in Intuitionistic Modal Logics
在本文中，我们介绍了一个一般家庭的序列式演算的模态语言及其片段，以捕捉所有建设性的可接受的系统的本质。称这些演算为\emph{constructive}，我们表明，任何足够强的建设性的微积分，满足一个温和的技术条件，可行地承认所有的Visser规则，即，有一种多项式时间算法，它读取维塞尔规则的前提的证明，并为其结论提供证明。作为一个积极的应用，我们证明了Visser规则在直觉模态逻辑的几个演算中的可行容许性，这些演算包括$\mathsf{CK}$，$\mathsf{IK}$及其由模态公理$T$，$B$，$4$，$5$，有界宽度和深度的模态公理以及命题逻辑的扩展。在消极的一面，我们表明，如果一个足够强大的直觉模态逻辑（满足一个温和的技术条件）不承认至少一个Visser的规则，那么它不能有一个建设性的逻辑演算。因此，除了$\mathsf{IPC}$之外，没有中间逻辑具有构造性的构造演算。
2022-10-16 cs.LO math.LO
Admissible Tools in the Kitchen of Intuitionistic Logic
通常将逻辑蕴涵“A蕴涵B”解读为“如果A则B”在直觉主义逻辑中是失败的：存在公式A和B使得“A蕴涵B”是不可证明的，即使B是可证明的，只要A是可证明的。直觉主义规则显然没有捕捉到逻辑的有趣元属性，并且从计算的角度来看，与直觉主义证明相对应的程序不够强大。然而，这种不可证明的影响是可接受的，我们研究他们的行为，通过一个证明项分配和相关规则的减少。我们引入V，一种能够表示可接受的推论的演算，同时通过具有仅仅是直觉术语的范式而保持在直觉世界中。然后，我们扩展直觉逻辑与原则相对应的可接受的规则。作为一个例子，我们考虑Kreisel-Putnam逻辑KP，我们证明了强正规化和析取性质，通过我们的长期分配。这是我们理解直觉逻辑的可接受规则的本质的第一步。
2018-10-17 cs.LO
Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents
本文提出首个针对递增域一阶双直觉逻辑的可靠且完备的多树相继式演算证明系统，通过显式本征变量上下文避免域坍缩并揭示驻留原则与存在谓词的依赖关系。
2024-11-19 cs.LO math.LO
Session Type Systems based on Linear Logic: Classical versus Intuitionistic
会话类型系统已经通过基于直觉和经典线性逻辑的Curry-Howard对应给出了逻辑基础。从这两个逻辑派生的类型系统在同一类的pi演算进程上强制通信正确性，但它们是显著不同的。Caires，Pfenning和Toninho非正式地观察到，与经典类型系统不同，直觉类型系统强制共享通道的局部性，即接收的通道不能用于复制输入。在本文中，我们从形式的角度重新审视这一观察。我们开发了统一线性逻辑（UnitedLinearLogic），一种包含经典线性逻辑和直觉线性逻辑的逻辑。然后，根据Curry-Howard对应的会话类型，我们定义了piectin，一个基于π演算的会话类型系统。使用pixel，我们可以正式评估直觉和经典类型系统之间的差异，并证明局部性和对称性在其中的作用。
2020-04-03 cs.LO cs.PL
Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
本研究提出一种基于无切割嵌套序列演算的纯句法方法，证明含逆模态的经典时态逻辑及其扩展、双直觉主义逻辑的Craig插值性质，创新引入定义插值元对偶的正交性条件，无需语义或嵌入辅助。
2023-06-14 cs.LO math.LO
A Cut-free Sequent Calculus for Basic Intuitionistic Dynamic Topological Logic
针对$\textsf{iK}_d$和$\textsf{iK}_{d*}$这两个动态拓扑逻辑系统，本文提出无切割的G3风格相继式演算，补充了其证明论分析，并证明了析取性质、Visser规则推广及插值性质等关键结果。
2025-02-13 cs.LO math.LO
Nested Sequents for Intuitionistic Grammar Logics via Structural Refinement
Institute of Artificial Intelligence, Technische Universität Dresden（德累斯顿工业大学人工智能研究所）
本文通过结构细化方法，为直觉语法学逻辑构建了无割嵌套序列表演系统，并证明了其保守性、不可判定性和可判定子类。
2025-12-03 cs.DM cs.LO math.LO
A new graphical calculus of proofs
我们提供了一个简单的图形表示的直觉逻辑的证明，这是灵感来自证明网和交互网（两个形式主义起源于线性逻辑）。这种证明的图形演算继承了每一种方法的良好特性，但不受它们的约束。通过Curry-Howard同构，该表示同样适用于λ演算，提供了函数计算的另一种图形表示。
2011-02-14 cs.LO
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
借助一个紧凑的Prolog为基础的定理证明直觉命题逻辑，我们合成的最小假设下，一个给定的公式公式成为一个定理。应用我们的合成算法，以涵盖基本的溯因推理机制后，我们合成的字面量，模仿行的真值表在经典或中间逻辑和我们的条件假设，把经典或中间逻辑的定理，在直觉逻辑。更进一步，我们推广我们的溯因推理机制，合成更有表现力的前置条件，使用最小的一组规范公式，在微积分中的任意公式可以减少，同时保持其可证明性。组织作为一个独立的文学Prolog程序，本文支持其内容的交互式探索，并确保我们的结果完全可复制。
2022-05-11 cs.LO
Polarizing Double Negation Translations
双重否定翻译用于编码和解码直觉逻辑中的经典证明。我们表明，在切自由片段，我们可以简化的翻译，并引入更少的否定。为了实现这一点，我们考虑了公式{}的两极分化，并使这些翻译适应不同的连接词和量词。我们表明，嵌入结果仍然持有，使用定制版本的重点经典的微积分。我们还证明了后者相当于更常见的版本的微积分。这种极化过程允许更轻的嵌入，并揭示了直觉和经典连接词之间的关系。
2013-12-19 cs.LO
Nested Sequents for Intuitionistic Modal Logics via Structural Refinement
我们采用了最近开发的方法-称为“结构细化”-提取嵌套系统的一个相当大的类的直觉模态逻辑从各自的标记的系统。这种方法可以被看作是一种手段，通过它的标记的递归系统可以被转换成嵌套递归系统，通过引入传播规则和消除的结构规则，其次是一个符号的翻译。我们得到的嵌套系统将传播规则，参数化与正式语法，并编码某些帧条件表示为一阶霍恩公式，对应于一个子类的斯科特-莱蒙公理。我们表明，我们的嵌套系统是健全的，切自由完成，并承认惠普的典型结构规则的容许性。
2021-07-05 cs.DM cs.FL cs.LO
Intuitionistic $j$-Do-Calculus in Topos Causal Models
Adobe Research and University of Massachusetts（Adobe研究院和马萨诸塞大学）
该论文将Pearl的do-演算推广到拓扑斯因果模型的直觉主义设置，引入j-do-演算，定义相关稳定性，给出推理规则并证明合理性，后续配套论文将阐述从数据估计实体及其实例化方法与实验结果。
2026-07-28 cs.AI cs.LO
A Kruskal Decision Procedure for Intuitionistic Modal Logic IK4
Scuola Normale Superiore（意大利高等师范学院）
该研究提出了直觉模态逻辑IK4的Kruskal判定程序，通过无切嵌套证明结合Kruskal定理等证明其可判定性，给出了统一的证明高度界。
2026-08-12 cs.LO
Pitts and Intuitionistic Multi-Succedent: Uniform Interpolation for KM
Université Paris Cité（巴黎西岱大学）；CNRS（法国国家科学研究中心）；IRIF（信息与随机研究所）；University of Birmingham（伯明翰大学）；University of Melbourne（墨尔本大学）
将 Pitts 的均匀插值证明论技术扩展到直觉主义多后承设定，为直觉主义模态逻辑 KM 设计终止的多后承相继演算并构造均匀插值，同时证明 KM-代数类的连贯性。
2026-05-27 cs.LO math.LO
Uniform Lyndon interpolation for intuitionistic monotone modal logic
本文证明了直觉单调模态逻辑$\mathsf{iM}$具有一致Lyndon插值性质性质（ULIP）.逻辑$\mathsf{iM}$是一种基于直觉的非正规模态逻辑，而ULIP属性是插值的加强，其中插值只依赖于蕴涵的前提或结论，并尊重命题变元的极性。我们的方法来证明ULIP产生明确的一致插值，并利用了一个终止的微积分$\mathsf{iM}$，我们已经为此目的开发。据我们所知，$\mathsf{iM}$具有ULIP和一个终止的逻辑演算的结果是第一个直觉非正规模态逻辑的结果。然而，而不是证明这些特定的结果，我们的目的是显示的建设性证明理论方法，我们用来证明ULIP的灵活性。它在过去几年中得到了发展，并已被应用于子结构，中间，经典（非）正规模态和直觉正规模态逻辑。根据这些结果，直觉非正规模态逻辑似乎是一个自然的下一类尝试应用该方法，我们在这方面迈出了第一步。
2022-08-09 cs.LO math.LO
An Intuitionistic Linear Logical Semantics of SAND Attack Trees
本文介绍了直觉线性逻辑中SAND攻击树的一种新的逻辑基础。这个新的基础是基于一个新的逻辑称为攻击树线性逻辑（ATLL）。在介绍ATLL之前，我们给出了几种新的攻击树逻辑模型，第一种是基于真值表的攻击树逻辑模型。然后，我们把这种语义提升为一种基于线性的攻击树语义，它引入了蕴涵，但这可以进一步提升为ATLL所基于的辩证模型。ATLL的一个重要特征是它支持顺序合取的完全分布性。
2018-01-21 cs.LO
An Intuitionistic Formula Hierarchy Based on High-School Identities
我们通过采用公式作为指数多项式的观点来重新审视直觉等价和形式证明表示的概念。在观察到大多数的可逆证明规则的直觉（最小的）命题演算是公式（即）同构对应的高中身份，我们可以得到一个更紧凑的变体的证明系统，只包括不可逆的证明规则，其中可逆的证明规则已被替换的公式规范化过程。此外，对于某些证明系统，如Vorob'ev，Hudelmaier和Dyckhoff的G4 ip微积分，甚至可以将所有的不可逆证明规则视为指数多项式之间的严格不等式;为了建立这一事实，给出了仔细的组合处理。最后，我们扩展了指数多项式类比的一阶量词，表明它产生了一个直观的层次结构的公式，类似于经典的算术层次结构，第一个分类公式，同时保持同构。
2018-08-12 cs.LO math.LO
Intersection Logic in sequent calculus style
交型赋值系统直接设计为将直觉逻辑的蕴涵和合取片断的公式赋值给代数演算的项的演绎系统。但它与逻辑的关系并不规范。所有的逻辑之间，已被提出作为其基础，我们认为ISL，它给出了一个逻辑解释的交集分裂的直觉合取成两个连接词，分别与本地和全球的行为，是当地的交集。我们认为ISL是一个有趣的逻辑本身，为了支持这一说法，我们给它的微积分制定，我们证明了它享有削减消除属性。
2011-01-24 cs.LO cs.PL
Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
本文为Fischer Servi的直觉主义模态逻辑IK及其扩展提供证明逻辑对应物，通过扩展证明项语法、公理化和无切嵌套序列系统实现语法实现。
2025-07-12 cs.LO math.LO
Meaning and identity of proofs in a bilateralist setting: A two-sorted typed lambda-calculus for proofs and refutations
本文为Wansing双直觉主义逻辑2Int构建双类类型化λ演算λ-2Int，建立带项标注的证明系统并证明对偶化定理，从而从双边主义视角探讨证明的意义、指称与同一性问题。
2024-02-23 cs.LO math.LO
Continuation-passing Style Models Complete for Intuitionistic Logic
一类模型，在连续单子的形式多态的一阶个人，这是健全的和完整的最小直觉谓词逻辑。证明的健全性和完整性是建设性的，其组成的计算内容，特别是一个$β$ -规范化的评估程序简单类型的lambda演算和类型。虽然灵感来自Danvy的类型导向部分求值器，但避免了分隔控制运算符（即计算效果）的必要使用。多态性的作用是至关重要的--去掉它可以让我们获得经典谓词逻辑的模型完备的概念。我们的模型和克里普克模型之间的联系是通过加强双重否定转移图式来实现的。
2011-03-03 cs.LO cs.PL math.LO
Dualized Simple Type Theory
我们提出了一种新的双直觉类型论，称为对偶类型论（DTT）。它是一个简单的类型论，具有完美的直觉对偶性，并对应于单边极化的微积分。我们证明DTT强正规化，并证明类型保持。DTT基于一种新的命题双直觉逻辑，称为对偶直觉逻辑（DIL），它建立在Pinto和Uustalu的逻辑L之上。DIL是L的一种简化，通过删除几个可接受的推理规则，同时保持一致性和完整性。此外，DIL是使用二元语法定义的，通过用极性标记公式和逻辑连接词，从而减少了定义逻辑所需的推理规则的数量。我们给出了相容性的一个直接证明，但证明完全性是通过约简到L。
2016-08-07 cs.LO
Classical and Intuitionistic Subexponential Logics are Equally Expressive
经典逻辑的直觉限制被标准地看作是增加了逻辑的表达性，因为经典逻辑可以通过双重否定在直觉逻辑中得到充分的表示，而另一个方向没有真值保持的命题编码。在这里，我们表明，次指数逻辑，这是一个家庭的子结构的经典逻辑，每个参数在一个前序的次指数连接词的改进，不遭受这种不对称性，如果前序是系统修改的编码的一部分。准确地说，我们显示了合成（即，聚焦的）对给定编码取模的部分双导数。我们的编码特定的次指数前序的特殊情况下，产生了已知的和新的充分性定理的子结构逻辑。
2010-06-16 cs.LO
A linear linear lambda-calculus
本文针对直觉主义乘加线性逻辑证明语言提出代数意义上的线性性定理，整合加法与标量乘法，为构建量子编程语言的逻辑研究计划提供支撑。
2024-04-09 cs.LO
A sequent calculus with procedure calls
在本文中，我们扩展的演算LKF到演算LK（T），允许调用一个决策过程。我们证明了LK（T）的截消元。
2012-04-23 cs.LO
