首页/论文/1208.1609

arXiv 1208.16092012-08-08cs.LO

复杂性证明的证明

Towards the Certification of Complexity Proofs

René Thiemann

备注：: Isabelle Users Workshop 2012, Associated with ITP 2012, http://www4.in.tum.de/~nipkow/Isabelle2012/

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们报告我们的形式化的矩阵解释在伊莎贝尔/HOL。矩阵需要证明终止证明，我们希望利用它们的复杂性证明，太。对于后者的目标，只有基本的方法已经被整合，我们讨论了一些即将出现的问题时，形式化更复杂的结果矩阵的解释，这是基于凯莱-汉密尔顿定理或联合谱半径理论。

英文摘要：

We report on our formalization of matrix-interpretation in Isabelle/HOL. Matrices are required to certify termination proofs and we wish to utilize them for complexity proofs, too. For the latter aim, only basic methods have already been integrated, and we discuss some upcoming problems which arise when formalizing more complicated results on matrix-interpretations, which are based on Cayley-Hamilton's theorem or joint-spectral radius theory.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

连接表的机器学习指导和证明认证

Machine Learning Guidance and Proof Certification for Connection Tableaux

连接演算允许目标导向证明搜索的非常紧凑的实现。我们给出了一个概述，我们的工作相关的连接表结石：首先，我们展示了优化的功能实现的子句和nonclausal证明搜索，包括一致的Skolemisation程序机器学习。然后，我们展示了两种基于机器学习的指导方法，即利用朴素贝叶斯概率对证明步骤进行重新排序，以及利用蒙特卡罗树搜索对证明搜索树进行扩展。最后，我们给出了一个翻译的连接证明LK，使证明认证和自动证明搜索的交互式定理证明。

2018-05-15cs.LO

一个通用的模态逻辑证明框架

A general proof certification framework for modal logic

证明认证中的一个主要问题是，不同的定理证明器，即使是为相同的逻辑设计的，也倾向于使用不同的证明形式，并以不同的格式产生输出。ProofCert项目促进使用一种通用的规约语言和一个小而可信的内核，以便检查来自不同来源和不同逻辑的证明。依靠这一思想，并通过使用经典的集中式演算作为核心，我们在这里提出了一个通用的框架检查模态证明。我们提出了一个类似于Prolog语言的框架的实现，并展示了如何可以专门化它在一个简单的和模块化的方式，以涵盖不同的证明形式主义，如标记系统，tableaux，numericalculi和嵌套numericalculi。我们通过提供几个例子来说明逻辑K的方法，并讨论如何进一步扩展该方法。

2018-10-24cs.LO

使用CeTA进行汇流证明

Certification of Confluence Proofs using CeTA

CeTA最初是作为一种工具开发的，用于认证必须以CPF格式提供的证书形式提供的终止证明。它的合理性被证明是IsaFoR的一部分，Isabelle形式化重写。到目前为止，CeTA还可以用于证明融合和非融合证明。在这个系统描述中，我们简要介绍了支持什么样的证明，以及证书中必须提供什么信息。正如我们将看到的，只需要少量的信息，因此我们希望CSI不会成为唯一可以生成证书的融合工具。

2015-05-06cs.LO

模态逻辑的前缀Tableau证明

Certification of Prefixed Tableau Proofs for Modal Logic

不同的定理证明器倾向于以不同的格式产生证明对象，尤其是模态逻辑，其中已经提出了几种演绎形式主义（以及基于它们的证明器）。这项工作属于建立一个共同的规约语言，以证明在广泛的演绎形式主义的一般项目。特别是，通过使用从模态语言翻译成一阶极化语言和一个检查器，其小内核是基于一个经典的集中式微积分，我们能够证明模态证明标记的微积分，前缀tableaux和自由变量前缀tableaux。我们描述了逻辑K的一般方法，给出了它在一个类prolog语言中的实现，提供了一些例子，并讨论了如何将该方法扩展到其他正规模态逻辑

2016-09-14cs.LO

认证扩展端接技术

Certification extends Termination Techniques

有一些终止证明是由终止工具生成的，对于这些工具，证明器的功能还不够强大。然而，类似的情况也发生在另一个方向。我们已经在更一般的设置中正式定义了终止技术，因为它们已经被引入。因此，我们可以使用到目前为止还没有终止工具支持的技术来证明证明。在本文中，我们将简要介绍其中的两种形式化：负常数多项式阶和北极终止。

2012-08-08cs.LO

认证问题格式

The Certification Problem Format

