We show that it is decidable for any extended ground term rewrite system R whether there is a ground term rewrite system S such that the congrunce ↔* R generated by R is equal to the congruence↔* S generated by S. If the answer is yes, then we can effectively construct such a ground term rewrite system S. We characterize congruences generated by extended ground term rewrite systems.
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.