FMP for QD logics. A wrong proof
本文旨在证明准密集逻辑具有FMP，但证明中存在无法修复的重大错误。
2026-03-16 cs.LO
Focusing and Polarization in Intuitionistic Logic
聚焦证明系统提供了一个范式，以结构化的可逆和不可逆推理规则的应用程序的切割自由证明。Andreoli的线性逻辑的聚焦证明系统已经被应用于证明搜索和证明归一化方法。文献中的各种证明系统都表现出某种程度上的聚焦特性。我们提出了一个新的，集中的证明系统的直觉逻辑，称为LJF，并显示如何其他证明系统可以映射到新的系统，通过插入逻辑连接，过早地停止聚焦。我们还使用LJF设计了一个经典逻辑的集中证明系统。我们的方法来设计和分析这些系统的基础上的完整性集中在线性逻辑和极性的概念，出现在吉拉德的LC和LU证明系统。
2007-08-16 cs.LO
A survey of proof nets and matrices for substructural logics
本文是一个调查的两种“压缩”证明计划，\emph{matrix method}和\emph{proof nets}，适用于各种逻辑沿着子结构层次从经典的所有方式到非关联的Lambek系统。为后者提供了一种新的处理证明网。证明网和矩阵的描述给出了一个统一的符号序列的基础上，使各种逻辑的计划的属性可以很容易地进行比较。
2012-03-22 cs.LO
Complexity of correctness for pomset logic proof nets
我们表明，它是coNP-完全的，以决定是否一个给定的证明结构的pomset逻辑是一个正确的证明网，使用图论在我们以前的文件（arXiv：1901.10247）。
2023-01-23 cs.LO
Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents (Extended version)
本文给出了基本正规时态逻辑Kt的一个线性嵌套演算。我们表明，演算，使向后证明搜索，反模型建设和句法切割消除。因此，线性嵌套序列提供了为包含逆的模态逻辑提供足够的证明理论所需的最小嵌套量。作为奖励，这产生了对称模态逻辑KB的无切演算。
2019-07-02 cs.LO
A logic of interactive proofs
本文提出概率双主体证成逻辑 IPJ，以支持对执行交互式证明的主体进行推理，并通过可忽略函数参数化分析概率增长，进而给出零知识证明的新概念。
2023-09-26 cs.LO
An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
微分线性逻辑丰富了线性逻辑与额外的逻辑规则的指数连接，对偶的通常规则的遗弃，削弱和收缩。本文提出了微分线性逻辑的证明网语法及其指称模型的范畴公理化。我们还介绍了一个简单的分类条件下，这些模型的一般反导数操作变得可用。最后，我们简要地描述了集合和关系的模型，并给出了有限性空间和线性和连续函数的模型更详细的说明。
2016-06-06 cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
A syntactic proof of decidability for the logic of bunched implication BI
本文通过证明论方法，给出了bunched implication逻辑BI可判定性的语法证明，提供了可实现的决策程序并界定了逻辑复杂性。
2026-01-03 cs.LO
Proof Normalisation in a Logic Identifying Isomorphic Propositions
我们定义了一个片段的命题逻辑同构命题，如$A\land B$和$B\land A$，或$A\Rightarrow (B\land C)$和$(A\Rightarrow B)\land(A\Rightarrow C)$被识别。我们定义了系统I，这个逻辑的证明语言，并证明其规范化和一致性。
2019-04-22 cs.LO
Proof-graphs for Minimal Implicational Logic
众所周知，命题经典证明的规模可能是巨大的。证明理论研究发现正常或切割自由证明和他们各自的非正常证明之间的指数差距。本文的目的是研究如何降低命题推理的权重。我们提出了形式主义的证明图的纯蕴涵逻辑，这是一个特定的形状，旨在捕捉演绎的逻辑结构的图形。这种形式主义的优点是公式可以在简化证明中共享。本文给出了最小蕴涵逻辑证明图的精确定义，并给出了证明图的规范化过程。与标准的树状形式主义相比，我们的规范化并没有增加节点的数量，当应用到相应的最小证明图表示。
2014-04-01 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
Focused Proof-search in the Logic of Bunched Implications
集束蕴涵（BI）逻辑自由地组合了加法和乘法连接词，包括蕴涵;然而，尽管其证明理论得到了充分的研究，但BI中的证明搜索一直是一个难题。聚焦原则是对证明-搜索空间的一种限制，它可以捕获各种目标导向的证明-搜索过程。在本文中，我们表明，集中的证明搜索是完整的BI首先重新制定传统的束的嵌套序列，使用更简单的数据结构，然后与极化和集中的变体，我们显示是健全的和完整的，通过削减消除参数。这建立了一个操作语义集中证明搜索的逻辑集束的影响。
2021-01-26 cs.LO
A Vernacular for Coherent Logic
我们提出了一个简单的，但表现力的证明表示，从不同的证明助手证明可以很容易地生成。该表示法只使用了少量的推理规则，并且基于一阶逻辑的一个片段，称为相干逻辑。融贯逻辑已经被许多研究者认为是一种适用于许多日常数学发展的逻辑。建议的证明表示是伴随着相应的XML格式和一套XSL转换生成正式的证明Isabelle/Isar和Coq，以及证明表示在一个自然语言的形式（在LATEX或HTML格式）。此外，我们的自动定理证明器的连贯逻辑出口证明建议的XML格式。所有的工具都是公开的，还有一组样本定理。
2014-05-14 cs.LO
Infinitary and Cyclic Proof Systems for Transitive Closure Logic
传递闭包逻辑是通过引入传递闭包算子而获得的一阶逻辑的已知扩展。虽然其他具有归纳定义的一阶逻辑的扩展是由一组归纳定义先验参数化的，但传递闭包算子的添加一致地捕获了所有有限归纳定义。在本文中，我们提出了一个无穷证明系统的传递闭包逻辑，这是一个无限下降式对应的现有（显式归纳）证明系统的逻辑。我们表明，作为一阶逻辑与归纳定义的类似系统，我们的无穷系统是完整的标准语义和包含显式系统。此外，传递闭包算子的一致性允许使用简单的语法标准来定义语义上有意义的完整限制。因此，对规则无穷（即循环）证明的限制为自动化归纳推理的有效系统提供了基础。
2018-06-28 cs.LO
Birkhoff style proof systems for hybrid-dynamic quantum logic
本研究基于混合与动态模态逻辑构建量子逻辑框架，提出量子子句概念及对应推理证明规则，验证了其可靠性与紧致性，并证明了该逻辑片段的Birkhoff完备性，为量子逻辑编程与形式规约提供理论支撑。
2024-06-19 cs.LO
Logical Pseudocode: Connecting Algorithms with Proofs
证明（微积分，自然演绎）和命令式算法（伪码）是两个众所周知的共存概念。那他们是什么关系？我们的答案是，\[ imperative\ algorithms\ =\ proofs\ with\ cuts \]这一观察导致一个推广的伪码，我们称之为{ \it逻辑伪码}。它类似于可计算性逻辑\cite{Jap03,Jap08}的自然演绎证明。其中的每一个陈述都对应于自然演绎中的一个证明步骤。因此，相对于伪代码，它的优点是保证每个语句相对于初始规范是正确和安全的。它也可以被看作是可计算性逻辑网（\colw）的扩展，具有正向推理能力。
2022-02-14 cs.LO
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
2000-06-05 cs.LO
A Heuristic Proof Procedure for Propositional Logic
定理证明是最古老的应用之一，它需要算法来修剪搜索空间。可逆证明程序一直是主要的工具。在本文中，我们提出了一种新的和强大的启发式称为$nongshim$，它可以被看作是可逆证明过程的基本原则。利用这种启发式方法，我们从命题逻辑中的逆演算导出了一个可逆的逆演算\cite{Ketonen,Troe}。
2022-02-22 cs.LO
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
有限迹上的时态逻辑与潜在无限迹上的时态逻辑不同。Rozelu首先证明了有限迹上线性时态逻辑（LTLf）的完备性，并提出了一个新的共归纳公理。我们提供了一个不同的证明，用更少，更传统的公理。我们的证明是Kröger和Merz的Henkin-Hasenjaeger式证明的直接改编。我们修改的本质是我们“注入”有限性：也就是说，我们改变证明结构以确保模型是有限的。我们的目标是提出一个全面的，可访问的证据。
2021-07-13 cs.LO
A Heuristic Proof Procedure for First-Order Logic
受{ \em可计算性逻辑} \cite{Jap03,Japic,Japfin}中讨论的有效证明过程的启发，我们描述了一阶逻辑的启发式证明过程。这是Gentzen证明系统的一个变体，具有以下特征：（a）它将序列视为机器与环境之间的游戏，（b）它将证明视为机器的获胜策略。从这个基于游戏的观点，一个强大的启发式可以被提取，并在证明搜索中可以获得相当程度的确定性。本文提出了一个关于一阶逻辑的新的演绎系统LKg，并证明了它的可靠性和完备性。我们还讨论了LKG '，一个变种的LKg与一些优化添加。
2018-02-09 cs.LO
Combinatorial Proofs and Decomposition Theorems for First-order Logic
我们发现一阶逻辑（不平等）的组合和语法证明之间的密切关系。虽然句法证明是在基于推理规则的演绎证明系统中形式化的，但组合证明是独立于任何推理规则集的证明的无语法表示。我们表明，这两个证明表示是相关的，通过一个深推理分解定理，建立了一种新的范式的语法证明。这就产生了（a）一阶组合证明的可靠性和完备性的简单证明，以及（b）一个完全完备性定理：每个组合证明都是一个句法证明的图像。
2021-04-27 cs.LO
Proof search for propositional abstract separation logics via labelled sequents
分离逻辑是霍尔逻辑的一个扩展族，用于对改变存储器的程序进行推理。这些逻辑是“抽象的”，因为它们独立于任何特定的具体内存模型。他们的断言语言，称为命题抽象分离逻辑，以各种方式扩展了（布尔）集束蕴涵（BBI）逻辑。我们发展了一个模块化的证明理论，各种命题抽象分离逻辑使用割自由标记的代数演算。我们首先扩展了Hou等人的BBI的割费标记的代数演算，通过添加部分确定性和可取消性的合理规则来处理Calcagno等人的分离代数的原始逻辑，同时保留割消除。我们通过一个合理的中间演算来证明我们演算的完备性，这个中间演算使我们能够从找不到证明的失败中构建反模型。然后，我们捕获其他命题抽象分离逻辑通过添加健全的规则不可分割的单位和不相交，同时保持完整性。我们提出了一个定理证明的基础上，我们的标记演算这些命题抽象分离逻辑。
2013-11-26 cs.LO
Cyclic Proofs, Hypersequents, and Transitive Closure Logic
我们提出了一个无割循环系统的传递闭包逻辑（TCL）的基础上的一种形式的超序列，适用于自动推理通过证明搜索。我们表明，以前提出的CRT-R系统的基本有效性从Kleene代数（KA）和命题动态逻辑（PDL），在标准的翻译是不完整的。另一方面，我们的系统忠实地模拟已知的循环系统KA和PDL，从而继承他们的完整性结果。我们的系统的一个特点是其更丰富的正确性标准，表现出“交替痕迹”，需要一个更复杂的合理性参数比传统的循环证明。
2022-05-17 cs.LO
Termination Proofs for Logic Programs with Tabling
表格逻辑编程在逻辑编程社区中越来越受到关注。它避免了SLD执行的许多缺点，并为逻辑程序提供了一种更灵活且通常非常有效的执行机制。特别地，逻辑程序的表格执行比基于SLD解析的执行更频繁地终止。在这篇文章中，我们介绍了两个概念的通用终止逻辑编程与Tabling：准终止和（更强的概念）LG终止。我们提出了这两个概念的终止，即准可接受性和LG-可接受性的充分条件，我们表明，这些条件也是必要的情况下，制表是精心挑选的。从这些条件出发，我们给出了模终止证明，即，证明能够组合单独程序的终止证明以获得组合程序的终止证明。最后，在模式信息的存在下，我们陈述了充分条件，这些条件构成了以基于约束的方式自动证明终止的基础。
2000-03-09 cs.LO
Six Proofs of Interpolation for the Modal Logic K
University of Amsterdam（阿姆斯特丹大学）；Utrecht University（乌得勒支大学）
本文通过不同方法展示了模态逻辑K的插值公理的六个证明，并比较了各方法的优劣。
2025-11-23 cs.LO
A general proof certification framework for modal logic
证明认证中的一个主要问题是，不同的定理证明器，即使是为相同的逻辑设计的，也倾向于使用不同的证明形式，并以不同的格式产生输出。ProofCert项目促进使用一种通用的规约语言和一个小而可信的内核，以便检查来自不同来源和不同逻辑的证明。依靠这一思想，并通过使用经典的集中式演算作为核心，我们在这里提出了一个通用的框架检查模态证明。我们提出了一个类似于Prolog语言的框架的实现，并展示了如何可以专门化它在一个简单的和模块化的方式，以涵盖不同的证明形式主义，如标记系统，tableaux，numericalculi和嵌套numericalculi。我们通过提供几个例子来说明逻辑K的方法，并讨论如何进一步扩展该方法。
2018-10-24 cs.LO
New Proofs of Weak Normalization for Propositional Logic
Chennai Mathematical Institute（钦奈数学研究所）
本文提出直觉主义自然演绎弱规范化的新证明，仅处理割，提供局部规则选择收缩或归约子证明，并在Lean中形式化，给出确定性算法。
2026-10-01 cs.LO
Proofs and Refutations for Intuitionistic and Second-Order Logic (Extended Version)
证明演算是一种类型化的证明演算，它利用证明和反驳概念之间的对偶性为经典命题逻辑提供计算解释。在这项工作中，我们将扩展Euda-Euda，以包括经典的二阶逻辑，通过将参数多态性和存在类型。该系统具有良好的计算性能，如类型保持，汇合，和强规范化，这是建立在通过reductionalargument。我们确定了一个句法限制的证明，其特点正是直观的片段的二阶dupda-dupta，我们研究规范的结果。
2022-10-13 cs.LO
Binding Logic: proofs and models
本文提出谓词逻辑的扩展“绑定逻辑”，允许变量在项和命题中被绑定，并通过将其编码回谓词逻辑证明了该逻辑的可靠性与完备性。
2023-05-25 cs.LO
(Co)inductive Proof Systems for Compositional Proofs in Reachability Logic
可达性逻辑是一种形式主义，可用于表达迁移系统的部分正确性。在本文中，我们提出了三个证明系统的形式主义，所有这些都是健全的和完整的，并继承了共归纳逻辑的性质。然而，证明系统在几个方面有所不同。首先，他们使用归纳和共归纳的比例不同。第二个方面是组合性，广义上意味着它们能够在较小的系统上证明更简单的公式，并将这些公式作为引理重用于较大的系统上的更复杂的公式。第三方面是它们的合理性证明的困难。我们发现，更多的归纳证明系统的使用，更专业的是它的使用coinduction（相对于我们的问题域），更组成的证明系统，但更困难的合理性证明变得。我们还简要地介绍了这些结果在Isabelle/HOL和Coq证明助手的机制。
2019-09-04 cs.LO
Automatic Generation of Proof Tactics for Finite-Valued Logics
现在有许多灵活的基于策略的逻辑框架，它们可以使用一种通用的高阶元语言来实现广泛的数学理论。作为证明助手，这种强大的系统的优点之一在于它们对推理能力的可扩展性的响应，其设计基于规则的程序设计语言，允许用户构建自己的“程序来构造证明”--所谓的证明策略。本贡献讨论了实现的算法，产生声音和完整的画面系统的一个非常包容的类充分表达有限值命题逻辑，然后说明了一些挑战和困难的算法形成的自动定理证明策略，这样的逻辑。我们将报告其实现的过程是基于证明系统的分析性的广义概念，旨在保证终止相应的自动化策略，这些策略涉及我们目标逻辑中的定理。
2010-03-25 cs.LO
On the role of connectivity in Linear Logic proofs
Université Paris Cité（巴黎西岱大学）；Università Roma Tre（罗马第三大学）
本文研究了线性逻辑证明中连通性的作用，提出了一种几何条件将必要性质转化为充分条件，从而为线性逻辑的片段提供正确性标准。
2026-02-06 cs.LO
Uniform Provability in Classical Logic
统一证明是微积分证明，具有以下特点：在证明的任何阶段，推导复杂公式的最后一步总是引入该公式的顶级逻辑符号。我们调查的相关性，这种统一的证明概念，在经典逻辑结构证明搜索。一种逻辑语言，其上下文可证明性等价于统一可证明性，它允许一个目标导向的证明过程，将逻辑符号解释为搜索指令，其含义由相应的推理规则给出。虽然这种统一的可证明性属性不直接适用于经典逻辑，但我们证明它适用于它的一个片段，该片段仅在对假设集进行适度的、合理的修改时排除全称量词的基本上为正的出现：向它们添加被证明的公式的否定。我们进一步注意到，所有使用添加的公式都可以分解为某些派生规则。由此产生的证明系统和统一的可证明性属性，它持有的是用来概述经典逻辑的证明过程。这个证明过程的一个有趣的方面是，它包含了以前提出的处理假设中的析取信息和处理假设的机制。我们的分析揭示了这些机制和统一证明的概念之间的关系。
1998-09-10 cs.LO
Canonicity of Proofs in Constructive Modal Logic
本文针对构造性模态逻辑中lambda演算与获胜策略间的证明等价性差距，通过扩充归约规则定义了新lambda演算，证明其规范化与合流性，并利用聚焦证明系统风格的类型系统建立了范式项与获胜策略间的一一对应关系。
2023-07-30 cs.LO
Categorical Proof Theory of Co-Intuitionistic Linear Logic
为了给余直觉主义逻辑提供范畴语义，人们必须面对特里斯坦·克罗拉德（Tristan Crolard）指出的事实，即把余指数定义为余积的集合在范畴集合中不起作用，其中余积是不相交的并集。遵循熟悉的直觉线性逻辑模型的构造与指数”！“，我们在具有附加结构的对称monoidal左闭范畴中建立了余直觉逻辑的模型，在自由范畴的构造中使用Crolard对余直觉逻辑的项赋值的一个变体.
2014-09-19 cs.LO
Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction
霍尔逻辑的证明表是一个带有前置和后置条件的带注释程序，它对应于霍尔逻辑的一棵推理树。在本文中，我们证明了部分正确性的证明表可以转化为一个推理序列的重写归纳约束重写。我们还表明，如果从程序获得的约束重写系统正在终止，则所得序列是对应于霍尔三重组的归纳定理的有效证明。这样一个有效的证明与终止的约束重写系统意味着完全正确的程序w.r.t.霍尔三人组转换，使我们能够应用技术证明终止约束重写证明总正确性的程序连同证明表格的部分正确性。
2018-02-19 cs.LO
The Foundation of a Generic Theorem Prover
Isabelle是一个交互式定理证明器，支持各种逻辑。它将规则表示为命题（而不是函数），并通过组合规则来构建证明。这些操作构成了一个元逻辑（或“逻辑框架”），其中对象逻辑被形式化。伊莎贝尔现在是基于高阶逻辑-一个精确和良好理解的基础。示例说明了使用此元逻辑来形式化逻辑和证明。一阶逻辑的公理被证明是可靠和完备的。后向证明通过关于对象级蕴涵的元推理形式化。高阶逻辑比其他元逻辑有几个实际的优势。许多证明技术是已知的，如休特的高阶统一程序。
2000-10-31 cs.LO
Proof Diagrams for Multiplicative Linear Logic
证明网的原始思想可以通过交互网语法来表达。为了保证证明结构和正确证明之间的对应性，需要额外的机制，如切换、跳转和图连通性。在本文中，我们给出了一个解释的证明网的语法字符串图。即使我们失去了标准的证明等价性，我们的结构允许定义一个框架，在这个框架中，可以在线性时间内验证图的合理性和良好类型。
2017-01-18 cs.LO
Multiplicative-Additive Proof Equivalence is Logspace-complete, via Binary Decision Trees
给定一个逻辑中提出的微积分，一个自然的问题是证明的等价性：以确定是否两个给定的证明是等同的任何指称语义，即任何类别的解释逻辑兼容其削减消除程序。这个概念通常可以通过一组规则排列在语法上捕获。非常一般地，证明网可以被定义为提供证明的等价类的规范表示的组合对象。特别地，逻辑的证明网的存在性提供了该逻辑的等价性问题的解决方案。在线性逻辑的某些片段中，可以给出具有良好计算性质的证明网的概念，使其成为研究割消过程的证明的合适表示。最近已经证明，对于线性逻辑的乘法（有单位）片段，不可能有这样一个证明网的概念，因为这个逻辑的等价问题是P空间完全的。研究线性逻辑中的乘加（无单位）片段，发现它与二进制决策树密切相关：建立了基于二进制决策树的证明表示，将证明等价约化为决策树等价，并给出了二进制决策树的逆编码作为证明.作为我们的主要结果，我们得到的证明等价问题的研究片段的复杂性是对数空间完全的。
2017-11-28 cs.LO
Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
Mechanizing Matching Logic In Coq
匹配逻辑是使用模式和模式匹配来指定和推理数学结构的形式体系。它越来越流行，已被用来定义许多逻辑系统，如具有递归定义的分离逻辑和线性时态逻辑。此外，它还作为K语义框架的逻辑基础，该框架用于为许多现实世界的语言构建实用的验证器。尽管匹配逻辑是一个容纳大量理论的基本形式系统，但它缺乏通用的、机器检查的形式化。因此，我们使用Coq证明助手来形式化匹配逻辑。具体来说，我们创建了一个新的表示匹配逻辑，使用本地无名编码，我们正式的语法，语义和证明系统，这种表示在Coq证明助手。最重要的是，我们证明了形式化证明系统的可靠性，并提供了一种在Coq中进行交互式匹配逻辑推理的方法。我们相信这项工作提供了一个以前未探索的途径推理匹配逻辑，其模型和证明系统。
2022-09-21 cs.LO
A Proof System with Names for Modal Mu-calculus
不动点是语义学、抽象解释和程序逻辑中的一个重要组成部分。它们添加到逻辑中可以增加相当大的表达能力。一个普遍的问题是如何定义这种逻辑的证明系统。在这里，我们将研究模态逻辑与不动点的证明系统。我们提出了一个Tableau证明系统，用于检查公式的有效性，它使用名称来跟踪不动点变量的展开，如Jungteerapanich所设计的。
2013-09-20 cs.LO
A Constructive Logic with Classical Proofs and Refutations (Extended Version)
我们研究了经典命题逻辑的保守扩展，区分了四种陈述模式：一个命题可以被肯定或否定，它可以是强的或经典的。强命题的证明在某种意义上必须是构造性的，而经典命题的证明则是通过矛盾来进行的。该系统，在自然演绎风格，被证明是健全的和完整的Kripke语义。我们从命题作为类型对应的角度出发，通过导出一个具有合流约简的项分配系统来发展该系统。强规范化的证明依赖于使用Mendler风格的递归转换到系统F。
2021-04-15 cs.LO
Certification of Prefixed Tableau Proofs for Modal Logic
不同的定理证明器倾向于以不同的格式产生证明对象，尤其是模态逻辑，其中已经提出了几种演绎形式主义（以及基于它们的证明器）。这项工作属于建立一个共同的规约语言，以证明在广泛的演绎形式主义的一般项目。特别是，通过使用从模态语言翻译成一阶极化语言和一个检查器，其小内核是基于一个经典的集中式微积分，我们能够证明模态证明标记的微积分，前缀tableaux和自由变量前缀tableaux。我们描述了逻辑K的一般方法，给出了它在一个类prolog语言中的实现，提供了一些例子，并讨论了如何将该方法扩展到其他正规模态逻辑
2016-09-14 cs.LO
A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
我们定义了PDL的无穷标号代数演算G3 PDL ^{ \infty }.然后给出了一个有限可表示的循环系统G3 PDL ^ω。我们表明，这两个是健全的和完整的PDL的标准模型，并进一步，G3 PDL ^{ \infty }是无割完全的。此外，我们还研究了证明搜索策略的循环系统的片段PDL没有测试。
2019-05-16 cs.LO
Proof Compression via Subatomic Logic and Guarded Substitutions
本文提出受保护替换机制，用于亚原子逻辑中的证明压缩，通过仅替换自由变量的受保护出现来构造推导叠加，实现无需切割规则即可p-模拟带替换的Frege系统。
2025-05-26 cs.LO
$\unicode{8523}$ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs
沿着Abramsky的“Proofs-as-Processes”程序的路线，我们提出了一个乘法线性逻辑作为并发函数编程的类型系统的解释。特别是，我们研究了线性多结论自然演绎系统，并表明它是同构的一个简单而自然的扩展$λ$ -演算的并行性和通信原语，称为$λ_{\unicode{8523}}$。我们将证明$λ_{\unicode{8523}}$满足类型化程序设计语言的所有理想属性：主题减少，进展，强规范化和汇合。
2019-07-08 cs.LO
Interaction and Depth against Nondeterminism in Proof Search
深度推理是一种证明理论方法，它概括了逻辑演算的标准推理概念，推理规则可以应用于逻辑表达式的任何深度。深度推理为不同逻辑的演绎系统的设计提供了更多的自由度，并提供了丰富的证明组合分析。特别是，指数较短的分析证明的建设成为可能，但成本更大的非决定性比微积分。在本文中，我们表明，证明搜索的不确定性可以减少而不会失去较短的证明，而不牺牲证明理论的清洁。为此，我们在逻辑表达式中采用了交互和深度方案。我们展示了我们的方法在乘法线性逻辑和经典逻辑的深度推理系统，讨论其证明复杂性及其与聚焦的关系，并提出了实现。
2014-05-28 cs.LO
Partial Regularization of First-Order Resolution Proofs
分解和叠加是现代定理证明器中广泛使用的命题和一阶逻辑的常用技术。在这些情况下，解决方案证明生产是这样的工具的一个关键特征;然而，它们产生的证明不一定尽可能简洁。对于命题归结证明，有各种各样的证明压缩技术。压缩自动定理证明器生成的一阶分辨率证明的技术较少。本文基于命题逻辑中的提升证明压缩思想，提出了一种压缩一阶逻辑证明的方法。一种用于命题证明压缩的方法是部分正则化，当推理$η$在从$η$到证明的根的每个路径中其主元文字已经作为另一推理的主元出现的意义上是冗余的时，其移除推理。本文描述了部分正则化算法的推广，从命题逻辑到一阶逻辑。广义算法进行部分正则化的决议证明包含决议和因式分解推理与统一。还提供了对广义算法及其与先前提升的GreedyLinearFirstOrderLowerUnits算法[12]的组合的经验评估
2018-04-18 cs.LO
Automata Theory Approach to Predicate Intuitionistic Logic
谓词直觉逻辑是依赖类型的一个很好的片段。根据Curry-Howard同构证明，逻辑中的构造与给定公式类型的程序综合有很好的对应。我们提出了一个模型的自动机，可以处理证明建设全直觉一阶逻辑。自动机是以这样一种方式构造的，即任何成功的运行都直接对应于逻辑中的正常证明。这使得讨论证明或程序的形式语言、自动机的闭包性质及其与传统逻辑连接词的联系成为可能。
2016-08-19 cs.LO
Formal Verification of Proofs from Automated Theorem Provers for Higher-Order Logic
Université Paris-Saclay（巴黎萨克雷大学）；ENS Paris-Saclay（巴黎萨克雷高等师范学院）；University of Greifswald（格赖夫斯瓦尔德大学）
本文提出一种在Dedukti框架中验证高阶逻辑自动定理证明器证明的通用方法论，应用于EP演算并集成至Leo-III，实现约80%证明步骤自动重构，成为首个支持独立可检查证明重构的高阶证明器。
2026-09-28 cs.LO
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
逻辑编程（LP）是一种基于一阶Horn子句逻辑的程序设计语言，它使用SLD-归结作为半决策过程。有限的SLD计算是归纳的声音和完整的最少Herbrand模型的逻辑程序。对偶地，SLD分解的共递归方法将无限SLD计算视为连续逼近程序的最大完全Herbrand模型中包含的无限项。在LP中实现协递归的最新算法基于循环检测。然而，这样的算法只支持推理的逻辑蕴涵合理的条款，他们没有考虑到生产力的重要性质，在无限的SLD计算。因此，循环检测落后于交互式定理证明（ITP）和项重写系统（TRS）中的共归纳方法。结构分解是一种新提出的替代SLD分解的方法，它可以定义和半决定一个适合于LP的生产力概念。在本文中，我们证明了健全的结构分辨率相对于Herbrand模型语义生产归纳，共归纳，混合归纳共归纳逻辑程序。我们介绍了两个算法，支持共归纳证明搜索无限生产条件。一个算法结合了循环检测的方法与生产性结构的解决方案，从而保证生产力的共归纳证明的无穷有理项。另一种则允许对无限非理性生产性术语的片段进行懒惰的合理观察。这使得LP中的共归纳方法与ITP和TRS中基于生产力的共归纳观察方法相提并论。
2017-05-04 cs.LO
Least and Greatest Fixed Points in Linear Logic
MALL（乘法，加法线性逻辑）的一阶理论仅在等式上是一个有趣但弱的逻辑，因为它不能捕获无界（无限）行为。而不是通过增加指数（！和？），我们添加最小和最大不动点算子。由此产生的逻辑，我们称之为muMALL，满足两个基本的证明理论性质：我们建立弱规范化，我们设计了一个集中的证明系统，我们证明完整的。第二个结果提供了一个强范式的无切割证明结构，可用于，例如，帮助自动化证明搜索。我们展示了如何将这些基础应用于直觉逻辑。
2010-11-30 cs.LO
