paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Build your own clarithmetic I: Setup and completeness

构建你自己的 clarithmetic I:系统设定与完备性
LMCS vol.Volume 12, Issue 32017匹配度 2/10 · 论文属于计算逻辑/证明论与复杂度算术系统,讨论可靠性与完备性,与用户关注的静态分析、LLM/Agent 辅助形式化验证、浮点程序分析或贝叶斯程序分析无直接交集;仅在最广义的形式化验证与可计算性理论层面略有相关性。引用 6 inbox
Giorgi Japaridze
dblp: 2026-09-10crossref: 2026-09-10arxiv: 2026-09-10

AI 速览

一句话:提出参数化理论 CLA11,通过调参得到相对于三复杂度类的可靠且完备算术系统,并证明完备性。

论文研究基于可计算逻辑的 clarithmetic 数论:公式表示交互式计算问题,真即存在算法解;对解施加复杂度约束可得到不同版本。作者引入参数化系统 CLA11(P1,P2,P3,P4),其中 P1、P2、P3 分别控制振幅、空间与时间复杂度。近乎机械地调节前三个参数,可针对广泛的三复杂度类自动获得可靠且完备的理论:可靠指每个定理表示的问题都有该类中的解,且解可从证明自动抽取;完备指该类中每个可解问题都由某定理表示。调节 P4 可在放弃递归可公理化但保持简洁优雅的代价下,将外延完备性强化为内涵完备性。本文为第一部分,引入系统并证明完备性;可靠性留待第二部分。

问题
如何基于可计算逻辑,把交互式数论问题的可解性及其时间、空间与振幅复杂度约束,统一刻画为具有证明论完备性的算术理论。
方法
引入参数化/模式化系统 CLA11(P1,P2,P3,P4),通过近乎机械地调节 P1、P2、P3 实例化出面向不同三复杂度类的理论,并证明其完备性;P4 用于在放弃递归可公理化代价下强化完备性。
评估
以证明论方式论证:对广泛的三复杂度类,系统可靠且完备,且解可从定理证明中自动抽取;本文为第一部分,给出系统并证明完备性,可靠性证明见第二部分。
原文摘要(Abstract)

Clarithmetics are number theories based on computability logic (see http://www.csc.villanova.edu/~japaridz/CL/ ). Formulas of these theories represent interactive computational problems, and their "truth" is understood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a parameterized/schematic version CLA11(P1,P2,P3,P4). By tuning the three parameters P1,P2,P3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a wide range of target tricomplexity classes, i.e. combinations of time (set by P3), space (set by P2) and so called amplitude (set by P1) complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, furthermore, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The present Part I introduces the system and proves its completeness, while Part II is devoted to proving soundness.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{Japaridze15,
  title = {Build your own clarithmetic I: Setup and completeness},
  author = {Giorgi Japaridze},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 12, Issue 3},
  year = {2017},
  doi = {10.2168/lmcs-12(3:8)2016}
}