A Labelled Sequent Calculus for Public Announcement Logic
公告逻辑（PAL）是认知逻辑（EL）的扩展，具有一些归约公理。在本文中，我们提出了一个无割标记的PAL演算，这是一个扩展的EL与简化公理的调整规则。这种演算允许切割，并允许终止证明搜索。
2022-10-27 cs.LO
A Gödel Calculus for Linear Temporal Logic
我们考虑哥德尔时序逻辑（$\sf GTL$），一个变种的线性时序逻辑的基础上哥德尔-达米特命题逻辑。在最近的工作中，我们已经表明，这种逻辑享受自然语义作为一个模糊逻辑和作为一个超直觉逻辑。使用语义学方法，证明了该逻辑是{ \sc pspace}-完全的。在本文中，我们提供了一个演绎演算$\sf GTL$，并表明这种演算是健全的和完整的上述语义。
2022-05-10 cs.LO
A Cut-free Sequent Calculus for Bi-Intuitionistic Logic: Extended Version
双直觉主义逻辑是直觉主义逻辑的推广，它具有一个与蕴涵有关的联结对偶。双直觉逻辑是由Rauszer作为具有代数和Kripke语义的Hilbert演算引入的。但她随后对BiInt的"无切“演算最近被Uustalu证明是失败的。我们提出了一个新的切割免费的BiInt演算，并证明它的声音和完整的Kripke语义。确保完整性是复杂的含义和它的对偶之间的相互作用，类似于未来和过去的时态逻辑模态。我们的演算处理这种相互作用，使用扩展序列传递信息的前提下的结论，使用实例化的变量在失败的派生树的叶子。我们简单的终止论证允许我们的演算用于自动演绎，尽管这不是它的主要目的。
2007-04-17 cs.LO
Light Logics and the Call-by-Value Lambda Calculus
所谓的轻逻辑已经被引入作为具有相当显著的规范化性质的逻辑系统。然而，从这些逻辑为纯λ演算设计类型分配系统是有问题的。在本文中，我们表明，从通常的按名称调用的转换到按值调用的λ演算允许恢复与底层逻辑的强连接。这将在基本仿射逻辑（EAL）的上下文中完成，设计一个自然演绎风格的类型系统，将EAL公式分配给lambda项。
2008-11-07 cs.LO
A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus
本文引入了由前向汇合 Kripke 模型刻画的自然直觉主义模态逻辑 FIK，为其提供了完备的 Hilbert 风格公理化和双嵌套演算，该演算兼具判定程序与有限反模型提取功能。
2023-09-12 cs.LO
Combining Event Calculus and Description Logic Reasoning via Logic Programming
本文介绍了一种在逻辑程序设计框架下将事件演算与描述逻辑相结合的知识表示语言。其目的是为用户提供一种表达语言，用于建模和分析随时间演变的系统。该方法的例子与逻辑程序设计语言中实现的Fusarium系统。本文扩展了Fusarium的规则语言与描述逻辑$\cal ALCIF$的弱DL-安全接口，并使事件演算适应这种扩展语言。通过这种方式，带时间戳的ABOX可以在事件演算中作为流畅项进行操作。这一切都是在福柯的时间分层概念的框架内进行的。本文件酌情提供了健全性和完整性的条件。使用一个详细的例子，它演示了事件演算，描述逻辑和逻辑编程规则的相互作用，用于计算可能的模型作为合理的解释的建模系统的当前状态。
2021-09-10 cs.LO
A Graph Calculus for Predicate Logic
我们介绍了一个反驳图演算经典的一阶谓词逻辑，这是以前的二元关系的扩展。一个简化的逻辑后果，建立一个构造的图有空的扩展，即。e.它代表底部。我们的演算通过将图转换为范式来确定图具有空扩展，该范式被扩展到其他图，直到我们可以识别冲突的情况（等价于公式及其否定）。
2013-03-29 cs.LO
Note on a Translation from First-Order Logic into the Calculus of Relations Preserving Validity and Finite Validity
Institute of Science Tokyo（东京科学大学）
本文提出了一种将一阶逻辑公式转换为关系演算方程的线性大小翻译方法，同时实现了对一阶逻辑三个变量片段的保守约简。
2025-12-24 cs.LO
On Coupled Logical Bisimulation for the Lambda-Calculus
我们研究了耦合逻辑互模拟（CLB）的原因上下文等价的演算。CLB起源于Dal Lago，Sangiorgi和Alberti的工作，作为一种工具来推理具有概率结构的微积分。我们适应原来的定义，以纯粹λ演算。我们开发了CLB的元理论，在按名称调用和按值调用中，并与应用互模拟（由于Abramsky）和逻辑互模拟（由于Sangiorgi，Kobayashi和Sumii）进行比较。我们还研究了增强的互模拟方法CLB开发的理论上的技术的情况下，对应于互模拟的功能不一定是单调的。
2014-10-10 cs.LO
A repetition-free hypersequent calculus for first-order rational Pavelka logic
我们提出了一个hypererprincipal演算$\text{G}^3\textŁ\forall$的一阶无穷值的Rankukasiewicz逻辑和它的扩展，一阶理性Pavelka逻辑，微积分是自底向上的证明搜索。在$\text{G}^3\textŁ\forall$中，没有结构规则，所有规则都是可逆的，并且在规则的任何前提中，公式的多集合的指定都不重复。演算$\text{G}^3\textŁ\forall$证明任何句子，该句子在至少一个先前已知的超演算中可证明。研究了$\text{G}^3\textŁ\forall$的证明理论性质，从而为证明搜索算法提供了基础。
2019-01-28 cs.LO
Sequent Calculus for Intuitionistic Epistemic Logic
直觉主义认知逻辑IEL的形式系统是由S. Artemov和T.原教皇它基于直觉主义的Brouwer-Hayting-Kolmogorov语义学，为从直觉主义的角度研究知识提供了形式化的基础。我们构造了IEL的一个无割演算，证明了在多项式空间中进行证明搜索是充分的，从而证明了IEL是PSPACE-完全的。
2015-08-31 cs.LO
A simple sequent calculus for nominal logic
名词逻辑是一阶逻辑的变体，它支持抽象语法中的绑定名称的推理。名词逻辑的一个关键特征是新量词，它对新名称（迄今为止未出现在任何值中的名称）进行量化。以前的尝试已经作出了开发方便的规则推理与新的量词，但我们认为，这些尝试都是不完全令人满意的。在这篇文章中，我们开发了一个新的numerical演算的名义逻辑中的规则，新的量词是比以前的尝试简单得多。我们还证明了几个结构和元理论的性质，包括削减消除，一致性，和等价的皮茨公理化的名义逻辑。
2013-12-17 cs.LO
Clone Theory: Its Syntax and Semantics, Applications to Universal Algebra, Lambda Calculus and Algebraic Logic
本文的主要目的是提出一种统一的方法，将逻辑系统的语法转化为一定的初始代数结构，以便用代数的方法来研究它。为此目的人们可以选择的代数结构是一个范畴的一个完整子范畴上的各种克隆。证明了方程逻辑、λ演算和一阶逻辑的语法都可以表示为正整数集合上的克隆或克隆的右代数。语义，然后表示来自这些克隆左代数的结构。
2008-10-17 cs.LO
First-Order Game Logic and Modal Mu-Calculus
本文研究了一阶博弈逻辑和一阶模态μ演算，它们用解释效果的一阶模态（如变量赋值）扩展了命题模态逻辑。不像在命题的情况下，这两个逻辑被证明具有相同的表达能力和他们的证明演算具有相同的演绎能力。两种结石也相互比较完整。在微分方程的存在下，推论获得了微分博弈逻辑（混合博弈的演绎验证逻辑）和微分μ演算（混合系统的模态μ演算）之间的可用和完整的翻译。微分μ-演算相对于一阶不动点逻辑是完备的，微分对策逻辑相对于它的无常微分的片段是完备的。
2022-02-11 cs.GT cs.LO math.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
On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
本文借助线性逻辑及其指数模态构造线性化系统 \muLLmodinf{}，并通过线性翻译证明非良基模态 $μ$-演算的语形切割消除。
2025-06-11 cs.LO
Axiomatizing Epistemic Logic of Friendship via Tree Sequent Calculus
本文积极地解决了Seligman、Girard和Liu等人提出的友谊认知逻辑是否能提供一个希尔伯特系统的问题。为了找到一个Hilbert系统，我们首先介绍了一个健全的，完整的和无割的树（或嵌套）EFL演算，这是一个集成的组合Seligman的基本混合逻辑的树演算和模态逻辑的树演算。然后，我们将树的结构转换成一个普通的公式来指定EFL的Hilbert系统，最后证明我们的Hilbert系统对于预定的二维语义是健全和完备的。
2019-07-10 cs.LO math.LO
Kuroda's Translation for the $λΠ$-Calculus Modulo Theory and Dedukti
本文将黑田翻译适配至λΠ-演算模理论下的高阶逻辑理论，并开发工具为证明语言Dedukti中的证明实现该翻译，扩展了经典逻辑到直觉主义逻辑嵌入的适用范围。
2024-07-09 cs.LO
Clones and Genoids in Lambda Calculus and First Order Logic
基因型是两个对象的范畴，其中一个是自身与另一个的产物。一个genoid可以看作是一个抽象的置换代数。这是一个值得注意的事实，这样一个简单的概念，可以用来提供一个统一的代数方法，λ演算和一阶逻辑。
2012-09-07 cs.LO cs.PL
Dedukti: a Logical Framework based on the $λ$$Π$-Calculus Modulo Theory
本文介绍逻辑框架Dedukti，它基于模理论的$\lambda$$\Pi$-演算，能表达多种逻辑理论并检查其他证明系统（如Zenon、HOL Light等）的大型证明库。
2023-11-13 cs.LO
Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic -- Extended Version
全直觉线性逻辑（FILL）是用PAR扩展的乘法直觉线性逻辑。它的证明理论是出了名的难以得到正确的，现有的微积分都涉及带有复杂注释的推理规则，以保证可靠性和切割消除。我们给出了一个简单的和无注释的显示演算的填充，满足贝尔纳普的通用削减消除定理。要做到这一点，我们的显示演算实际上处理了FILL的扩展，称为双直觉线性逻辑（BiILL），通过一个带有par的附加词定义了一个“排除”连接词。我们完善我们的显示演算为BIILL到一个切自由嵌套的嵌套式演算与深推理，其中显式的结构规则的显示演算成为可接受的。分离性保证了在深度推理演算中FILL公式的证明不包含任何排除的痕迹。每个这样的规则对于FILL的语义来说都是合理的，因此我们的深度推理演算和显示演算相对于FILL是保守的。深度推理演算还具有子公式性质和终止反向证明搜索，这给出了BiILL和FILL的NP-完全性。
2013-07-18 cs.LO
Nested-sequent Calculus for Modal Logic MB
本文针对模态逻辑 MB 的完全性与可判定性未决问题，构造了其嵌套矢列演算并加以解决，同时探讨了添加新模态符号后的逻辑 MB+。
2024-12-31 cs.LO
Encoding many-valued logic in $λ$-calculus
本文扩展Church编码至McCarthy三值逻辑，并推广到四、五值逻辑，在无穷λ-演算中通过⊥统一不可解项，还适用于λI-演算，并用于计算无限命题真值以探讨Russell悖论。
2021-06-26 cs.LO
A Proof Tree Builder for Sequent Calculus and Hoare Logic
我们已经开发了一个基于Web的教学证明助手，证明树生成器，它可以让你从最初的目标向上应用规则在微积分和霍尔逻辑的一个简单的命令式语言。我们配备了一个基本的证明自动化功能和Z3集成我们的工具。普林斯顿大学自动推理课程的学生使用了我们的工具，并发现它很直观。证明树生成器可在https://proof-tree-builder.github.io上在线获得。
2023-03-10 cs.LO
Reducing Higher Order Pi-Calculus to Spatial Logics
在本文中，我们表明，理论的过程可以减少到理论的空间逻辑。首先，我们提出了一种高阶π演算的空间逻辑SL，并给出了SL的推理系统。证明了SL的可靠性和不完备性。进一步证明了SL公式的结构同余关系和一步转移关系可以用SL公式的逻辑关系来描述。我们还扩展了SL公式的过程的互模拟。然后，我们扩展SL的所有定义和结果，SL的弱语义版本，称为WL。最后，我们在SL中加入了mu算子。这个新逻辑被命名为muSL。我们证明了WL是muSL的一个子逻辑，并且复制算子可以用muSL表示。
2012-11-17 cs.LO
Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 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
Structural Multi-type Sequent Calculus for Inquisitive Logic
本文定义了一种可靠的、完备的、具有Belnap式割消和子公式性质的多型演算。探究逻辑是探究语义的逻辑，由Groenendijk，Roelofsen和Ciardelli开发的语义框架，它捕获自然语言中的断言和问题。探究式逻辑是健全的，完整的。所谓的状态语义（也称为团队语义）。希尔伯特式的探究逻辑表示在一致替换下并不是封闭的;事实上，某些公式的出现被限制在公式的某个子类中，称为平坦公式。这一点和其他特征使得对这种逻辑的解析演算的探索并不简单。我们开发了一定的代数和秩序理论分析的团队语义，它提供了一个多类型的环境，占两个域的解释，平面和一般公式，以及它们的相互作用的设计准则。这种多类型的环境反过来又为我们在本文中介绍的查询逻辑的多类型演算提供了语义环境。
2016-04-04 cs.LO
Completeness of Flat Coalgebraic Fixpoint Logics
模态不动点逻辑传统上在计算机科学中起着核心作用，特别是在人工智能和并发性中。μ演算和它的亲属是这类逻辑中最具表现力的。然而，流行的定点逻辑倾向于用表达性来换取简单性和可读性，事实上，它经常存在于μ演算的单个变量片段中。这种平坦定点逻辑的家族包括，例如，LTL、CTL和常识逻辑。将这一概念扩展到共代数逻辑的通用语义框架，使得能够覆盖标准μ演算之外的广泛逻辑，例如，分级μ演算和交替时间μ演算（如交替时间时序逻辑ATL）的平坦片段，以及概率和单调不动点逻辑。我们给出了一个通用的完整性证明的Kozen-Park公理化这样平坦的余代数不动点逻辑。
2016-06-09 cs.LO
Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures
语法逻辑是指多模态逻辑K的扩展，其中模态公理从形式语法生成。我们考虑一个证明理论，在嵌套微积分，与逆，即，语法逻辑，每个模态算子[a]都有一个逆。扩展以前的作品嵌套的tense逻辑系统，我们表明所有的语法逻辑（有或没有逆）可以在嵌套的tense演算，其中的公理是内在的演算作为结构规则的形式化。这些结石的语法切割消除证明使用类似的程序显示逻辑。如果文法是上下文无关的，那么可以摆脱所有的结构规则，支持深度推理和额外的传播规则。我们给出了一个新的半决策过程的上下文无关文法逻辑，使用嵌套的深度推理演算，并表明，在给定的上下文无关文法是正规的情况下，这个过程终止。与文献中所有其他现有的决策程序的规则文法逻辑，我们的程序不假设一个有限状态自动机编码的公理。
2012-04-11 cs.LO
The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics
TU Wien（维也纳工业大学）
本文研究了模态 mu-演算的交替层级在非平凡融合逻辑上的严格性问题，证明了多模态 mu-演算的交替层级在模态逻辑的非平凡融合上是严格的，并讨论了其退化为模态逻辑的示例。
2025-11-04 cs.LO
Communication, and concurrency with logic-based restriction inside a calculus of structures
众所周知，我们可以使用结构证明理论来提炼或概括现有的范例计算原语，或者发现新的范例计算原语。在这样的观点下，我们继续开发一个程序，其目标是建立逻辑系统的证明搜索和过程代数中的计算之间的对应关系。我们给出了一个纯粹的逻辑帐户的进程代数操作，其中严格包括我们发现在米尔纳CCS行动的限制行为。这在被赋予自对偶量词的深层推理结构演算中的逻辑系统中是可能的。使用证明搜索这样一个逻辑系统的无切证明，我们展示了如何解决可达性问题的进程代数，包含一个重要的片段米尔纳CCS。
2012-12-19 cs.LO
Decidability of Intuitionistic Sentential Logic with Identity via Sequent Calculus
我们的论文有两个目的：本文首先在Chlebowski和Leszczynska-Jasion的论文“An Investigation into Intuitionistic Logic with Identity”中提出的演算的基础上，给出了一个直觉主义非Fregean逻辑ISCI的演算（Bulletin of the Section of Logic 48（4），p. 259-283，2019），其次，我们通过所获得的系统讨论ISCI的可判定性问题。上述论文中的原始演算没有为ISCI提供可判定性结果。为了得到这个结果，有两个问题需要解决：直觉逻辑的所谓循环特性和由于身份专用规则的形式而缺乏子公式性质。我们讨论可能的路线，以克服这些问题：我们考虑一个较弱的版本的子公式属性，守卫的复杂性公式，可以包括在它里面，我们还提出了一个证明搜索过程，当它失败时，然后存在一个反模型（在Kripke语义ISCI）。
2022-04-14 cs.LO
Intersection Logic in sequent calculus style
交型赋值系统直接设计为将直觉逻辑的蕴涵和合取片断的公式赋值给代数演算的项的演绎系统。但它与逻辑的关系并不规范。所有的逻辑之间，已被提出作为其基础，我们认为ISL，它给出了一个逻辑解释的交集分裂的直觉合取成两个连接词，分别与本地和全球的行为，是当地的交集。我们认为ISL是一个有趣的逻辑本身，为了支持这一说法，我们给它的微积分制定，我们证明了它享有削减消除属性。
2011-01-24 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
Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems
本文给出了区间时态逻辑（ITL）和持续时间演算（DC）在无穷区间上的概率扩展，并给出了它们的完整的希尔伯特式证明系统。的完整性结果是一个强完备性定理的概率ITL系统相对于一个抽象的语义和相对完备性定理的概率DC系统相对于实时语义。所提出的系统subconsiderable概率实时DC从文献中已知的。所提出的系统之间的对应关系和系统的概率区间时态逻辑有限的时间间隔和扩展模态。
2007-07-19 cs.LO
Soft lambda-calculus: a language for polynomial time computation
软线性逻辑（[Lafont02]）是线性逻辑的一个子系统，其特征是PTIME类。我们介绍软Aldida演算作为演算典型的直觉和仿射变体的这种逻辑。我们证明了该演算的（无类型）项可以在多项式时间内约简。然后，我们扩展了软逻辑的类型系统与递归类型。这允许我们考虑表示列表的非标准类型。利用这些数据集，我们以插入排序算法为例，检验了软微积分的具体表达能力。
2003-12-07 cs.CC cs.LO
The taming of recurrences in computability logic through cirquent calculus, Part I
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（现在的）第一部分包含了一个完整性证明和一个可靠性证明，（即将出版的）第二部分包含了一个完整性证明。
2012-09-19 cs.LO math.LO
The taming of recurrences in computability logic through cirquent calculus, Part II
本文构造了一个相应的演算系统，并从可计算性逻辑的语义角度证明了它的可靠性和完备性（见http：//www.cis.upenn.edu/paggiorgi/cl.html）.该系统的逻辑词汇包括否定、平行合取、平行析取、分支递归和分支共递归。这篇文章分两部分发表，（前）第一部分包含了一个完整性证明，（现在）第二部分包含了一个完整性证明。
2011-06-19 cs.LO math.LO
Psi-calculi: a framework for mobile processes with nominal data and logic
psi演算的框架扩展了pi演算的数据结构和逻辑断言和条件的名义数据表。它们可以在进程之间传输，并且它们的名称可以像标准pi演算中那样静态地作用域。Psi演算可以捕获与其他提出的pi演算扩展相同的现象，例如应用pi演算，spi演算，融合演算，并发约束pi演算，以及具有多元通信信道或模式匹配的演算。PSI演算甚至可以更通用，例如允许结构化通道，高阶形式主义，如用于数据结构的λ演算，以及用于断言的谓词逻辑。我们提供了充分的比较，相关的结石，并讨论了一些重要的应用。我们标记的操作语义和互模拟的定义是直接的，没有结构一致性。我们建立最低要求的名义数据和逻辑，以证明一般代数性质的PSI演算，所有这些都已检查的互动定理证明伊莎贝尔。PSI演算的表达性明显超过其他形式主义，而语义的纯度与原始的PI演算相当。
2011-03-31 cs.LO
Dialectical logic: the Process Calculus
辩证逻辑是辩证过程的逻辑。辩证逻辑的目标是揭示逻辑计算系统中固有的动力学概念。标准逻辑中的命题和真值的基本概念被辩证逻辑中的过程和流的概念所包含。标准逻辑激发了辩证逻辑的核心顺序方面。Horn-clause逻辑要求类型和非对称性，也激发了辩证逻辑的平行方面。米尔纳和霍尔的过程逻辑揭示了辩证逻辑的内在和外在两个方面。辩证逻辑的序列内在方面应被看作是吉拉德线性逻辑的一种类型化或分布式的非对称张量形式。辩证逻辑的最简单版本本质上是直觉主义的。然而，通过遵循Glivenko在标准逻辑中使用双重否定闭包的方法，我们可以定义辩证逻辑的经典版本。
2018-10-09 cs.LO
A Sequent Calculus for Dynamic Topological Logic
本文对动态拓扑逻辑$\textbf{DTL}$的时间-拓扑片段$\textbf{DTL}_{0}^{\circ * \slash \Box}$引入了一个新的演算，利用\cite{paper3}中给出的$\textbf{DTL}_{0}^{\circ * \slash \Box}$的公理化，从语义上证明了其可靠性，并从语法上证明了其完备性. $\textbf{DTL}_{0}^{\circ * \slash \Box}$的无割的Tumbler演算是Gentzen经典Tumbler演算的命题片段、模态扩展的两个$\Box$结构规则、以及时间扩展的九个$\circ$（下一个）和$*$（下一个）结构规则的结合。未来的研究将集中在动态拓扑$\textbf{S5}$逻辑的超代数演算的建设，以证明Kremer的下一个删除猜想几乎离散空间$\textbf{S5H}$上的同胚逻辑。
2014-08-03 cs.LO math.LO
Towards the Formalization of Fractional Calculus in Higher-Order Logic
分数阶微积分是将经典的积分和微分理论推广到任意阶（即，实数或复数）。在过去的二十年里，这种新的数学建模方法已被广泛用于分析各种科学和工程领域的广泛的物理系统。在本文中，我们描述了一个正在进行的项目，旨在形式化的分数阶微积分的基本理论的HOL光定理证明。主要是，我们提出了这种形式化工作的动机和应用，实现我们目标的路线图，项目的当前状态和未来的里程碑。
2015-05-08 cs.LO
LogicProof: An Interactive Web-Based Educational Theorem Prover for Natural Deduction and Sequent Calculus across Classical and Constructive Logics
Technical University of Košice（科希策理工大学）
介绍LogicProof这一用于教育的交互式网络定理证明器，支持经典和构造性逻辑的自然演绎与相继式演算，经学生测试能提升对形式证明构建的理解，补充现有教学方法。
2026-07-07 cs.LO
Command injection attacks, continuations, and the Lambek calculus
本文展示了命令注入攻击，延续和Lambek演算之间的联系：某些命令注入，如对SQL的重言式攻击，被证明是一种控制效果的形式，可以使用Lambek演算进行类型化，推广了延续的双重否定类型。Lambek的句法演算是一个逻辑，其中两个隐含连接词分别从左和右获取它们的论点。这些连接词描述了在构建句法结构时，字符串如何与它们的左右上下文相互作用。微积分是一种没有结构规则的命题逻辑，因此是线性逻辑和分离逻辑等子结构逻辑的先驱。
2016-06-21 cs.LO cs.PL
On syntactic concept lattice models for the Lambek calculus and infinitary action logic
本研究将Wurm提出的句法概念格语义扩展到带Kleene迭代的Lambek演算无穷版本（无穷动作逻辑），证明其强完备性及相关推论，还探讨了常元问题并强化了原有结果以纳入常元。
2025-10-28 cs.LO
A propositional cirquent calculus for computability logic
本文提出CL18公理化系统，用于可计算性逻辑的基本命题片段，并证明其相对于该逻辑博弈语义的可靠性与完备性。
2024-11-09 cs.LO math.LO
A Non-Wellfounded and Labelled Sequent Calculus for Bimodal Provability Logic
本研究针对双模可证性逻辑CS，基于类Kripke语义建模构建带标记非良基演算系统，借助循环证明理论实现逆良基性，证明系统的可靠性与完备性，同时给出原始判定程序和反模型提取方法。
2025-06-17 cs.LO math.LO
A Process Calculus with Logical Operators
为了将规范的操作和逻辑风格结合在一个统一的框架中，Lüttgen和Vogler在[TCS 373（1-2）：19-40; Inform.计算（& C）208：845-867]。与通常的LTS相比，本文引入了逻辑LTS上的两个逻辑构造器$\wedge$和$\vee$来描述规范的逻辑组合。目前，这类框架已经得到了相当深入的研究，但过程代数式的方法尚未涉及，逻辑LTS上构造函数的公理化也没有。本文试图沿着这个方向发展吕特根和Vogler的工作。我们将提出一个逻辑LTS（CLL，简称）的进程演算。语言CLL详细探讨了从两个不同的，但等价的观点。基于行为视图，采用就绪模拟的概念对精化关系进行形式化描述，发展了行为理论。基于证明论的观点，给出了一个可靠的、基础完备的CLL公理系统，它通过（不）方程律来捕获CLL中的算子。
2012-12-11 cs.LO
Justification Logic of the Lambda Calculus
Faculty of Technical Sciences, University of Novi Sad（诺维萨德大学技术科学学院）；Mathematical Institute of the Serbian Academy of Sciences and Arts（塞尔维亚科学院数学研究所）；School of Computer Science, University of Birmingham（伯明翰大学计算机学院）
研究λ演算的证明逻辑，通过引入一种逻辑，其模态证明项为类型化λ项，能同时推理计算与证明。给出公理系统、自然演绎系统及Curry-Howard解释，还构建相继式演算并证明切割消去，得到归一化结果。
2026-07-28 cs.LO math.LO
A Sequent Calculus for Modelling Interferences
一个逻辑演算，这是一个保守的线性逻辑的扩展。这项工作的动机涉及懒惰评估，真正的并发性和干扰证明搜索。该演算包括两个新的连接词来处理多重结构，并具有割消性质。扩展提出了第一个结果，我们的目标。
2007-06-22 cs.LO
Display to Labeled Proofs and Back Again for Tense Logics
我们介绍之间的翻译显示演算证明和标记演算证明的紧张逻辑的背景下。首先，我们证明了，在显示演算的最小时态逻辑Kt扩展与一般路径公理的每一个派生可以有效地转化为相应的标记演算的派生。关于逆翻译，我们表明，Kt扩展与路径公理，在相应的标记演算的每个派生可以放入一个特殊的形式，是可翻译的派生在相关的显示演算。在这个逆翻译中的一个关键见解是将显示序列规范表示为标记的多树。标记的多树，它表示等价类的显示序列模显示公设，也揭示了相关的对应结果紧张的逻辑。
2021-05-06 cs.LO math.LO
Teaching a Formalized Logical Calculus
经典一阶逻辑在许多方面都是数学、语言学、计算机科学和人工智能的核心，因此有必要详细定义它。我们提出了合理性和完整性证明的一阶逻辑，形式化的互动证明助手伊莎贝尔/HOL的一个微积分。我们的形式化是基于Stefan Berghmann的工作，我们已经更新为使用Isabelle的声明式证明风格Isar（正式证明档案，条目FOL-Fitting，2007年8月/2018年7月）。我们用de Bruijn指数表示变量;这使得在量词下的替换对人类读者来说不那么直观。然而，与使用字符串表示的变量的替换实现相比，自然数的性质产生了一个优雅的解决方案。所考虑的微积分具有一个总是空的前件和一个在后件中的公式列表的特殊性质。我们得到的可靠性和完整性的证明，作为其tableau对应的逆对偶的派生结果的微积分。我们努力不仅提出的结果的合理性和完整性的证明，但也提供了一个深入到一个类似编程的方法，一阶逻辑语法，语义和微积分的形式化。我们在一门计算机科学专业的逻辑本科课程中使用了这种形式化，并讨论了我们的经验。
2020-02-28 cs.LO
A cirquent calculus system with clustering and ranking
循环演算是G.Japaridze为了满足其可计算逻辑理论的需要而提出的一种新的证明理论和语义方法。Japaridze的早期文章“From formulas to cirquents in computability logic”将cirquents的概念推广到了所谓的聚类和排序的版本，并表明，通过聚类和排序的cirquents，可以捕获，提炼和推广所谓的扩展IF逻辑。雅帕里泽的治疗扩展IF逻辑，但是，是纯粹的语义，并没有演绎系统提出。本文从句法上构造了一个具有聚类和排序功能的、可靠的、完备的w.r.t.基于情境的语义学的命题片段。这样一个系统不仅可以被认为是经典命题逻辑的保守扩展，而且当被限制为不超过2秩的cirquents时，也可以被认为是完全一般性的纯命题扩展IF逻辑的公理化。
2014-09-11 cs.LO
