On the Limits of Second-Order Unification
Jordi Levy · DIGITAL.CSIC (Spanish National Research Council (CSIC)) · 2014
Second-Order Unification is a problem that naturally arises when applying automated deduction techniques with variables denoting predicates. The problem is undecidable, but a considerable effort has been made in order to find decidable fragments, and understand the deep reasons of its complexity. Two variants of the problem, Bounded Second-Order Unification and Linear Second-Order Unification ¿where the use of bound variables in the instantiations is restricted¿, have been extensively studied in the last two decades. In this paper we summarize some decidability/undecidability/complexity results, trying to focus on those that could be more interesting for a wider audience, and involving less technical details.