我们提供了一个CPF的概述，认证问题的格式，并解释了一些设计决策。而CPF最初是为了将三种不同的终止证明格式组合成一种格式而发明的，同时，术语重写系统的其他几个属性的证明也是可表达的：如汇合，复杂性和完成。因此，该格式已经得到了几个工具和认证器的支持。它的接受度也在国际比赛中得到了证明：终止和汇合比赛的认证赛道都使用CPF作为自动化工具和可信认证机构之间的交换格式。

2014-10-30cs.LO

更多相关论文收起更多论文

具有计算效果的程序认证

Program certification with computational effects

动态求值是计算机代数中的一种范例，它被引入用于代数数的计算。例如，在线性代数中，动态求值可以用于将为系数模为某个素数的矩阵编写的程序应用于系数模为某个合数的矩阵。在现代计算语言中实现动态求值的一种方法是使用语言提供的异常机制。在本文中，我们提出了一个证明系统的异常，其中包括提高和处理，通过扩展Moggi的方法基于单子。而且，这个证明系统的核心部分与祈使式语言中的状态效果证明系统是对偶的，后者依赖于comonad的范畴概念。这两个证明系统都在Coq证明助手中实现，它们被组合在一起，以便同时处理两种效果。

2014-11-26cs.LO

Theorema与Rocq中双边耐心排序的认证

Certification of Bilateral Patience Sort in Theorema and Rocq

Johannes Kepler University（约翰内斯·开普勒大学）；Université de Lorraine（洛林大学）

本研究对特定Patience Sort算法的递归优化过程进行形式化认证，对比Theorema与Rocq框架的实现差异，揭示算法设计对形式证明复杂度的影响。

2026-09-28cs.LO

UNSAT证明中的确定性

Determinism in the Certification of UNSAT Proofs

Inria Paris（法国国家信息与自动化研究所巴黎中心）；American University of Paris（巴黎美国大学）

对SAT求解器增加可信度的研究非常活跃，并使用各种方法。这些方法中的一些从证明者那里获得证明，然后检查它，通常是根据证明的信息复制搜索。因为认证过程涉及另一个重要的证明搜索，我们可以对它的信任降低了。一些试图修改这一使用证明人已验证了证明助理，如伊莎贝尔/HOL和Coq。我们的方法是不同的，因为它是基于一个非常简单的证明。该认证机构享有非常高的信任度，但效率非常低。在本文中，我们用这种方法进行了实验，并得出结论，通过对格式进行一些限制，可以基本上消除搜索的需要，并且原则上可以证明任意大小的证明。

2017-12-05cs.AIcs.LO

CeTA -一种用于认证端接分析的工具

CeTA - A Tool for Certified Termination Analysis

自2004年第一次终止竞争以来，人们非常感兴趣的是，由终止工具自动生成的证明是否确实正确。终止证明技术的数量的增加以及生成的证明的复杂性的增加（例如，几种技术的组合、穷举标记、树自动机等），进行认证（即，检查这些证明的正确性对于人类来说越来越乏味。因此，人们对终止证明的自动认证感兴趣。这导致了使用证明助手（如Coq和Isabelle）进行认证的一般方法。我们目前的最新发展IsaFoR/CeTA（版本1.03），这是认证CeTA，基于Isabelle/HOL形式化重写IsaFoR。

2012-08-08cs.LO

标准图灵模型中统一认证的局限性——语义不变量与可接受方法

Limits of Uniform Certification in the Standard Turing Model -- Semantic Invariants and Admissible Methods

研究标准图灵模型中统一证明生成方法的结构局限，将可接受方法形式化为生成器-验证器对，通过赖斯定理揭示对非平凡语义不变量认证的约束，应用此框架于相关语义不变量，表明标准模型中不存在统一可接受方法认证它们。

2026-09-14cs.LO

迈向 QBF 中的统一认证

Towards Uniform Certification in QBF

本文提出一种新技术，将策略提取与局部论证相结合，证明扩展 QBF Frege 可 p-模拟多种子句证明系统，从而支持 QBF 求解中的统一认证。

2024-02-12cs.CCcs.LO

非线性函数界的证明：模板法

Certification of Bounds of Non-linear Functions: the Templates Method

这项工作的目的是证明下界的实值多元函数，定义的半代数或超越表达式。最终，证书必须在Coq之类的证明系统中是可正式证明的。这种工具的应用范围很广，例如黑尔斯对开普勒猜想的证明就产生了数千个不等式。我们介绍了一种近似算法，它结合了最大加基方法（最优控制）和Manna等人开发的线性模板方法（静态分析）的思想。该算法包括在边界的一些成分的功能的上确界的二次形式具有良好的选择曲率。这导致半代数优化问题，解决平方和松弛。模板限制了这些弛豫的爆破，代价是使近似粗糙化。我们说明了我们的框架的效率，从文献中的各种例子，并讨论了与Coq的接口。

