发表机构
HSE University（高等经济大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
研究在Rocq中首次形式化验证罗马诺夫三元组逻辑，实现滑动窗口3-CNF的已验证过滤器，给出正确性边界，开发VFR原型并通过基准测试验证，完整工具链已公开。
AI 中文摘要
我们在Rocq证明辅助工具中首次实现了罗马诺夫三元组逻辑（TLS）的机械化形式化。TLS是一种基于三元组的组合框架，用于推理分层三元组结构（称为紧凑三元组结构（CTS））中的兼容路径及其通过罗马诺夫有效程序（我们称之为简单顶点交集（SVI））的交集。TLS最初由布尔可满足性问题驱动，构成了一套此前尚未建立形式化性质的自包含数学理论。我们在Rocq中形式化了TLS的核心内容，包括紧凑三元组公式（CTF）、CTS、超结构、清除操作和SVI。针对良构的滑动窗口片段，我们验证了逐子句的CNF到CTF的翻译、清除程序和对齐交集，并证明了过滤器阶段的显式多项式时间边界。我们的主要贡献是精确的正确性边界：存在联合可满足集合意味着SVI非空，但反之在一般情况下不成立；对于对齐结构，我们恢复了完全双向蕴含，并将其扩展至结构系统。我们还形式化了分组窗口翻译的可靠性，并给出了其完备性的形式化反例。我们引入了VFR，这是一个提取的OCaml原型，为滑动窗口片段提供已验证的判定程序，为一般3-CNF提供可靠的单侧过滤器，配有Python运行时和可复现的Docker打包。对随机实例和结构化实例的基准测试证实了预测行为，完整工具链作为整理后的Zenodo制品可用。该Rocq开发包含17个文件中超过23000行代码，有427个已证明的引理和定理，且无承认目标。
英文摘要
We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a combinatorial framework originally motivated by Boolean satisfiability, based on triplet structures and a filter that we call Simple Vertex Intersection (SVI). We formalise the core of TLS, including its translation from 3-CNF, the clearing procedure, and the SVI algorithm. For the well-formed sliding-window fragment, we prove explicit polynomial-time bounds for the filter stages and verify the translation and intersection operations. Our main contribution is a precise correctness boundary: for general formulas, SVI non-emptiness is necessary but not sufficient for satisfiability; for aligned structures, we prove a full bi-implication, extended to systems of structures. We also formalise the grouped-window translation and provide a formal counterexample to its completeness. We introduce VFR (Verified Filter for Romanov's triplet logic), an extracted OCaml prototype that implements a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, with a Python runtime and Docker packaging. Benchmarks corroborate the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises over 23,000 lines of code, with 424 proved lemmas and no unproved assumptions.
Comments33 pages, 3 figures, 2 tables, 2 listings, 19 references. v3: updated Zenodo links to point to the latest version of the code artifact (Concept DOI: 10.5281/zenodo.20397949)
