Tootfinder

Construction of a valued field whose valuation ring is definable but neither $\exists\forall\exists$ nor $ \forall\exists\forall$-definable in the language of rings
Mohsen Khani, Shaghayegh Shirani, Zahra Yadegari, Afshin Zarei
https://arxiv.org/abs/2508.06876

Construction of a valued field whose valuation ring is definable but neither $\exists\forall\exists$ nor $ \forall\exists\forall$-definable in the language of rings
We give an example of a valued field $(K,A)$ such that the valuation ring $A$ is definable by an $L_{\text{ring}}$-formula without parameters, but there is no $\exists\forall\exists$ or $\forall\exists\forall$-formula in $L_{\text{ring}}$ to define it.

Forall-Exists Relational Verification by Filtering to Forall-Forall
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann
https://arxiv.org/abs/2509.04777 https://

Forall-Exists Relational Verification by Filtering to Forall-Forall
Relational verification encompasses research directions such as reasoning about data abstraction, reasoning about security and privacy, secure compilation, and functional specificaton of tensor programs, among others. Several relational Hoare logics exist, with accompanying tool support for compositional reasoning of $\forall\forall$ (2-safety) properties and, generally, k-safety properties of product programs. In contrast, few logics and tools exist for reasoning about $\forall\exists$ propert…

Crosslisted article(s) found for cs.PL. https://arxiv.org/list/cs.PL/new
[1/1]:
- Forall-Exists Relational Verification by Filtering to Forall-Forall
Ramana Nagasamudram, Anindya Banerjee, David A. Naumann

Synthesis Benchmarks for Automated Reasoning
M\'arton Hajdu, Petra Hozzov\'a, Laura Kov\'acs, Andrei Voronkov, Eva Maria Wagner, Richard Steven \v{Z}ilin\v{c}\'ik
https://arxiv.org/abs/2507.19827

Synthesis Benchmarks for Automated Reasoning
Program synthesis is the task of constructing a program conforming to a given specification. We focus on deductive synthesis, and in particular on synthesis problems with specifications given as $\forall\exists$-formulas, expressing the existence of an output corresponding to any input. So far there has been no canonical benchmark set for deductive synthesis using the $\forall\exists$-format and supporting the so-called uncomputable symbol restriction. This work presents such a data set, compos…

How Hard is it to be a Star? Convex Geometry and the Real Hierarchy
Marcus Schaefer, Daniel \v{S}tefankovi\v{c}
https://arxiv.org/abs/2506.18818 https://…

How Hard is it to be a Star? Convex Geometry and the Real Hierarchy
A set is star-shaped if there is a point in the set that can see every other point in the set in the sense that the line-segment connecting the points lies within the set. We show that testing whether a non-empty compact smooth region is star-shaped is $\forall\mathbb{R}$-complete. Since the obvious definition of star-shapedness has logical form $\exists\forall$, this is a somewhat surprising result, based on Krasnosel'ski\uı's theorem from convex geometry; we study several related complexity …