TL;DR
This paper develops a compact, sequent-based proof system for Transition Algebra, enhancing its practical applicability and establishing a model-theoretic semantics that achieves completeness and Craig interpolation.
Contribution
It introduces a new induction-restricted proof system and semantics for Transition Algebra, improving its completeness and practical utility.
Findings
Created a compact proof system for TA using induction restrictions.
Established a semantics that ensures the system's completeness.
Provided a model-theoretic proof of Craig interpolation for TA.
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).
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.