A transformation between institutions representing the theorem of herbrand-Schmidt-Wang
Juan Climent Vidal, J. Soliveres Tur · 2009
We prove that domain unification, when viewed as a suitable transformation between two convenient institutions, represents the theorem of Herbrand-Schmidt-Wang encoding manysorted first-order logic into single-sorted first-order logic.