Induction rules for Transition Algebra
Logic in Computer Science
2026-05-06 v1
Abstract
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).
Keywords
Cite
@article{arxiv.2605.03628,
title = {Induction rules for Transition Algebra},
author = {Go Hashimoto},
journal= {arXiv preprint arXiv:2605.03628},
year = {2026}
}