Induction rules for Transition Algebra
This work provides a compact and complete proof system for Transition Algebra, which is foundational for reasoning about rewriting systems but remains domain-specific.
The authors address the lack of compactness in Transition Algebra's proof system by restricting the (Star) rule to induction and using a sequent calculus, achieving completeness and enabling a model-theoretic proof of Craig interpolation.
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).