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).

翻译：过渡代数（Transition Algebra, TA）是为讨论重写系统而引入的一种无穷逻辑。TA中已有的自然演绎证明系统对可数签名满足完备性。然而，它缺乏紧致性，使其不适用于实际应用。本次，我们将通过将（星号）规则限制为归纳规则来创建一个紧致的证明系统。同时，我们将采用矢列证明系统替代自然演绎。此外，我们将引入一种使该系统完备的语义，并展示其应用（Craig插值定理的模型论证明）。