2013-07-10cs.LOcs.SC

实代数几何中的形式证明：从有序域到量词消去

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination

本文描述了离散实闭域在Coq证明助手中的形式化。这个抽象的结构捕捉例如实代数数的理论，一个具有良好算法性质的实数的可判定子集。实代数数和更一般的半代数簇的理论是实分析中许多有效方法的核心，包括非线性算术的决策过程或实值函数的优化方法。在定义了离散实闭域的抽象结构和多项式实根的基本理论之后，根据计算机代数中关于量词消去的标准文献，给出了一个基于伪余项序列的代数证明的形式化.这种形式化涵盖了理论的很大一部分，这是在计算机代数实践中实现的有效算法的基础。这项工作的成功为这些有效方法的正式认证铺平了道路。

2012-02-15cs.LO

安全的形式化

Formalization of security

Max Planck Institute for Security and Privacy（马克斯·普朗克安全与隐私研究所）；IMDEA Software Institute（IMDEA软件研究所）

本章围绕证明助手，介绍其在系统安全、基于语言的安全、安全编译、密码学领域用于验证安全属性及支持认证的应用。

2026-07-31cs.CRcs.LOcs.PL

组合原理的证明复杂性和二进制编码

Proof complexity and the binary encoding of combinatorial principles

我们认为证明的复杂性，根据不寻常的二进制编码的某些组合原则。我们对比证明复杂性与正常的一元编码在几个反驳系统，基于决议和非线性规划。请参阅文章的完整摘要。

2022-04-05cs.CCcs.LO

参数化证明复杂度和W[1]

Parameterized Proof Complexity and W[1]

我们启动了一个参数化证明复杂性的程序，旨在提供FPT不同于W[1]的证据。类似的程序已经存在于W[2]和W[SAT]类中。我们比较了这些程序，并证明了W[1]-参数化Resolution的上下界。

2012-03-23cs.CCcs.LO

代数证明复杂性：进展、前沿与挑战

Algebraic Proof Complexity: Progress, Frontiers and Challenges

我们调查最近的进展证明复杂性强证明系统及其连接代数电路复杂性，显示两者之间的协同作用如何产生新的方法来解决基本的开放问题，解决老问题，和新的研究方向。特别是，我们专注于证明复杂性下界（即某些重言式的证明大小的下界），代数电路下界和多项式身份测试问题从去随机化理论之间的紧密联系。

2016-07-02cs.CCcs.LOmath.LO

从代数电路复杂性证明复杂性下界

Proof Complexity Lower Bounds from Algebraic Circuit Complexity

我们给上和下界的子系统的电源的理想证明系统（IPS），代数证明系统最近提出的Grochow和Pitassi，其中的电路，包括证明来自各种限制代数电路类。这模仿了一个既定的研究方向，在布尔设置子系统的扩展弗雷格证明，证明线是电路从限制布尔电路类。除了一个，本文考虑的所有子系统都可以模拟研究充分的零星证明系统，在此之前，没有已知的下限时，测量证明大小的多项式的代数复杂性（除了相对于度，或稀疏性）。我们给出了两个一般的方法转换某些代数下界证明复杂性。我们的方法需要更强的概念下界，下界多项式以及整个家庭的多项式定义。我们的技术让人想起现有的方法转换成相关的证明复杂性的结果，如可行的插值布尔电路下界。我们获得了各种类别（稀疏多项式，深度3幂公式，只读一次遗忘代数分支程序和多线性公式）的相关类型的下界，并推断出相关的证明复杂性结果。我们补充我们的下限给出简短的反驳以前研究的子集和公理使用IPS子系统，使我们能够得出结论，这些子系统之间的严格分离。

2016-06-16cs.CCcs.LOmath.LO

Pebble游戏，证明复杂性和时空权衡

Pebble Games, Proof Complexity, and Time-Space Trade-offs

卵石游戏在20世纪70年代和80年代在许多不同的背景下被广泛研究。在过去的十年里，人们对卵石游戏的兴趣从证明复杂性的领域中复苏。Pebbling已被证明是一个有用的工具，用于研究基于分辨率的证明系统，比较不同子系统的强度，显示证明空间的界限，并建立大小空间的权衡。这是一个关于证明复杂性的研究的调查，利用了pebbling的结果和工具，重点是证明空间的下限以及证明大小和证明空间之间的权衡。

2013-09-20cs.CCcs.DMcs.LO