Unification with Simple Variable Restrictions and Admissibility of ${\Pi }_2$-rules

Rodrigo Nicolau Almeida, Silvio Ghilardi

We develop a method to recognize admissibility of ${\Pi }_2$-rules, relating this problem to a specific instance of the unification problem with linear constants restriction, called h…