Higher-order unification revisited: Complete sets of transformations
From MaRDI portal
Publication:1823936
DOI10.1016/S0747-7171(89)80023-9zbMath0682.03034MaRDI QIDQ1823936
Publication date: 1989
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
simple theory of types; higher-order unification; generalization of partial binding to higher-order substitutions; imitation rule; method of transformations
03B35: Mechanization of proofs and logical operations
03F35: Second- and higher-order arithmetic and fragments
Related Items
A combinatory logic approach to higher-order E-unification, Polymorphic rewriting conserves algebraic strong normalization, Unification under a mixed prefix, A decision algorithm for distributive unification, Decidability of behavioural equivalence in unary PCF, Third order matching is decidable, Reduction and unification in lambda calculi with a general notion of subtype, Higher order unification via explicit substitutions, Decidability of bounded second order unification, Normal forms in combinatory logic, Higher-order unification via combinators
Uses Software