Apply2Isar: Automatically Converting Isabelle/HOL Apply-Style Proofs to Structured Isar
本文介绍了 Apply2Isar 工具，它能够自动将 Isabelle/HOL 中可读性较差的过程式"apply-style"证明脚本转换为更稳健且易读的声明式 Isar 证明，并通过在 Isabelle 形式化证明档案上的大规模评估验证了其有效性。
💻 Category
cs.LO
64 篇论文
The Unit Gap: How Sharing Works in Boolean Circuits
该论文证明了在允许自由反演的与 - 非门基下，布尔电路与公式的最小规模之差恒为 0 或 1（单位间隙定理），并揭示了共享机制仅在变量数达到特定阈值时生效，且当差值为 1 时仅由单个扇出为 2 的门通过特定复用方式产生。
Step Automata
本文针对现有文献中计算与并发结合研究的不足，提出了“步自动机”和“步图灵机”（STM）的概念，作为传统自动机和经典图灵机的自然扩展，允许其执行不含偏序关系的原子动作步骤。
Formalizing the stability of the two Higgs doublet model potential into Lean: identifying an error in the literature
本文通过将 2006 年关于两希格斯二重态模型（2HDM）势稳定性的经典论文形式化至 Lean 定理证明器，首次发现并证实了该文献中存在一个导致其核心定理失效的非平凡错误。
Central Limits via Dilated Categories
本文通过引入膨胀半范数增强范畴论作为统一框架，建立了一个抽象中心极限定理，不仅将经典中心极限定理和大数定律作为特例，还推导出了适用于辛流形观测量的新型中心极限定理，从而为统计推断及相关计算系统的理论分析提供了通用基础。
On the expressive power of inquisitive team logic and inquisitive first-order logic
本文证明了在询问团队逻辑中，开放公式的表达能力严格超越一阶逻辑，并进一步表明扩展该逻辑可表达有限性，而标准询问一阶逻辑的部分语句也能表达非一阶模型性质。
Towards a Higher-Order Mathematical Operational Semantics
本文通过将 Turi 和 Plotkin 的双代数抽象 GSOS 框架推广至高阶语言，建立了基于点状高阶 GSOS 律的抽象规范理论，从而为 SKI 演算和-演算等系统的组合性证明提供了通用的数学语义框架。
Consistency-based Abductive Reasoning over Perceptual Errors of Multiple Pre-trained Models in Novel Environments
该论文提出了一种基于一致性的测试时溯因推理框架，通过逻辑编程将多个预训练模型的预测及其错误检测规则编码，利用整数规划或启发式搜索算法在满足逻辑一致性约束的前提下最大化预测覆盖率，从而在分布偏移的新环境中有效缓解单一模型性能下降并提升整体精度与召回率。
A Graded Modal Type Theory for Pulse Schedules
本文提出了一种名为 GRAMPUS 的分级模态类型理论，利用代表时间信息的等级来形式化描述超导量子计算机的脉冲调度，并通过范畴论语义及语法模型证明了该语言在量子芯片输入信号模型中的完备性与可靠性。
The Skolem Problem in rings of positive characteristic
本文证明了在正特征有限生成交换环中，线性递归序列的零项判定问题（即 Skolem 问题）是可判定的，并指出其零集可表示为有限个-正规集的并。
WME: Extending CDCL-based Model Enumeration with Weights
本文提出了将权重传播、基于权重的剪枝及权重感知冲突分析融入时序与非时序回溯框架的 CDCL 算法，从而将加权模型枚举确立为求解器层面的原生推理任务，并系统探索了其在内存效率与剪枝效果之间的权衡。
A Formalization of Abstract Rewriting in Agda
本文在 Agda 证明助手中对抽象重写系统进行了构造性形式化，通过消除经典逻辑依赖、厘清不同终止性概念间的逻辑关系，并以此为基础对经典终止与合流准则进行了改进与推广，最后通过 lambda 演算的形式化展示了该框架的通用性。
Duality theory in linear optimization and its extensions -- formally verified
本文在 Lean 4 中形式化证明了线性有序域上的多个 Farkas 型定理，并将对偶理论扩展至允许系数取“无穷大”的情形。
Constraint satisfaction problems, compactness and non-measurable sets
该论文证明了有限关系结构若具有宽度一，则其紧性可在 ZF 公理系统中得证，否则其紧性将蕴含三维空间中非可测集的存在。
A Topological Rewriting of Tarski's Mereogeometry
本文利用 Coq 证明助手在 lambda-MM 库中扩展了 Tarski 的几何形式化，通过证明 mereological 类对应于正则开集，成功从单纯论框架推导出完整的拓扑空间，并在此基础上验证了 Tarski 几何公理系统的部分公理及其 Hausdorff 性质。
Can LLM Aid in Solving Constraints with Inductive Definitions?
该论文提出了一种将大语言模型与约束求解器相结合的神经符号方法，通过让大语言模型迭代生成辅助引理来辅助求解涉及归纳定义的约束问题，实验表明该方法能将相关证明任务的成功率提升约 25%。
Model Change for Description Logic Concepts
本文研究了描述逻辑概念在点式解释模型下的修改问题，区分了剔除、接收和修正三种操作，论证了修正不能简单归结为前两者的组合，并给出了针对EL和ALC逻辑中这些操作兼容性的正负结果。
Classical Explanations in (and of) General Probabilistic Theories
该论文在概率模型范畴中引入了“解释”的范畴论定义，证明了其可组合性，并指出每个局部有限概率模型都拥有一个典范的、尖锐的经典解释（即典范的经典表示）。
LTLGuard: Formalizing LTL Specifications with Compact Language Models and Lightweight Symbolic Reasoning
本文提出了 LTLGuard，一种结合约束生成与轻量级形式化一致性检查的模块化工具链，旨在利用资源高效的小型语言模型将非正式需求准确转化为无冲突的线性时序逻辑（LTL）规范。
Diagonalizing Through the -Chain: Iterated Self-Certification on Bounded Turing Machines and its Least Fixed Point
该论文通过域理论框架将受限自认证的时间开销转化为升链迭代，证明其斯科特极限（Scott limit）构成了描述机器完整停机行为的算子最小不动点，从而为停机问题提供了从有限可观测性到连续对角线延迟的新视角。