Embedding Modal Logics into Logics of Bunched Implications
Australian National University（澳大利亚国立大学）
本文给出S4嵌入BBI的全新句法证明，证明其在S4任意公理扩张下稳定，可扩展至BBI的多种语言扩张，还给出BBI演绎定理的首个完整证明。
2026-08-10 cs.LO math.LO
Stone-Type Dualities for Separation Logics
本文系统建立了分离逻辑及其变体的Stone型对偶定理，统一处理BI、BBI及多种扩展逻辑，首次证明了DMBI等逻辑的可靠性与完备性，为资源语义提供了范畴论框架。
2019-03-13 cs.LO
Semantic Cut Elimination for the Logic of Bunched Implications, Formalized in Coq
集束蕴涵逻辑（BI）是构成分离逻辑主干的子结构逻辑，分离逻辑是研究堆操作程序推理的逻辑。虽然BI的证明理论和元理论在数学上都有涉及，但重要的元理论结果的形式化仍然刚刚起步。在本文中，我们提出了一个自包含的形式化，在Coq的证明助手，证明了中央元理论性质的BI：削减消除其微积分。提出的证明是 * 语义 *，在这个意义上说，是通过解释在一个特定的“通用”模型的序列。这导致了一个比标准的Gentzen风格的切割消除参数更模块化和优雅的证明，这在BI的手动证明中可能是微妙和容易出错的。特别是，我们的语义方法避免了不必要的反演证明推导，或使用削减减少和多削减规则。除了模块化，我们的方法也是强大的：我们演示了我们的方法规模，与微小的修改，（i）BI的扩展与任意一组的\emph{simple structural rules}，和（ii）扩展与S4一样的$\Box$模态。
2021-12-10 cs.LO math.LO
Semantical Analysis of the Logic of Bunched Implications
我们给出了一种新的方法来证明逻辑（以下简称：对象逻辑）的可靠性和完备性，该逻辑绕过模型中的真值直接与有效性一起工作。我们不是在特定的模型中使用特定的世界，而是使用特征世界（即，世界的一般代表）在任意模型中。这种推理被一个元逻辑（在这种情况下，一阶经典逻辑）的微积分捕获，它的表达足以捕获对象逻辑的语义。从本质上讲，人们对对象逻辑的有效性有一个演算。该方法通过还原逻辑的视角（与演绎逻辑的更传统范式相反）进行，使用还原空间作为媒介，以展示对象逻辑的相继演算和有效性演算中还原的行为等价性。而不是研究一般的技术，我们说明了它的逻辑集束的影响（BI），因此IPL和MILL（无否定）也治疗。直观地说，BI是直觉命题逻辑和乘法直觉线性逻辑的自由组合，这使得它的元理论相当复杂。关于BI的文献包含许多相似但最终不同的代数结构和满足关系，它们要么仅捕获逻辑的片段（尽管很大），要么具有用于某些连接词的复杂子句（例如，Beth's clause for disjunction instead of Kripke's）。正是这种复杂性促使我们使用BI作为这种语义方法的案例研究。
2022-10-11 cs.LO math.LO
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
作为会话的命题（Propositions-as-Sessions）的出现，为消息传递并发奠定了逻辑基础，它是线性逻辑命题与并发进程会话类型之间的Curry-Howard对应。这种方法的核心是由线性逻辑预示的资源消耗范式。在本文中，我们研究了一个新的点，在设计空间的会话类型系统的消息传递并发程序。我们确定O 'Hearn和Pym的逻辑束的影响（BI）作为一个富有成效的基础解释的逻辑作为一个并发程序设计语言。这导致了对非线性资源的处理，这与基于线性逻辑的现有方法完全不同。我们介绍了一个新的$π$ -演算会话，称为$π$ BI，其最显着的特点是一个构造称为产卵，它表达了新的形式的共享，诱导BI的结构原则。我们说明了$π$ BI的表现力，并奠定了其基本理论：类型保存，死锁自由和弱规范化的结果良好的类型化进程;一个操作上健全和完整的仿射$λ$ -演算的类型化编码;和一个非干扰的结果访问资源。
2022-09-12 cs.LO cs.PL
Proof-theoretic Semantics for the Logic of Bunched Implications
本文为捆绑蕴含逻辑提出一种基扩展语义，系统组合IPL与IMLL的B-eS，以处理捆绑结构的复杂性，并展示其在安全建模中的应用。
2024-11-11 cs.LO math.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
A Proof-theoretic Semantics for Intuitionistic Linear Logic
Department of Computer Science, University College London（伦敦大学学院计算机科学系）
本文扩展了Gheorghiu等人对直觉主义乘法线性逻辑的基扩展语义，为完整的直觉主义线性逻辑（包括模态连接词bang）提供了证明论语义，并讨论了处理bang连接词的挑战。
2026-06-12 cs.LO
A Labelled Sequent Calculus for BBI: Proof Theory and Proof Search
我们提出了一个标记的布尔BI演算，一个经典的变种的O'Hearn和Pym的逻辑的集束蕴涵。微积分是简单的，健全的，完整的，并享受削减消除。我们表明，在我们的证明系统中的所有结构规则，包括那些规则，操纵标签，可以本地化周围的应用程序的某些逻辑规则，从而本地化这些规则的处理证明搜索。在此基础上，我们展示了一个自由变量演算，处理结构规则懒在约束系统。最后提出了一种求解约束的探试法，并给出了实验结果。
2015-05-04 cs.LO
A Probabilistic Separation Logic
概率独立性是一个有用的概念，用于描述随机抽样的结果-所有概率语言中的基本操作-和用于推理随机变量组。然而，现有的验证方法处理独立性很差，如果有的话。我们提出了一个概率分离逻辑PSL，其中分离模型概率独立性。本文首先给出了一个新的聚束蕴涵逻辑（BI）的概率模型。然后，我们建立了一个程序逻辑的基础上，这些断言，并证明系统的可靠性。我们证明了我们的逻辑验证信息理论的安全性的密码结构的几个众所周知的任务，包括私人信息检索，不经意的传输，安全多方除了，和简单的不经意的RAM。我们的证明纯粹是根据高级属性进行推理的，比如独立性和一致性。
2020-07-17 cs.LO cs.PL
Resource-distribution via Boolean constraints
我们考虑的问题，搜索证明顺序表示逻辑与乘法（或内涵）连接词。具体来说，我们从线性逻辑的乘法片段开始，一方面扩展到线性逻辑及其添加剂，另一方面扩展到集束蕴涵逻辑BI的添加剂。我们给出了一个代数方法计算乘法规则中的侧公式的分布，一旦有足够的信息，它允许在证明的分支上确定公式的发生或不发生。这样一个规则的结论中的每个公式都被赋予一个布尔表达式。随着搜索的进行，生成一组布尔约束方程。我们表明，这样一组方程的解决方案确定了相应的证明给定的搜索。我们解释了一系列的战略，从懒惰的渴望，解决约束方程组。我们指出如何将我们的方法系统地应用到大家庭的相关系统。
2000-12-21 cs.LO
Focusing and Polarization in Intuitionistic Logic
聚焦证明系统提供了一个范式，以结构化的可逆和不可逆推理规则的应用程序的切割自由证明。Andreoli的线性逻辑的聚焦证明系统已经被应用于证明搜索和证明归一化方法。文献中的各种证明系统都表现出某种程度上的聚焦特性。我们提出了一个新的，集中的证明系统的直觉逻辑，称为LJF，并显示如何其他证明系统可以映射到新的系统，通过插入逻辑连接，过早地停止聚焦。我们还使用LJF设计了一个经典逻辑的集中证明系统。我们的方法来设计和分析这些系统的基础上的完整性集中在线性逻辑和极性的概念，出现在吉拉德的LC和LU证明系统。
2007-08-16 cs.LO
Intuitionistic Layered Graph Logic: Semantics and Proof Theory
该文提出直觉主义分层图逻辑ILGL，给出其语义与证明论，证明可判定性及Stone对偶，并扩展至谓词版本，用于建模复杂系统的分层结构。
2018-10-29 cs.LO
Structural focalization
本文提出命题直觉主义逻辑的聚焦矢列演算，借助结构化消切风格的归纳证明其聚焦性、内部可靠性与完备性，主要贡献在于恒等扩张证明。
2014-03-17 cs.LO
Skolemisation for Intuitionistic Linear Logic
本文针对聚焦直觉主义线性逻辑提出了一阶聚焦变体，并给出了可靠且完备的斯科伦化过程，以改进证明搜索并减少回溯。
2024-05-02 cs.LO
Towards the Automated Generation of Focused Proof Systems
本文处理的问题，制定和证明的完整性集中式证明系统在自动化的方式。聚焦是一门关于证明的学科，它将证明结构分成多个阶段，以减少证明搜索的非确定性。我们证明了，它是可能的构造一个完整的集中证明系统从一个给定的非集中证明系统，如果它满足一定的条件。我们的核心思想是推广基于Miller和Saurin给出的置换引理的线性逻辑证明系统的完备性证明。这是通过从证明系统的规则置换关系构建一个图来完成的，称为置换图。然后，我们表明，从一个给定的证明系统的置换图，它是可能的，以构建一个完整的集中证明系统，并另外推断哪些公式收缩是允许的。提供了一种用于构建系统的置换图的实现。我们应用我们的技术生成集中的证明系统MALLF，LJF和LKF的线性，直觉和经典逻辑，分别。
2015-11-13 cs.LO
Fixpoint constructions in focused orthogonality models of linear logic
本文研究线性逻辑聚焦正交性范畴中的不动点构造理论，通过证明初始代数和终余代数的提升定理，为带类型最小和最大不动点的模型提供公理化范畴框架，并扩展至域论中双自由代数的提升。
2023-11-18 cs.LO math.CT
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
本文探讨了基于序列的证明形式化方法的层级结构，分析了内部与外部演算的区别及其翻译难度。
2025-05-07 cs.LO math.LO
Provability in BI's Sequent Calculus is Decidable
本文针对束蕴涵逻辑（BI）自问世以来缺乏有效证明搜索过程的问题，通过推广根岑的可判定性论证并结合戴克霍夫缩并消除论证的关键特征，证明可将任意相继式的证明搜索空间规约为原始递归集，从而得出BI相继式演算的可证明性是可判定的，但文中存在错误导致主定理证明无效。
2024-04-12 cs.LO cs.SC math.LO
Modular Labelled Sequent Calculi for Abstract Separation Logics
抽象分离逻辑是霍尔逻辑的一系列扩展，用于推理操纵诸如存储器位置之类的资源的程序。这些逻辑是“抽象的”，因为它们独立于任何特定的具体资源模型。他们的断言语言，称为命题抽象分离逻辑（PASL），以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。特别地，这些逻辑包含连接词$*$和$-\!*$，分别表示资源的组成和扩展。这种额外的表达能力是有代价的，因为所产生的逻辑都是不可判定的。鉴于其广泛的适用性，甚至半决策程序，这些逻辑是可取的。虽然在文献中讨论了几个PASL和它们与BBI的关系，但这些逻辑的证明理论和自动推理是本文的会议版本解决的开放问题，该版本使用无割标记演算为各种PASL开发了模块化证明理论。本文非平凡地改进了以前的工作，给出了一个一般框架的演算上的任何新的公理在逻辑满足一定的形式对应的推理规则在我们的框架，和完整性证明一般考虑这样的公理。我们的基础演算处理Calcagno等人。的原始逻辑的分离代数，增加了健全的规则，部分确定性和cancellativity，同时保持削减消除。然后，我们证明了分离逻辑中的许多重要性质，如不可分单元、不相交性、可分裂性和交叉分裂性，都可以用我们的一般公理形式表示。因此，我们的框架免费提供了这些属性的推理规则和完整性。最后，我们展示了我们的演算如何减少到具有全局标签替换的演算，从而实现更高效的实现。
2018-03-26 cs.LO cs.PL
Cut Elimination in Multifocused Linear Logic
我们研究切消除的多焦点变体的全线性逻辑在微积分。多焦点范式的证明产生的问题，不出现在一个标准的聚焦系统，有关的限制，在分组规则的情况下，在聚焦阶段。我们表明，削减消除可以在一个明智的方式，即使证明需要一些特定的引理来处理多聚焦阶段，并讨论与削减消除时所产生的困难，考虑范式的证明在线性逻辑。
2015-02-17 cs.LO
Least and Greatest Fixed Points in Linear Logic
MALL（乘法，加法线性逻辑）的一阶理论仅在等式上是一个有趣但弱的逻辑，因为它不能捕获无界（无限）行为。而不是通过增加指数（！和？），我们添加最小和最大不动点算子。由此产生的逻辑，我们称之为muMALL，满足两个基本的证明理论性质：我们建立弱规范化，我们设计了一个集中的证明系统，我们证明完整的。第二个结果提供了一个强范式的无切割证明结构，可用于，例如，帮助自动化证明搜索。我们展示了如何将这些基础应用于直觉逻辑。
2010-11-30 cs.LO
A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
逻辑学和类型论中的基本证明搜索策略可以被看作是规则在适当的微积分中的根优先应用，最好没有由规则置换产生的冗余。本文讨论的问题，定义这样的纯类型系统（PTS，这是最初提出的自然演绎风格），然后组织他们的规则，有效的证明搜索。我们引入纯类型序列演算与元变量（PTSCalpha）的想法，通过丰富的语法的置换自由演算的命题逻辑由于Herbelin，这是密切相关的自然演绎和已经很好地适应证明搜索。的操作语义是改编自Herbelin的，并定义了一个系统的本地重写规则，在削减消除，使用明确的替代。我们证明了这个系统的融合。限制我们的注意力PTSC，这个系统的地面条款的类型系统，我们得到的主题约简属性，并表明每个PTSC是逻辑等价于其相应的PTS，前者是强正规化的当且仅当后者是。我们展示了如何使PTSC的逻辑规则到一个语法导向的系统PS证明搜索，通过将转换规则的类型检查的PTS规则的语法导向的演示文稿。最后，我们考虑如何使用PTSCalpha的显式作用域元变量来表示部分证明项，并使用它们来分析交互式证明构造。这建立了一个框架PE，我们能够研究证明搜索策略，类型居民枚举和（高阶）统一。
2011-03-23 cs.LO
From IF to BI: a tale of dependence and separation
我们需要一个新的眼光在逻辑的信息依赖和独立的Hintikka和Sandu和Vaananen，和他们的组成语义由于霍奇斯。我们如何霍奇斯的语义可以被看作是一个特殊的情况下，一般建设，这提供了一个背景下，一个有用的完整性定理，就更广泛的一类模型。我们对逻辑的每个方面都有一些新的认识。我们表明，自然命题逻辑所携带的语义是捆绑的蕴涵由于Pym和O 'Hearn，它结合了直觉和乘法连接词的逻辑。这引入了几个新的连接词以前没有考虑在逻辑的信息依赖，但我们显示发挥了非常自然的作用，最显着的直觉含义。至于量词，我们表明，他们在霍奇斯语义的解释是被迫的，因为他们是下的图像通常的塔斯基语义的一般建设，这意味着他们是伴随着替代，因此唯一确定。至于依赖谓词，我们表明，这是从一个更简单的谓词，恒常性或依赖于没有定义。这就离不开直觉蕴涵的运用。然后将函数相关的Armstrong公理恢复为直觉蕴涵公理的标准集。我们还证明了Hodges风格的完全抽象结果，其中直觉蕴涵起着非常自然的作用。
2011-02-07 cs.LO math.LO
Canonicity of Proofs in Constructive Modal Logic
本文针对构造性模态逻辑中lambda演算与获胜策略间的证明等价性差距，通过扩充归约规则定义了新lambda演算，证明其规范化与合流性，并利用聚焦证明系统风格的类型系统建立了范式项与获胜策略间的一一对应关系。
2023-07-30 cs.LO
Certification of Prefixed Tableau Proofs for Modal Logic
不同的定理证明器倾向于以不同的格式产生证明对象，尤其是模态逻辑，其中已经提出了几种演绎形式主义（以及基于它们的证明器）。这项工作属于建立一个共同的规约语言，以证明在广泛的演绎形式主义的一般项目。特别是，通过使用从模态语言翻译成一阶极化语言和一个检查器，其小内核是基于一个经典的集中式微积分，我们能够证明模态证明标记的微积分，前缀tableaux和自由变量前缀tableaux。我们描述了逻辑K的一般方法，给出了它在一个类prolog语言中的实现，提供了一些例子，并讨论了如何将该方法扩展到其他正规模态逻辑
2016-09-14 cs.LO
Semi-Substructural Logics with Additives
本工作研究了偏斜幺半范畴证明论的扩展，提出并形式化了一种带加法连接词的聚焦相继式演算，有效减少了证明搜索的非确定性。
2024-04-23 cs.LO
A general proof certification framework for modal logic
证明认证中的一个主要问题是，不同的定理证明器，即使是为相同的逻辑设计的，也倾向于使用不同的证明形式，并以不同的格式产生输出。ProofCert项目促进使用一种通用的规约语言和一个小而可信的内核，以便检查来自不同来源和不同逻辑的证明。依靠这一思想，并通过使用经典的集中式演算作为核心，我们在这里提出了一个通用的框架检查模态证明。我们提出了一个类似于Prolog语言的框架的实现，并展示了如何可以专门化它在一个简单的和模块化的方式，以涵盖不同的证明形式主义，如标记系统，tableaux，numericalculi和嵌套numericalculi。我们通过提供几个例子来说明逻辑K的方法，并讨论如何进一步扩展该方法。
2018-10-24 cs.LO
Sequent Calculi for Data-Aware Modal Logics
本文从证明论视角研究数据感知混合模态逻辑HXpathD，提出了可靠完备的Gentzen式相继式演算，证明其规则可逆且满足切割消除，为数据感知模态逻辑及更广泛模态系统的证明论研究奠定基础。
2025-10-02 cs.LO
Lambek-Grishin Calculus: Focusing, Display and Full Polarization
\emph{Focused sequent calculi}是一种改进的证明演算，其中关于推理规则的适用性的附加副条件强制实现证明搜索策略。聚焦无割证明给出了一种特殊的范式，用于定义微积分证明的恒等式。通过对\emph{multi-type calculi}理论及其代数语义的\emph{heterogenous consequence relations}推广，提出了一种新的Lambek-Grishin逻辑的聚焦显示演算fD.LG和全极化代数语义FP.LG.微积分fD.LG有\emph{strong focalization}，它是\emph{sound and complete} w.r.t.这个完备性结果在某种意义上比标准极化代数语义的完备性更强（例如参见Bastenhof对于Lambek-Grishin逻辑的相位语义或Hamano和Takemura对于线性逻辑的相位语义），因为我们不需要在同一公式上连续应用移位的证明上做商。我们计划调查之间的连接，如果有的话，这个完整性的结果和概念的\emph{full completeness}介绍Abramsky等人。我们还显示了一些额外的结果。fD.LG是健全和完整的w.r.t. LG-代数：这相当于所谓的\emph{completeness of focusing}的语义证明，假定用于Lambek-Grishin逻辑的标准（显示）微积…
2020-11-05 cs.LO math.LO
On Geometry of Interaction for Polarized Linear Logic
我们提出了乘法极化线性逻辑（MLLP）的交互几何（GoI）模型，MLLP是Olivier Laurent的极化线性逻辑的乘法片段。这是通过将多个点均匀地添加到GoI的各种分类模型来完成的。在极化证明理论中，多点在语义上表征证明网络的动态性方面发挥着重要作用。例如，它们允许我们描述极化的关键特征，聚焦，以及我们构建具体极化GoI模型的基础。我们的方法两极分化GoI涉及两个独立的研究，根据不同的分类角度的GoI。(i)受Abramsky，Haghverdi和Scott工作的启发，定义了一个极化的GoI情况，其中多点被添加到配备有自反对象$U$的跟踪monoidal类别。使用这个框架，吉拉德的执行公式的分类版本的定义，以及GOI解释MLLP，证明。运行的执行公式示出的特征的聚焦属性（从而极性），以及动态的削减消除。(ii)Joyal-Street-Verity的Int构造是GoI建模的另一个基本范畴结构。在这里，我们调查它在一个多点设置。我们的演示文稿产生了一个紧凑的版本Hamano-Scott的极化类别，从而指称模型MLLP。这些产生于正和负对象的monoidal范畴之间的逆变对偶性，以及它们之间的适当双模结构（代表“非聚焦证明”）。最后，作为上述（ii）的一个特殊情况下，MLLP的紧凑模型也提出了基于Rel（集合和关系的范畴）配备了多点。
2017-04-07 cs.LO
A Survey of the Proof-Theoretic Foundations of Logic Programming
一些形式系统，如归结和最小模型语义，为逻辑编程提供了一个框架。在本文中，我们将调查使用结构证明理论作为替代基础。在过去的35年里，研究人员一直在使用这个基础来将逻辑编程从一阶经典逻辑的根源提升到直觉和线性逻辑的高阶版本。这些更具表现力的逻辑程序设计语言允许捕获有状态计算和丰富形式的抽象，包括高阶编程、模块化和抽象数据类型。术语级绑定是另一种抽象，在证明理论和这些扩展逻辑程序设计语言中，它们都得到了优雅而直接的处理。逻辑编程也激发了证明理论的新成果，例如涉及极性和聚焦证明的成果。这些最新的研究结果提供了一个高层次的手段，呈现前向链和后向链风格推理之间的差异。在证明论中验证逻辑编程也有助于识别它与函数式编程、演绎数据库和模型检验的联系和区别。
2021-10-30 cs.LO cs.PL
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
本文提出共诱导证明搜索方法，扩展至偏极直觉逻辑LJP，并通过解释将该方法应用于其他直觉逻辑系统，实现了解的可判定性继承。
2025-12-04 cs.LO math.LO
