
TL;DR
This paper proves that the uniform one-dimensional guarded fragment has the Craig interpolation property and that its satisfiability problem is NEXPTIME-complete, advancing understanding of its logical and computational characteristics.
Contribution
It establishes the Craig interpolation property and complexity classification for the uniform guarded fragment, a natural extension of guarded two-variable logic.
Findings
Uniform guarded fragment has Craig interpolation property.
Satisfiability problem for the fragment is NEXPTIME-complete.
Provides complexity and logical property results for the fragment.
Abstract
In this paper we prove that the uniform one-dimensional guarded fragment, which is a natural polyadic generalization of the guarded two-variable logic, has the Craig interpolation property. We will also prove that the satisfiability problem of uniform guarded fragment is NEXPTIME-complete.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDNA and Biological Computing · Formal Methods in Verification · semigroups and automata theory
