跳转至

文章背景与核心概要

本文介绍了首个使用 Rocq 证明助手对罗马诺夫三元组逻辑（Romanov's Triplet Logic, TLS）进行的机械化形式化工作。TLS 是一个基于三元组的组合框架，旨在推理分层三元组结构（称为紧凑三元组结构（CTS））中的兼容路径，并通过罗马诺夫有效过程（称为简单顶点交集（SVI））对其交集进行推理。该研究最初由布尔可满足性（SAT）驱动，形成了一个自包含的数学理论，此前其严格的形式化性质尚未得到确立。

作者在 Rocq 中实现了 TLS 核心的形式化（涵盖紧凑三元组公式、CTS、超结构、清除以及 SVI），验证了过滤阶段的多项式时间界限，并确立了滑动窗口和分组窗口翻译的精确正确性边界。此外，该工作引入了 VFR，这是一个提取出的 OCaml 原型，具有经过验证的判定过程、可靠的单向过滤器、Python 运行时以及作为 Zenodo 制品发布的、可复现的 Docker 封装。

Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas

Authors: Dmitry V. Alexandrov
Submitted: August 19, 2026
Primary Subject: Logic in Computer Science (cs.LO)
Additional Subjects: Artificial Intelligence (cs.AI), Computational Complexity (cs.CC), Programming Languages (cs.PL)
arXiv ID: 2608.18445 [cs.LO]

Formal Verification of Romanov's Triplet Logic: A Verified Filter for Sliding-window 3-CNF with Application to Structured Formulas

Authors: Dmitry V. Alexandrov
Submitted: August 19, 2026
Primary Subject: Logic in Computer Science (cs.LO)
Additional Subjects: Artificial Intelligence (cs.AI), Computational Complexity (cs.CC), Programming Languages (cs.PL)
arXiv ID: 2608.18445 [cs.LO]

Executive Summary

本文介绍了使用 Rocq 证明助手对罗马诺夫三元组逻辑（TLS）进行的首次机械化形式化。TLS 是一个基于三元组的组合框架，旨在推理分层三元组结构（称为紧凑三元组结构（CTS））中的兼容路径，并通过罗马诺夫有效过程（被称为简单顶点交集（SVI））来计算其交集。

Executive Summary

This paper presents the first mechanized formalization of Romanov's Triplet Logic (TLS) using the Rocq proof assistant. TLS is a triplet-based combinatorial framework designed to reason about compatible paths through layered triplet structures—known as Compact Triplets Structures (CTS)—and their intersection via Romanov’s Effective Procedure, referred to as Simple Vertex Intersection (SVI).

最初受布尔可满足性（SAT）的启发，TLS 构成了自包含的数学理论，而其严格的形式化性质此前尚未得到确立。作者在 Rocq 中将 TLS 的核心进行了形式化（涵盖紧凑三元组公式、CTS、超结构、清除过程以及 SVI），验证了过滤阶段的多项式时间界限，并为滑动窗口和分组窗口翻译确立了精确的正确性边界。此外，该研究引入了 VFR，这是一个提取出的 OCaml 原型，具备经过验证的判定过程、可靠的单向过滤器、Python 运行时环境，以及作为 Zenodo 制品提供的可复现 Docker 封装。

Originally motivated by Boolean satisfiability (SAT), TLS forms a self-contained mathematical theory whose rigorous formal properties had not been previously established. The author formalizes the core of TLS in Rocq (covering Compact Triplets Formulas, CTS, hyperstructures, clearing, and SVI), verifies polynomial-time bounds for filter stages, and establishes precise correctness boundaries for both sliding-window and grouped-window translations. Furthermore, the work introduces VFR, an extracted OCaml prototype featuring a verified decision procedure, a sound one-sided filter, a Python runtime, and a reproducible Docker packaging available as a Zenodo artifact.

Key Contributions & Technical Highlights

  • Rocq 中的机械化形式化：
  • 跨越 17 个文件的 23,000 多行代码。
  • 427 个已证明的引理和定理，且零未证明目标（admitted goals）。
  • 已形式化的核心理论：
  • 紧凑三元组公式（CTF）、紧凑三元组结构（CTS）、超结构、清除过程以及简单顶点交集（SVI）。
  • 正确性边界：
  • 证明了联合可满足集的存在意味着 SVI 的非空性，尽管逆命题在一般情况下不成立。
  • 证明了对于对齐结构，完全的双向蕴含关系得以恢复（这可推广到结构系统）。
  • 分组窗口分析：
  • 形式化了分组窗口翻译的可靠性，同时展示了一个具体的、关于其完备性的形式化反例。
  • 提取的制品（VFR）：
  • 一个提取出的 OCaml 原型，为滑动窗口片段提供了经过验证的判定过程，并为通用 3-CNF 提供了可靠的单向过滤器。
  • 随附 Python 运行时、Docker 支持以及针对随机和结构化实例的基准验证。

Key Contributions & Technical Highlights

  • Mechanized Formalism in Rocq:
  • Over 23,000 lines of code across 17 files.
  • 427 proved lemmas and theorems with zero admitted goals.
  • Core Theory Formalized:
  • Compact Triplets Formulas (CTF), Compact Triplets Structures (CTS), hyperstructures, clearing procedures, and Simple Vertex Intersection (SVI).
  • Correctness Boundaries:
  • Proves that the existence of a joint satisfying set implies the non-emptiness of SVI, though the converse does not hold generally.
  • Demonstrates that for aligned structures, a complete bi-implication is recovered (which extends to systems of structures).
  • Grouped-Window Analysis:
  • Formalizes the soundness of grouped-window translation while exhibiting a concrete formal counterexample to its completeness.
  • Extracted Artifacts (VFR):
  • An extracted OCaml prototype providing a verified decision procedure for the sliding-window fragment and a sound one-sided filter for general 3-CNF.
  • Packaged with a Python runtime, Docker support, and benchmark validations on random and structured instances.

Metadata & Reference Information

Metadata & Reference Information