General Conservative Extension Theorem in Process Algebras with Inequalities

摘要

The authors prove a general conservative extension theorem for transition systembased process theories with easy-to-check and reasonable conditions. The core of this result is another general theorem which gives sufficient conditions for a system of operational rules and an extension of it in order to ensure conservativity, that is, provable transitions from an original term in the extension are the same as in the original system. As a simple corollary of the conservative extension theorem, the authors prove a completeness theorem. The authors also prove a general theorem giving sufficient conditions to reduce the question of ground confluence modulo some equations for a large term rewriting system associated with an equational process theory to a small term rewriting system under the condition that the large system is a conservative extension of the small one. The authors provide many applications to show that their results are useful.