On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2023
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866912406623485952 |
|---|---|
| author | Nakamura, Yoshiki |
| author_facet | Nakamura, Yoshiki |
| contents | We introduce the $k$-variable-occurrence fragment, which is the set of terms having at most $k$ occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the $k$-variable-occurrence fragment using the finiteness of a monoid. As a case study, we prove that for Tarski's calculus of relations with bounded dot-dagger alternation (an analogy of quantifier alternation in first-order logic), the equational theory of the $k$-variable-occurrence fragment is decidable for each $k$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_05046 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation Nakamura, Yoshiki Logic in Computer Science We introduce the $k$-variable-occurrence fragment, which is the set of terms having at most $k$ occurrences of variables. We give a sufficient condition for the decidability of the equational theory of the $k$-variable-occurrence fragment using the finiteness of a monoid. As a case study, we prove that for Tarski's calculus of relations with bounded dot-dagger alternation (an analogy of quantifier alternation in first-order logic), the equational theory of the $k$-variable-occurrence fragment is decidable for each $k$. |
| title | On the Finite Variable-Occurrence Fragment of the Calculus of Relations with Bounded Dot-Dagger Alternation |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2307.05046 |