Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops

2025/04/29 by Nakamura, Yoshiki
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2504.20415

Abstract

We show that the emptiness (unsatisfiability) problem is undecidable and \mathrmΠ⁰₁-complete for deterministic propositional while programs with (graph) loop. To this end, we introduce a hypothesis elimination using loops. Using this, we give reductions from the complement of the periodic domino problem. Moreover, as a corollary via hypothesis eliminations, we also show that the equational theory is \mathrmΠ⁰₁-complete for the positive calculus of relations with transitive closure and difference. Additionally, we show that the emptiness problem is PSPACE-complete for the existential calculus of relations with transitive closure.

Related

• Existential Calculi of Relations with Transitive Closure: Complexity and Edge Saturations
• Elementary Sets for Logic Programs
• On P Versus NP
• Proving Program Properties as First-Order Satisfiability
• The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete