Induction rules for Transition Algebra
Fuente:
arXiv
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917462115614720 |
|---|---|
| author | Hashimoto, Go |
| author_facet | Hashimoto, Go |
| contents | Transition Algebra (TA) is a type of infinite logic introduced to discuss rewriting systems. The natural deductive proof systems already introduced in TA satisfy completeness for countable signatures. However, it lacks compactness, making it unsuitable for practical applications. This time, we will create a compact proof system by restricting the (Star) rule to induction. We will also use a sequent proof system instead of natural deduction. Furthermore, we will introduce a semantics that makes this system complete, and its application (a model-theoretic proof of Craig interpolation). |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_03628 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Induction rules for Transition Algebra Hashimoto, Go Logic in Computer Science Transition Algebra (TA) is a type of infinite logic introduced to discuss rewriting systems. The natural deductive proof systems already introduced in TA satisfy completeness for countable signatures. However, it lacks compactness, making it unsuitable for practical applications. This time, we will create a compact proof system by restricting the (Star) rule to induction. We will also use a sequent proof system instead of natural deduction. Furthermore, we will introduce a semantics that makes this system complete, and its application (a model-theoretic proof of Craig interpolation). |
| title | Induction rules for Transition Algebra |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.03628 |