Papers With

← All papers
First page of Revisiting average case complexity of multilevel syllogistic

Revisiting average case complexity of multilevel syllogistic

Lars Warren Ericson

cs.LO Jun 15, 2026 · v2 cs.CC
formalization verification logic
Read PDF arXiv abstract Code
TL;DR
Formalizes average-case complexity classes, MLS/EMLS syntax and semantics, and a partial decision procedure in Lean 4, with conditional hardness results.
Abstract
We describe a Lean 4 formalization revisiting NYU Courant Technical Report TR1995-711 on the average-case complexity of Multilevel Syllogistic (MLS). The development encodes Reischuk–Schindelhauer average-case classes, an axiomatic MLS/EMLS semantics layer, a partial Ferro–Omodeo–Schwartz decision procedure with proved soundness and partial completeness on a membership-free fragment, serialization and step budgets, and conditional NP-average completeness and non-AvP hardness corollaries modulo explicitly documented structural axioms. Full Lean sources are inlined in the appendix modules.
Problem

The 1995 Courant technical report TR1995-711 claims that Multilevel Syllogistic (MLS), EMLS, and FP/LP are NP-average complete, which implies super-polynomial average-case running times unless NEXP=EXP. Average-case complexity infrastructure does not yet exist in Mathlib, so these claims had never been machine-checked.

Approach

The authors encode Reischuk–Schindelhauer average-case classes in Lean 4: rank, Av(T), DistTime, AvP, distNP and distributional reductions, using finitely supported distributions. They give a deep embedding of MLS/EMLS syntax with axiomatic set semantics. On top of this they build a partial Ferro–Omodeo–Schwartz decision procedure, plus serialization, step budgets and NP membership of SatMLS. Hardness results are stated modulo explicitly documented structural axioms.

Results

Soundness and partial completeness of the decision procedure are proved on a membership-free fragment, and NP membership of SatMLS is proved via a checker. NP-average completeness and non-AvP hardness are obtained only as conditional corollaries that depend on the documented axioms. The full Lean sources are included in the appendix.