A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns

Zhibo Chen, Frank Pfenning

Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has…