Finding Connections via Satisfiability Solving
本文提出了一种结合对称性破缺的 SAT 求解方法，通过三种不同的 SAT 编码将连接演算的搜索结构直接编码，并开发了新求解器 upCoP 以推动一阶逻辑自动证明的自动化进程。
💻 Category
cs.LO
64 篇论文
Commutation Groups and State-Independent Contextuality
该论文引入了用于研究态无关上下文性的“对易群”代数结构，通过字符串重写系统和广义泡利群表示，系统分析了上下文性见证的生成条件并构建了非上下文性赋值方案。
Online Monitoring of Metric Temporal Logic using Sequential Networks
本文提出了一种基于时序网络的统一在线监控框架，通过利用未来时间标记技术将度量时序逻辑（MTL）规范高效地转换为离散和稠密时间下的时序网络，从而在性能与可扩展性上优于现有方法。
Module checking of pushdown multi-agent systems
本文研究了推多代理系统（PMS）的模块检查问题，证明了针对 ATL 规范的检查是 2EXPTIME 完全的，而针对 ATL* 规范的检查则是 4EXPTIME 完全的，后者比前两者在计算复杂度上高出指数级，是少数具有初等但超过三重指数时间复杂度的自然判定问题之一。
The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness
本文通过 Lean 4 形式化证明揭示了在步长复制递归器中直接组合式终止度量存在的全局障碍，并展示了投影方法如何突破该限制，同时为受限安全片段提供了完整的机器验证归一化与一致性认证链。
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
本文提出了一种名为 MPBMC 的混合方法，利用图神经网络嵌入结合运行时设计统计信息对硬件属性进行功能聚类，从而显著提升了多属性有界模型检查（BMC）的验证效率。
Fusions of One-Variable First-Order Modal Logics
本文研究了单变量一阶模态逻辑的独立融合性质，证明了在不带等词的情况下，Kripke 完备性和可判定性在两种域语义下均得以保持，而引入等词或非刚性常元则会导致这些性质丧失，并进一步通过编码丢番图方程及将此类融合视为共享 S5 模态的命题模态逻辑融合，给出了完备性与可判定性传递的充分条件。
Complete Diagrammatic Axiomatisations of Relative Entropy
本文从范畴论视角出发，利用量化幺正代数和带量化等式的弦图语言，针对随机矩阵的两种自然幺正结构（克罗内克积与直和），给出了相对熵（包括 Kullback-Leibler 散度及任意阶 Rényi 散度）的完备公理化刻画。
Modal Fragments
本文系统综述了命题逻辑与模态逻辑中基于基限制的片段研究，通过借鉴 Post 格理论分析表达力与计算复杂度，整合了从任意模态公式定义的通用框架到由布尔函数与特定模态算子构成的“简单模态片段”这两条研究脉络，并探讨了相关片段的可教性与精确可学习性。
The Complexity of the Constructive Master Modality
本文通过引入语义定义的构造性主模态逻辑 和 ，利用其与 片段的翻译证明了这些逻辑具有指数大小有限模型性质且为 EXPTIME 完全，从而解决了 Afshari 等人关于其无菱形片段的猜想，并成功将 和 嵌入其中以确立其有效性问题的 EXPTIME 上界。
Constraint Learning for Non-confluent Proof Search
本文提出了一种用于经典一阶连接演算的约束学习机制，通过迭代优化约束语言，在保持完备性的同时显著减少了非合流表演算证明搜索中的回溯。
On Solving String Equations via Powers and Parikh Images
本文提出了一种结合字符串幂运算、广义 Parikh 映射和等式分解技术的创新方法，通过扩展 Nielsen 变换来求解复杂的字符串方程及 SMT 输入。
NL2GDS: LLM-aided interface for Open Source Chip Design
本文提出了 NL2GDS 框架，利用大语言模型将自然语言硬件描述自动转化为可综合 RTL 代码及 GDSII 版图，并通过开源 OpenLane 流程在基准测试中实现了显著的面积、延迟和功耗优化，从而加速了开源芯片设计并降低了 ASIC 设计门槛。
Reversible Computation with Stacks and "Reversible Management of Failures"
本文介绍了名为 SCORE 的语言，并通过证明辅助工具在特定状态空间中验证了栈操作为全双射函数，从而实现了将计算模型中的项解释为全双射函数，而非传统的部分双射函数。
Ohana trees, linear approximation and multi-types for the I-calculus: No variable gets left behind or forgotten!
本文通过引入一种能够追踪被隐藏或无限推远自由变量的“Ohana 树”概念，为I-演算建立了一种新的等价理论，并证明了其泰勒展开与 Ohana 树之间的交换定理，进而构建了一个基于非幂等类型系统和修正关系语义的指称模型以刻画该理论。
LeanTutor: Towards a Verified AI Mathematical Proof Tutor
本文提出了名为 LeanTutor 的概念验证系统，通过结合大语言模型的自然语言交互能力与 Lean 定理证明器的可验证性，构建了一个包含自动形式化、下一步生成及自然语言反馈模块的 AI 数学证明辅导工具，并引入了 PeanoBench 数据集用于评估。
The Geometry of Reasoning: Flowing Logics in Representation Space
本文提出了一种将大语言模型推理视为表征空间中逻辑流轨迹的几何框架，通过解耦逻辑结构与语义，证实了仅靠下一词预测训练即可使模型内化逻辑不变性，并揭示了可能独立于具体架构的通用表征规律。
Proof Strategy Extraction from LLMs for Enhancing Symbolic Provers
本文提出了 Strat2Rocq 框架，通过离线提取大语言模型的证明策略并将其形式化为 Rocq 引理，在在线阶段增强 CoqHammer 等符号证明器的自动化能力，从而在开源软件验证项目中显著提升了证明成功率。
SpotIt: Evaluating Text-to-SQL Evaluation with Formal Verification
本文提出了名为 SpotIt 的新评估流程，利用形式化等价验证引擎主动搜索能区分生成查询与真实答案的数据库，以克服现有基于测试的 Text-to-SQL 评估方法因偶然匹配而高估模型性能的局限性。
Formal that "Floats" High: Formal Verification of Floating Point Arithmetic
本文提出了一种结合分治策略、反例引导精化及人机协同 AI 辅助的扩展方法论，通过直接 RTL 到 RTL 的模型检查实现了对浮点运算的高效形式化验证，显著提升了覆盖率并减少了断言数量。