Solving Higher-Order Equations

This monograph develops techniques for equational reasoning in higher-order logic. Due to its expressiveness, higher-order logic is used for specification and verification of hardware, software, and mathematics. In these applica­ tions, higher-order logic provides the necessary level of abstraction for con­ cise and natural formulations. The main assets of higher-order logic are quan­ tification over functions or predicates and its abstraction mechanism. These allow one to represent quantificati