5 papers
A Complete Propositional Dynamic Logic for Regular Expressions with Lookahead
Yoshiki Nakamura
We consider (logical) reasoning for regular expressions with lookahead (REwLA). In this paper, we give an axiomatic characterization for both the (match-)language equivalence and t…
The Equational Theory of Relational Kleene Algebra with Graph Loop is PSPACE-Complete
Yoshiki Nakamura
In this paper, we show that the equational theory of relational Kleene algebra with the graph loop operator (a.k.a. fixset) is PSpace-complete. Here, the graph loop is the unary op…
Undecidability of the Emptiness Problem of Deterministic Propositional While Programs with Graph Loop: Hypothesis Elimination Using Loops
Yoshiki Nakamura
We show that the emptiness (unsatisfiability) problem is undecidable and -complete for deterministic propositional while programs with (graph) loop. To this end,…
Guarded Negation Transitive Closure Logic
Diego Figueira, Santiago Figueira, Yoshiki Nakamura
We study the guarded negation fragment of transitive closure logic (GNTC). We show that the satisfiability problem for GNTC is 2ExpTime-complete, by establishing the following redu…
Note on a Translation from First-Order Logic into the Calculus of Relations Preserving Validity and Finite Validity
Yoshiki Nakamura
In this note, we give a linear-size translation from formulas of first-order logic into equations of the calculus of relations preserving validity and finite validity. Our translat…