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

Verification of a DPLL Transition System in Rocq

We present a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwenhuis et al., SAT solving is modeled as a set of rule-based transitions between states rather than as a concrete algorithm. We formalize the syntax and semantics of propositional formulas, define the classical and base DPLL transition systems, and prove their key metatheoretic properties. In particular, we establish correctness and completeness with respect to satisfiability, and we prove termination by showing that the transition relation is well-founded. The formalization extends the original abstract system by also including the pure literal rule. Building on the verified transition system, we introduce an abstract notion of strategy and derive a terminating solver from any strategy satisfying suitable conditions. We then implement a concrete strategy in Rocq and show that it satisfies the strategy specification.

STLSat---An Improved Tableau for Satisfiability Checking of Signal Temporal Logic Formulas

Signal Temporal Logic (STL) is a formalism used to describe temporal properties of real-valued signals in cyber-physical systems. In mission- and safety-critical domains, specifications often consist of large collections of STL formulas, making consistency checking and requirement analysis a major engineering bottleneck. Despite tableau-based satisfiability procedures being a natural solution to solve this problem, we have recently found out that the only existing tree-shaped tableau for bounded discrete-time STL does not provide a sound satisfiability/unsatisfiability verdict for all possible STL formulas. In this paper, we pinpoint the flaw in that procedure and present a new tree-shaped tableau which we prove to be sound and complete for bounded discrete-time STL. On top of this theoretical foundation, we introduce STLSat, an open-source Rust tool that decides the satisfiability of STL formulas, synthesizes concrete witness signals, checks the logical implication and equivalence between specifications, and extracts unsatisfiable cores, allowing users to identify inconsistent subsets of requirements for more effective specification debugging. STLSat also implements enhanced First-Order Logic and Satisfiability Modulo Theories encodings for STL, which allow it to act as a portfolio solver. We evaluate STLSat on an extended benchmark suite (including STL and Mission-time Linear Temporal Logic formulas) that we release publicly. Across the whole benchmark, the portfolio solver matches or outperforms state-of-the-art tools while preserving correctness guaranteed by our sound tableau procedure.

New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations

Sequent-style tableaux for first-order logic: structural analysis, cut admissibility, and the correspondence with LK

We give a self-contained development of the first-order block calculus in unsigned sequent-style notation: each node of the refutation tree carries a finite block $\Pi = \Gamma \cup \neg[\Delta]$, negation is governed by explicit rules, and a branch closes on a complementary pair of literals. The calculus is Smullyan's, and so in substance are the theorems; what is offered here is a different arrangement of them. The structural properties are established in the order of dependence familiar from G3-style sequent calculi: closure on arbitrary formulae is admissible, weakening and the substitution of parameters are admissible with preservation of the height, every rule is height-preserving invertible, and cut is admissible, the last being derived from the first three rather than conversely. Soundness, completeness under a fair strategy, countable compactness and the countable model property follow, together with a syntactic criterion under which every fair construction terminates. The correspondence is then proved, in both directions and with cut included, with Gentzen's LK in its usual presentation with explicit weakening, which requires lemmas on parameters that set-based Gentzen systems do not need.

From Dag-Like Proofs to Boolean Circuits in Lean

In this article, we present a method for encoding Dag-Like Derivability Structures (DLDS), obtained via horizontal compression of Natural Deduction proofs in purely implicational minimal logic, as Boolean circuits. These DLDS compress Natural Deduction tree-like proofs into directed acyclic graphs, preserving logical correctness while reducing redundancy. We formally define the circuit construction process and establish its pointwise correctness, showing that, for any fixed path assignment, the resulting Boolean circuit agrees with the intended dependency-propagation semantics. A Lean formalization establishes machine-checked guarantees for the circuit evaluator and includes a restricted bridge for the uncompressed simple-tree fragment, connecting valid DLDS instances in that fragment to genuine circuit acceptance of their extracted paths under the route and discharge conditions formalized in Lean. This approach opens new perspectives for automated theorem proving and formal certification.

A Rocq Prover STL Formalization with Transformations for Mission Planning