Search papers, labs, and topics across Lattice.
This paper presents the first mechanized formalization of Romanov's Triplet Logic (TLS) within the Rocq proof assistant, establishing its formal properties and verifying key processes such as the CNF-to-CTF translation and the clearing procedure. The authors demonstrate that while the existence of a joint satisfying set guarantees non-emptiness of the Simple Vertex Intersection (SVI), the reverse is not universally true, highlighting a nuanced correctness boundary. Additionally, they introduce VFR, an OCaml prototype that serves as a verified decision procedure for the sliding-window fragment and a sound filter for general 3-CNF, supported by extensive benchmarks and a reproducible toolchain.
A nuanced correctness boundary in Romanov's Triplet Logic reveals that a satisfying set does not guarantee a non-empty intersection, challenging existing assumptions in Boolean satisfiability.
We present the first mechanised formalisation of Romanov's Triplet Logic (TLS) in the Rocq proof assistant. TLS is a triplet-based combinatorial framework for reasoning about compatible paths through layered triplet structures, called Compact Triplets Structures (CTS), and their intersection via Romanov's Effective Procedure, which we refer to as Simple Vertex Intersection (SVI). Originally motivated by Boolean satisfiability, TLS constitutes a self-contained mathematical theory whose formal properties had not been previously established. We formalise the core of TLS in Rocq, including Compact Triplets Formulas (CTF), CTS, hyperstructures, clearing, and SVI. For the well-formed sliding-window fragment we verify a clause-by-clause CNF-to-CTF translation, the clearing procedure, and aligned intersection, and we prove explicit polynomial-time bounds for the filter stages. Our main contribution is a precise correctness boundary: the existence of a joint satisfying set implies non-emptiness of SVI, but the converse does not hold in general; for aligned structures we recover a complete bi-implication, extended to systems of structures. We also formalise soundness of grouped-window translation and exhibit a formal counterexample to its completeness. We introduce VFR, an extracted OCaml prototype that provides a verified decision procedure for the sliding-window fragment and a sound one-sided filter for general 3-CNF, with a Python runtime and reproducible Docker packaging. Benchmarks on random and structured instances confirm the predicted behaviour, and the complete toolchain is available as a curated Zenodo artifact. The Rocq development comprises more than 23,000 lines of code across seventeen files, with 427 proved lemmas and theorems and zero admitted goals.
