5 papers · 1 filter
A Fine-Grained Dichotomy for Bounded-Variable Query Evaluation: The Calculus of Relations, a Boolean Modal Logic, and One-Variable Counting Logic
Yoshiki Nakamura, Yuya Uezato
We study the fine-grained complexity of evaluating Boolean bounded-variable first-order queries over sparse relational structures. For every fixed , every relational signa…
An Exponential Succinctness Gap between Three-Variable Logic and the Calculus of Relations
Yuya Uezato
Three-variable first-order logic (FO3) and the calculus of relations (CoR) define the same binary queries, an equivalence going back to Tarski in the 1940s. While the classical tra…
On the Complexity of the Matching Problem of Regular Expressions with Backreferences
Soh Kumabe, Yuya Uezato
ReDoS is a well-known type of algorithmic complexity attack, where an adversary supplies maliciously crafted strings to a regular expression matching engine, aiming to exhaust comp…
Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Models
Sho Sonoda, Shunta Akiyama, Yuya Uezato
Agentic theorem provers combine a reasoning model, retrieval, search, and a proof assistant verifier, yet it remains unclear which components actually improve finite-budget proof s…
Exponential Sample Complexity Separation between Flat and Hierarchical Agentic Theorem Provers
Sho Sonoda, Shunta Akiyama, Yuya Uezato
Agentic theorem provers often introduce intermediate lemmas, proof sketches, or subgoal decompositions before returning to tactic-level search. This can look like an expensive deto…