Maslov's class K with Equivalence

Oskar Fiuk

Home/Archive/arXiv

arXiv · 2610.06493

Maslov's class K with Equivalence

Oskar Fiuk

View original source ↗Read source document ↗Export metadata ↓

Abstract

Maslov's class K is a decidable fragment of equality-free first-order logic. It subsumes numerous classical decidable fragments, including the equality-free monadic fragment, the equality-free two-variable fragment, and the Gödel class. Introduced over 50 years ago, the class K has been studied in automated deduction, primarily through resolution-based methods. Despite this long history, the precise complexity of the satisfiability problem for K remained open until recently, when NExpTime-completeness was finally established. The two main contributions of this work are as follows. 1. The recent proofs of NExpTime-completeness and the finite model property for K are highly non-trivial and technically sophisticated. We present considerably simpler proofs of both results. Our approach combines a novel reduction from K to the class of solvable Skolem sentences with a randomised construction of finite models. 2. We introduce the class K+E by allowing sentences in K to contain one distinguished binary predicate E whose interpretation is constrained to be an equivalence relation. By leveraging our approach to this extended class, we prove that K+E has the finite model property and that its satisfiability problem is 2-NExpTime-complete.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeX RIS

Oskar Fiuk. 2026-10-05. Maslov's class K with Equivalence. https://arxiv.org/abs/2610.06493

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Coslice Colimits in Homotopy Type Theory

We contribute to the theory of (homotopy) colimits inside homotopy type theory. The heart of our work characterizes the connection between (graph-indexed) colimits in a type universe and colimits in coslices of the universe, called coslice colimits. To derive this characterization, we give a construction of coslice colimits that is tailored to reveal the connection. We use the construction to prove that the forgetful functor from a coslice creates colimits over trees. We also use it to study how coslice colimits interact with orthogonal factorization systems and with cohomology theories. As a result of their interaction with orthogonal factorization systems, all colimits of pointed types preserve $n$-connectedness, which implies that higher groups, in the sense of Buchholtz, van Doorn, and Rijke, are closed under colimits. We have formalized major portions of this work (see https://github.com/PHart3/colimits-agda for the Agda code), including our main construction of the coslice colimit functor.

cs.LO↗

arXiv2026

Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents

We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central problems, which we call "cycle recognition" and "unraveling." Cycle recognition concerns identifying cycles in non-wellfounded proofs in order to extract corresponding cyclic proofs, while unraveling studies the converse transformation, from cyclic proofs to non-wellfounded ones. Although these processes are well understood for Gentzen sequents, they have received little attention for more expressive sequent formalisms and become more challenging in the linear nested sequent setting. To address cycle recognition, we show the completeness of non-wellfounded proofs relative to a particular normal form exhibiting a property we call "saturation recurrence," which enables the systematic extraction of cyclic proofs. To address unraveling, we introduce a specialized procedure that shifts rule applications forward along linear nested sequents, allowing non-wellfounded proofs to be reconstructed from cyclic ones. Overall, our work provides new proof-theoretic techniques for cycle recognition and unraveling in expressive multisequent formalisms.

cs.LO↗

arXiv2026

Decreasing Diagrams are Complete for Confluence

Confluence is a fundamental property of nondeterministic computations, arising from parallelism, concurrency, or freedom in the evaluation order. It guarantees that such a computation always yields the same result, regardless of the order in which steps are taken. The decreasing diagrams technique of van Oostrom is one of the most versatile methods for establishing confluence of transition systems (abstract rewriting systems). It reduces global confluence to local confluence: a system is confluent whenever its transitions admit a locally decreasing labeling. Essentially all classical confluence criteria arise as corollaries. A central question, posed by van Oostrom in 1993, asks whether the decreasing diagrams technique is complete: Does every confluent transition system admit a locally decreasing labeling? This is Problem 56 of the RTA List of Open Problems. A positive answer was known only for countable systems, and recently up to the first uncountable cardinal $\aleph_1$. The general case remained open. We settle this thirty-three-year-old problem in full. We prove that every confluent transition system admits a locally decreasing labeling using only three labels. This bound is optimal, as two labels do not suffice even at the first uncountable cardinality. It follows that this single criterion can, in principle, certify the confluence of every confluent system, and hence of every confluent program. The entire development is machine-checked in the Isabelle/HOL and Lean proof assistants and relies only on classical logic and the axiom of choice.

cs.LO↗