A simple proof of the completeness of APAL
Philippe Balbiani, Hans van Ditmarsch
给出了任意公告逻辑APAL的完备性的一个简单证明.该证明是对出版物Knowable as Known after an Announcement中的证明的改进。
We provide a simple proof of the completeness of arbitrary public announcement logic APAL. The proof is an improvement over the proof found in the publication Knowable as Known after an Announcement.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)
本文提出完备性阈值作为桥梁，使有界证明能够推导出无界保证，并以冒泡排序为例说明只需考虑少数特定输入即可获得无界内存安全保证。
Completeness of Cyclic Proofs for Symbolic Heaps
分离逻辑在理论和实践上都是成功的软件验证方法。符号堆的判定过程是其中的关键问题之一。本文提出了一个具有一般形式归纳定义的符号堆循环证明系统，并证明了它的可靠性和完备性。最后给出了具有归纳定义的符号堆蕴涵的判定过程。具有归纳定义的符号堆的蕴涵的判定性是一个重要的问题。循环证明系统的完备性也是一个重要的问题。本文的结果回答了这两个问题。该判决过程是可行的，因为它是不确定的双指数时间复杂度。
Soundness and Completeness of a Model-Checking Proof System for CTL
提出一种用于 CTL 片段的局部模型检测证明系统，通过标记相继式保证终止性，并证明其可靠性、完备性及有限状态下的证明搜索终止性。
Light Affine Logic (Proof Nets, Programming Notation, P-Time Correctness and Completeness)
本文是一个结构介绍轻仿射逻辑，其直观的片段。轻仿射逻辑有一个多项式成本削减消除（P时间正确性），并编码所有P时间图灵机（P时间完整性）。通过引入直觉轻仿射逻辑的证明网，证明了P-时间正确性。P-Time的完整性通过一个非常紧凑的程序符号得到了充分的证明。一方面，P-Time正确性的证明描述了切割消除的复杂性是如何控制的，这要归功于利用证明网的结构属性的适当切割消除策略。这使得我们能够很好地理解“段落”模态的含义，这是轻逻辑的一个特点。另一方面，P-时间完备性的证明，以及大量的编程实例，给出了一个非平凡的任务，编程资源的限制，使用直觉轻仿射逻辑推导程序的味道。
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
有限迹上的时态逻辑与潜在无限迹上的时态逻辑不同。Rozelu首先证明了有限迹上线性时态逻辑（LTLf）的完备性，并提出了一个新的共归纳公理。我们提供了一个不同的证明，用更少，更传统的公理。我们的证明是Kröger和Merz的Henkin-Hasenjaeger式证明的直接改编。我们修改的本质是我们“注入”有限性：也就是说，我们改变证明结构以确保模型是有限的。我们的目标是提出一个全面的，可访问的证据。
On the meaning of logical completeness
哥德尔的完备性定理与可证明性有关，而ludics中的吉拉德定理（以及博弈语义学中的完全完备性定理）与证明有关。我们的目的是寻找这两个学科之间的联系。根据以前的工作[3]，我们考虑了具有收缩和普遍非决定论的原始ludics的扩展，它们发挥双重作用，以捕获线性逻辑的极化片段，从而捕获经典命题逻辑的构造性变体。然后，我们证明了一个完整性定理证明在这个扩展的设置：对于任何行为（公式）A和任何设计（证明尝试）P，要么P是A的证明，要么存在A的正交的模型M击败P。与博弈语义中的完全完备性证明相比，我们的证明与Goedel完备性证明有惊人的相似性，在这一点上，它明确地构造了一个基本上使用Koenig引理的反模型，通过归纳公式进行，并暗示了Loewenheim-Skolem定理的类似物。
Axioms vs. rewrite rules: from completeness to cut elimination
本文研究自动定理证明中证明搜索与重写结合时的完备性问题，指出其关键在于为演绎与计算结合的扩展证明概念建立切割消去，从而揭示自动定理证明与证明论之间的新联系。
A Henkin-style completeness proof for the modal logic S5
本文提出了一个最近的形式化的Henkin风格的完整性证明的命题模态逻辑S5使用精益定理证明。形式化的证明接近于Hughes和Cresswell的证明，但是这个系统基于不同的公理选择，更好地描述为一个Mendelson系统，增加了K，T，S4和B的公理方案，以及必要性规则作为推理规则。该语言有假和蕴涵作为唯一的原始逻辑连接词和必要性作为唯一的原始模态算子。完整的源代码可以在www.example.com上获得，并且已经使用Lean 3.4.2进行了类型检查。
Proof-Theoretic Soundness and Completeness
我们给出了一个演算推理的一阶片段的经典逻辑，这是足够的直觉Kripke框架的真值条件，并概述了证明理论的合理性和完整性证明，我们相信这是有利于自动化。
A New Proof of P-time Completeness of Linear Lambda Calculus
本文给出了线性λ演算的P-时间完备性的一个新的证明，该证明最初由H. 2003年的Mairson。我们的证明使用了与Mairson使用的类型本质上不同的布尔类型。此外，我们的证明的正确性可以使用标准ML的实现进行机器检查。
Birkhoff's Completeness Theorem for Multi-Sorted Algebras Formalized in Agda
这个文件提供了一个正式的证明伯克霍夫的完备性定理的多排序代数，其中指出，任何方程蕴涵有效的所有模型也是可证明的方程理论。更准确地说，如果某个方程在所有验证一组固定方程的模型中都是有效的，那么这个方程可以使用同余的证明规则从该组导出。该证明已在Agda版本2.6.2中正式化，并包含Agda标准库版本1.7，本文档复制了已注释的Agda代码。
On completeness of reducibility candidates as a semantics of strong normalization
本文定义了一个健全的和完整的语义标准，基于reductioncandidates，强规范化的理论表示在最小的演绎模LA咖喱。使用咖喱风格的证明条款允许建立这一标准的经典概念前海廷代数，并使该标准涉及所有的理论表示最小的演绎模。与使用Church风格的证明项相比，该方法提供了更简单的准则定义和更简单的完备性证明。
Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report
该早期技术报告首次研究内存安全性证明的完备性阈值，针对不分配/释放内存的数组遍历堆操作程序，提出将无界内存安全证明规约为有界证明的完备性阈值概念，并给出具体计算的初步思路。
The Completeness of Propositional Resolution: A Simple and Constructive<br> Proof
众所周知，归结方法（对于命题逻辑）是完备的。然而，在文献中发现的完备性证明使用了一个矛盾论证，表明如果一组子句是不可满足的，那么它必须有一个归结反驳。因此，这些证明实际上都没有给出一个从一组不可满足的子句中产生一个归结反驳的算法。本文给出了命题归结的完备性的一个简单的构造性证明，它包括一个算法和一个正确性证明。
On Statman's Finite Completeness Theorem
本文给出了Statman有限完备性定理及其推论（即$λ$-可定义性猜想蕴含高阶匹配猜想）的完整自洽证明。
Representation and duality of the untyped lambda-calculus in nominal lattice and topological semantics, with a proof of topological completeness
我们给出了一个语义的λ演算的基础上的拓扑对偶定理的名义集。一个新的解释lambda给出的伴随，和lambda-条款绝对解释为集（没有估值是必要的）。
Probabilistic Interval Temporal Logic and Duration Calculus with Infinite Intervals: Complete Proof Systems
本文给出了区间时态逻辑（ITL）和持续时间演算（DC）在无穷区间上的概率扩展，并给出了它们的完整的希尔伯特式证明系统。的完整性结果是一个强完备性定理的概率ITL系统相对于一个抽象的语义和相对完备性定理的概率DC系统相对于实时语义。所提出的系统subconsiderable概率实时DC从文献中已知的。所提出的系统之间的对应关系和系统的概率区间时态逻辑有限的时间间隔和扩展模态。
Verified completeness in Henkin-style for intuitionistic propositional logic
本文在Lean定理证明器中形式化并验证了Troelstra和van Dalen提出的直觉主义命题逻辑Henkin式完备性证明，是该方法下首个经机械验证的同类成果，源码已开源。
Intuitionistic Completeness of First-Order Logic
我们建立完整的直觉一阶逻辑，iFOL，表明一个公式是可证明的，当且仅当其嵌入到最小的逻辑，mFOL，是一致有效的下布劳威尔海廷柯尔莫哥洛夫（BHK）语义，预期的语义iFOL和mFOL。我们的证明是直观的，并提供了一个有效的程序Prf，统一的最小证据转换成一个正式的一阶证明。我们已经实现了Prf。一致有效性是使用交集运算符定义的，它是话语和原子谓词域上的通用量词。一致有效的iFOL公式也是直观有效的，但不是相反。我们最强的结果需要范定理，它也可以证明经典的显示，Prf终止使用柯尼希定理。我们的完备性定理背后的基本思想是，一个单一的证据项evd见证了最小逻辑公式F的一致有效性。即使找到一个一致的实现子也保证了直觉的有效性，因为Prf（F，evd）建立了F的一阶证明，建立了它的直觉有效性，并提供了一个纯粹的逻辑规范化实现子。我们为iFOL建立完整性如下。弗里德曼证明了iFOL可以通过他的A-变换嵌入到最小逻辑（mFOL）中，将公式F映射到FA。如果F是一致有效的，那么FA也是一致有效的，并且通过我们的完备性定理，我们可以在极小逻辑中找到FA的一个证明。然后我们从FFalse直观地证明F，即通过对A和mFOL的\bot取False。我们的结果解决了Beth在1947年提出的一个悬而未决的问题。
Hilbert-Post completeness for the state and the exception effects
在本文中，我们提出了一个新的框架来研究计算效果的句法完备性，我们将其应用到例外效果。当应用到国家的影响，我们的框架可以被看作是一个概括的Pretnar的工作在这个问题上。我们首先介绍一个相对概念的希尔伯特-波斯特完整性，非常适合的组合效果。然后，我们证明了异常效果是相对希尔伯特-波斯特完整的，以及“核心”的语言，可用于实现它，这些证明已被形式化，并检查与证明助手Coq。
Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof
本文提出一个更简单易懂的Kozen模态μ演算公理化系统完备性证明，基于Walukiewicz的原始证明进行改进。
Proof-Theoretic Functional Completeness for the Connexive Logic C
本文通过纯证明论方法，在双边主义框架下结合相干推理理解，证明了逻辑C联结词的功能完备性。
Simpler completeness proofs for modal logics with intersection
有一个显着的兴趣，扩大各种模态逻辑与交叉，最突出的例子是知识和doxastic逻辑与分布式知识。这种逻辑的完备性证明往往是复杂的，特别是在标准认知逻辑中的模型类，如S5，主要是由于标准模态逻辑中模态的交集的不可定义性。在[8]中概述了S5情况的标准证明方法，后来在[13]中更详细地解释，使用“解开折叠方法”的情况来实现树状模型以处理不可定义性问题。然而，由于细节水平和对S5的依赖，这种方法不容易适应其他逻辑。在本文中，我们提出了一个更简单的证明技术，通过建立一个树状规范模型直接，这避免了复杂的过程中解开和折叠。我们证明了技术，通过显示正常模态逻辑K，D，T，B，S4和S5扩展与交叉模态的完整性。此外，这些树型规范模型是兼容的Fischer-Ladner风格的闭包，我们结合的方法来显示所提到的逻辑的完整性进一步扩展与传递关闭的联合模态PDL或认知逻辑。其中一些完备性结果是新的。
Games and Full Completeness for Multiplicative Linear Logic
我们提出了一个游戏语义的线性逻辑，其中公式表示游戏和证明表示获胜的策略。我们表明，我们的语义产生一个范畴模型的线性逻辑和证明完全完备的乘法线性逻辑与MIX规则：每一个获胜的策略是一个独特的无割证明网的表示。{ \em history-free}策略的概念扮演了一个关键的角色;在无历史策略和交互作用几何之间建立了强有力的联系。我们的语义学结合了极性的自然概念，导致了添加剂的精细处理。我们与Joyal，Blass等人的相关工作进行了比较。
Completeness of Relational Algebra via Cylindric Algebra
本文通过 cylindric 代数方法重新证明了关系代数对一阶逻辑允许公式完备性，并提出一种生成等价关系表达式的新算法，为处理不完整或模糊信息的扩展提供基础。
On Star Expressions and Coalgebraic Completeness Theorems
一个开放的问题所提出的米尔纳要求证明，一定axiomatisation，米尔纳表明是健全的关于双相似性的正则表达式，也是完整的。这个问题的主要困难之一是缺乏一个完整的Kleene定理，因为有自动机，不能指定，直到双相似性，由一个表达式。Grabmayer and Fokkink（2020）证明了那些可以用正则表达式表示而不需要常数1的自动机，并使用这种特征来对Milner关于这个表达式子集的问题给出肯定的回答。本文从泛余代数的角度分析了Grabmayer和Fokkink关于完备性的证明，并由此抽象地说明了他们的证明方法。然后，我们比较这种证明方法的另一种方法，从共代数语言理论的完整性证明。这最终导致了两种抽象的完整性证明方法，我们称之为局部和全局方法，以及一种方法何时可以代替另一种方法的描述。
A formal proof of modal completeness for provability logic
本研究在HOL Light定理证明器中实现哥德尔-勒布可证性逻辑（GL）模态完备性的形式化证明，介绍实现细节与非标准证明结构选择，并分析该形式化系统推理的优缺点。
Combinatorial Proofs and Decomposition Theorems for First-order Logic
我们发现一阶逻辑（不平等）的组合和语法证明之间的密切关系。虽然句法证明是在基于推理规则的演绎证明系统中形式化的，但组合证明是独立于任何推理规则集的证明的无语法表示。我们表明，这两个证明表示是相关的，通过一个深推理分解定理，建立了一种新的范式的语法证明。这就产生了（a）一阶组合证明的可靠性和完备性的简单证明，以及（b）一个完全完备性定理：每个组合证明都是一个句法证明的图像。
Flat modal fixpoint logics with the converse modality
我们证明了一个通用的完整性结果，一类模态不动点逻辑对应于平面片段的双向μ演算，延长早期的工作Santocanale和Venema。我们观察到，Santocanale和Venema的证明，至少不动点的Lindenbaum-Tarski代数的某些平坦的不动点逻辑是建设性的，使用有限伴随，不再工作时，逆模态介绍。相反，我们的完整性证明直接构建了一个模型的一致性公式，使用归纳规则的方式是类似于标准的完整性证明命题动态逻辑。这种方法结合了焦点的概念，这是以前使用的基于表格的模态不动点逻辑推理。
Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
本论文提出两项贡献：一是用于公平调度下忙等待程序终止性验证的分离逻辑，二是将有界内存安全证明简化为有界证明的完备性阈值概念，并刻画了数组遍历程序的阈值。
Correctness and completeness of logic programs
讨论了定子句逻辑程序的正确性和完备性的证明。我们提出了一种方法来证明完整性，而证明正确性，我们采用了一种方法，应该是众所周知的，但往往被忽视。此外，我们展示了如何证明的完整性和正确性的存在SLD树修剪，并指出，近似规范简化规范和证明。我们比较证明方法声明式诊断（算法调试），表明近似规范消除了后者的一个主要缺点。我们认为，我们的证明方法反映了程序的自然声明性思维，它们可以正式或非正式地用于日常编程。
A Completeness Proof for A Regular Predicate Logic with Undefined Truth Value
我们提供了一个健全的和完整的证明系统Kleene的三元逻辑谓词的扩展。理论的概念是扩展的，对于每个函数符号，一个公式，指定何时定义的功能。“被定义”的概念通过一个简单的递归算法扩展到术语和公式。“已定义”公式的构造使得它们本身总是已定义的。完整性证明依赖于Henkin构造。对于每一个公式，公式、它的否定和它的“被定义”公式的否定之一在构造的模型上是真的。许多其他三进制逻辑在文献中可以减少到我们的。部分函数在计算机科学中无处不在，甚至在学校的方程求解中也是如此。我们的工作的动机是试图解释，正是在逻辑方面，典型的非正式方法的推理，在这样的应用。
Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics
研究了Burgess提出的优先条件逻辑PCL及其扩展.首先，一个自然语义的基础上的邻域模型，推广刘易斯的球模型的反事实逻辑，提出。直接证明了PCL及其推广的可靠性和完备性。然后介绍了该家族所有逻辑的标号微积分。该演算是模块化的，并具有标准的证明理论性质，其中最重要的是容许切割，这需要一个完整的演算的语法证明。通过采用一种通用的策略，根优先证明搜索终止，从而为PCL及其扩展提供了一个决策过程。最后，建立演算的语义完备性：从一个失败的证明尝试中的有限分支中，有可能提取出根节点的有限反模型。后一个结果给出了所有考虑的逻辑的有限模型性质的构造性证明。
Binding Logic: proofs and models
本文提出谓词逻辑的扩展“绑定逻辑”，允许变量在项和命题中被绑定，并通过将其编码回谓词逻辑证明了该逻辑的可靠性与完备性。
On Logic of Formal Provability and Explicit Proofs
1933年，哥德尔考虑了两种描述可证明性的模态方法。一个捕获了形式可证明性，并导致了逻辑GL和Solovay的完备性定理。另一种是以模态逻辑S4为基础，发展出阿特莫夫的证明逻辑LP。本文研究了作者提出的逻辑GLA，它是GL和LP语言的结合体。GLA具有Kripke风格的语义和相应的完备性定理。建立了GLA关于算术可证性语义的可靠性和完备性。
Proof-theoretic Semantics for First-order Logic
本文为一阶经典逻辑的证明论语义提供了一种初等、构造性且原生的完备性证明，并同时给出一阶直觉主义逻辑的可靠性与完备性证明。
Taming "McKinsey-like" formula: An Extended Correspondence and Completeness Theory for Hybrid Logic H(@)
本文通过改进文[8]中的算法hybrid-ALBA，将文[8]中的混合语言L（@）的归纳公式片段扩充为一个类McKinsey公式，并证明扩充类中的每个公式都有一个一阶对应.我们还确定了这个扩展归纳片段的一个子类，即扩展骨架公式，它扩展了[8]中的骨架公式类，每个公式都公理化了一个完整的混合逻辑。我们这里的证明方法是证明论的，遵循[10，19]和[3，第14章]，与[8]中的代数证明相反。
Towards the Automated Generation of Focused Proof Systems
本文处理的问题，制定和证明的完整性集中式证明系统在自动化的方式。聚焦是一门关于证明的学科，它将证明结构分成多个阶段，以减少证明搜索的非确定性。我们证明了，它是可能的构造一个完整的集中证明系统从一个给定的非集中证明系统，如果它满足一定的条件。我们的核心思想是推广基于Miller和Saurin给出的置换引理的线性逻辑证明系统的完备性证明。这是通过从证明系统的规则置换关系构建一个图来完成的，称为置换图。然后，我们表明，从一个给定的证明系统的置换图，它是可能的，以构建一个完整的集中证明系统，并另外推断哪些公式收缩是允许的。提供了一种用于构建系统的置换图的实现。我们应用我们的技术生成集中的证明系统MALLF，LJF和LKF的线性，直觉和经典逻辑，分别。
Model Theory and Proof Theory of Coalgebraic Predicate Logic
本文提出一种基于Set-余代数的通用对应语言，推广一阶逻辑，研究其公理化、完备性、表达能力及模型论性质，并建立相继式系统的消割结果。
Teaching a Formalized Logical Calculus
经典一阶逻辑在许多方面都是数学、语言学、计算机科学和人工智能的核心，因此有必要详细定义它。我们提出了合理性和完整性证明的一阶逻辑，形式化的互动证明助手伊莎贝尔/HOL的一个微积分。我们的形式化是基于Stefan Berghmann的工作，我们已经更新为使用Isabelle的声明式证明风格Isar（正式证明档案，条目FOL-Fitting，2007年8月/2018年7月）。我们用de Bruijn指数表示变量;这使得在量词下的替换对人类读者来说不那么直观。然而，与使用字符串表示的变量的替换实现相比，自然数的性质产生了一个优雅的解决方案。所考虑的微积分具有一个总是空的前件和一个在后件中的公式列表的特殊性质。我们得到的可靠性和完整性的证明，作为其tableau对应的逆对偶的派生结果的微积分。我们努力不仅提出的结果的合理性和完整性的证明，但也提供了一个深入到一个类似编程的方法，一阶逻辑语法，语义和微积分的形式化。我们在一门计算机科学专业的逻辑本科课程中使用了这种形式化，并讨论了我们的经验。
Complete Robust Hybrid Systems Reachability
本文提出鲁棒微分动态逻辑，证明其对混合系统可达性问题的绝对完备性，为精确语义的混合系统提供自动验证方法。
Soundness and Completeness of the NRB Verification Logic
这篇简短的论文给出了一个模型，并证明了确定性命令式程序的NRB验证逻辑的完整性，该逻辑在过去曾被用作大型，快速变化的开源C代码档案（如Linux内核源代码）的自动语义检查的基础。该模型是一个彩色的状态转换模型，从上面的一组可能的程序的过渡近似。相应地，逻辑捕获可能在程序中的给定点触发特定缺陷的所有跟踪，但也可能标记误报。
Dynamic Epistemic Logic with Communication Actions
这项工作提出了一个动态认知逻辑与通信动作，可以同时进行。与Ditmarsch、Hoek和Kooi提出的并发认知动作逻辑不同，这里的并发机制是所谓的真正并发，这里我们使用的是基于进程演算的方法，如CCS和CSP，以及动作模型逻辑。我们的方法使得证明的可靠性，完整性和可判定性，不同于其他的方法。我们提出了一个公理化，并表明，证明的合理性，完整性和可判定性，可以使用减少的方法。
Formal verification of a proof procedure for the description logic ALC
描述逻辑（DL）是一种用于以结构化和形式化的方式表示和推理应用领域知识的语言。为了实现这一目标，已经实施了几个证明器，如RACER和FaCT++，但这些证明器本身尚未获得认证。为了确保这些DL中推导的合理性，有必要正式验证这些推理机应用的推导。形式化方法为证明过程的规范和验证提供了强大的工具，其中包括证明过程的可靠性，完整性和终止性等属性的方法。在本文中，我们提出了一个证明过程的描述逻辑ALC的定义，基于语义tableau方法。我们通过使用Isabelle证明助手证明其可靠性、完备性和终止性来确保证明器的有效性。证明分为两个阶段进行，首先在抽象级别上建立这些属性，然后将它们实例化以用于基于列表的实现。
Sahlqvist-Type Completeness Theory for Hybrid Logic with Binder
在本文中，我们继续在\cite{Zh21c}的研究，发展的Sahlqvist型完备性理论的混合逻辑与满意运营商和向下绑定$\mathcal{L}(@, \downarrow)$。我们按照\cite{ConRob}中的思想定义了$\mathcal{L}(@, \downarrow)$的骨架Sahlqvist公式类，但是我们遵循了一种不同的证明策略，这是纯粹的证明理论，即对于每个骨架Sahlqvist公式$ϕ$及其混合纯对应$π$，$\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$证明了$π$，因此$\mathbf{K}_{\mathcal{H}(@, \downarrow)}+ϕ$相对于$π$定义的框架类是完备的，使用\cite{Zh21c}中定义的算法$\mathsf{ALBA}^{\downarrow}$的受限版本。
Set-Theoretic Completeness for Epistemic and Conditional Logic
在哲学和数学文献中，逻辑的标准方法是定义一种语言，这种方法也被计算机科学所采用（语法），一个适当的模型类以及语言中公式的解释（语义学），公理和推理规则的集合，表征推理（证明理论），然后通过可靠性和完整性结果将证明理论与语义联系起来。在这里，我们考虑一种在经济学文献中更常见的方法，它纯粹在语义，集合论层面上工作。我们提供了一些认知和条件逻辑的集合论完备性结果，并对比了句法和集合论方法的表达能力
Automated proof search system for logic of correlated knowledge
本文提出了相关知识逻辑的自动证据检索系统和可判定性。证明系统的核心是具有可靠性、完备性、截集规则和结构规则的可容许性以及所有规则的可逆性等性质的逻辑演算。证明搜索过程的基础上的微积分执行自动终止证明搜索，并允许我们实现相关知识的逻辑决策结果。
Syntactic completeness of proper display calculi
最近的一系列结构证明理论的研究旨在探索分析演算的概念（即那些支持通用和模块化证明策略的演算），并确定可以根据这些演算捕获的逻辑类。在这种情况下，Wansing引入了适当显示演算的概念，作为证明演算的一个可能的设计框架，其中以特别透明的方式实现了分析性需求。最近，可适当显示逻辑（即那些可以用适当显示演算等价表示的逻辑）的理论已经与广义Sahlqvist理论（又名统一对应）联系起来发展。具体地说，可恰当显示逻辑在句法上被刻画为那些由解析归纳公理化的逻辑，这些公理可以等价地和算法地转化为解析结构规则，从而得到的恰当显示演算具有一组基本性质：可靠性、完备性、保守性、割消和子公式性质。在这种情况下，证明给定的演算是完整的w.r.t.原始逻辑通常在语法上执行，即，通过示出在基本系统中存在逻辑的每个给定公理的（无割）推导，其中从给定公理算法生成的分析结构规则已经被添加到该基本系统中。然而，到目前为止，这种证明策略的语法完整性已经实现了个案的基础上，而不是一般。在本文中，我们解决这个差距，证明在任何正常的（分配）格扩展签名正确显示逻辑的语法完备性。具体来说，我们表明，对于每一个分析归纳公理的切割自由推导可以有效地产生具有特定的形状，被称为前范式。
Image Reflection on Process Graphs -- A Novel Approach for the Completeness of an Axiomatization of 1-Free Regular Expressions Modulo Bisimilarity
本文提出一种基于LLEE图“图像反射”现象的新方法，直接证明双模拟坍缩保持LEE/LLEE结构，从而为1-自由正则表达式模双相似性的公理系统完备性提供了新证明，并可简化相关正则表达式完备性证明中的图变换。
Uniform Algebras: Models and constructive Completeness for Full, Simply Typed λProlog
本文为λProlog语言基础逻辑HOHH建立模型论，证明消解的可靠性与完备性，并利用最小不动点及Lindenbaum代数变体给出构造性证明，同时提出新的切割消去方法。
Conceptual completeness for subgeometric logics
研究几何逻辑片段的“概念完备性”，通过理论与拓扑斯之间的对偶刻画，证明相干逻辑等片段在完整几何逻辑中保守嵌入，并等价于基于集合模型的传统重构定理。
Internal Languages for Thin Epsilon-Hyperdoctrines: Soundness, Completeness, and Rocq Formalization
该研究提出带希尔伯特ε算子的直觉主义内涵一阶逻辑的类型化证明项演算，证明其关于特定超教义模型的可靠性与完备性，相关成果在Rocq中形式化。
Abstract Canonical Inference
一个规范推理的抽象框架被用来探讨不同的证明顺序如何导致饱和度和完备性的不同变体。像完成，paramodulation，饱和，冗余消除和重写系统减少的概念连接到证明顺序。演绎机制的公平性是根据证明顺序来定义的，区别于产生完整性的（普通）“公平性”和产生饱和度的“均匀公平性”。
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逻辑的标准（显示）微积…
Finishing Oltean's Completeness Proof in Lean 4 for Hybrid Logic $L(\forall)$
本文在 Lean 4 中完成了混合逻辑 $L(\forall)$ 的机器检查完备性证明，通过结构新鲜性和存在引理 Henkin 构造两种工具解决了新鲜名称的生成问题。
Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory (Extended Version)
我们研究各种配方的完整性一阶逻辑措辞建设性类型论和机械化的Coq证明助手。具体而言，我们研究的经典和直觉主义的自然演绎和微积分的变种模型论，代数和博弈论语义的完整性。作为完整性方面的标准模型理论语义的塔斯基和Kripke是不容易建设性的，我们分析连接的完整性定理，马尔可夫原理和弱柯尼希引理，并讨论非标准的语义承认无故障的完整性。我们贡献了一个可重用的Coq库一阶逻辑包含本文所涉及的所有结果。
Some problems with two axiomatizations of discussive logic
本文讨论了Jakowski讨论（或话语）逻辑D2的两个公理化问题。最近的公理化D2和完整性证明相对于D2的预期语义似乎是错误的，因为一些公式有效根据预期的语义变成不可证明的。虽然没有提供新的公理化，也没有一个修复的完整性证明，这里发现的缺点可能是一个改进的公理化的一步。
Proof systems for partial incorrectness logic (partial reverse Hoare logic)
本文为部分不正确性逻辑（部分反向霍尔逻辑）定义了普通和循环两种证明系统，证明其可靠且相对完备，并通过循环不变式及循环证明转化方法完成完备性证明。
On correctness and completeness of an n queens program
Thom Frühlynth提出了一个简短，优雅和有效的Prolog程序的n皇后问题。然而，该程序可能会被视为相当棘手，人们可能不会相信它的正确性。本文以声明的方式解释了程序，并证明了程序的正确性和完整性。规范和证明是声明性的，即它们从任何操作语义中抽象出来。该规范是近似的，不需要精确地描述程序的语义。尽管该程序的工作在非地面条款，这项工作采用了标准的语义，基于逻辑后果和Herbrand解释。本文的另一个目的是提出一个关于逻辑程序语义的精确声明推理的例子。逻辑程序设计理论与实践（TPLP）
A comparison of three kinds of monotonic proof-theoretic semantics and the base-incompleteness of intuitionistic logic
本文比较可归约性语义与基语义（含Sandqvist变体）三种单调证明论语义，建立二者间的转换条件，并据此讨论直觉主义逻辑的基完备性问题。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。