Canonization for disjoint unions of theories
KrstićSava, ConchonSylvain · Information and Computation · 2005
If there exist efficient procedures (canonizers) for reducing terms of two first-order theories to canonical form, can one use them to construct such a procedure for terms of the disjoint union of ...