Higher-order unification revisited: Complete sets of transformations

DOI10.1016/S0747-7171(89)80023-9zbMath0682.03034OpenAlexW1974087219MaRDI QIDQ1823936

Wayne Snyder, Jean H. Gallier

Publication date: 1989

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0747-7171(89)80023-9

zbMATH Keywords

simple theory of typeshigher-order unificationgeneralization of partial binding to higher-order substitutionsimitation rulemethod of transformations

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Related Items

Context rewriting, Higher-order unification, polymorphism, and subsorts, Second-order unification in the presence of linear shallow algebraic equations, Higher-order unification via combinators, Third order matching is decidable, Functions-as-constructors higher-order unification: extended pattern unification, Reduction and unification in lambda calculi with a general notion of subtype, Decidability of bounded second order unification, Higher-order unification with dependent function types, Regular Patterns in Second-Order Unification, Modular higher-order E-unification, Efficient second-order matching, Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type, Unification for $$\lambda $$ -calculi Without Propagation Rules, Normal forms in combinatory logic, Tractable and intractable second-order matching problems, Extensional higher-order paramodulation in Leo-III, From programming-by-example to proving-by-example, Higher order disunification: Some decidable cases, Higher-order narrowing with convergent systems, Conditional equational theories and complete sets of transformations, Unnamed Item, Polymorphic rewriting conserves algebraic strong normalization, A combinatory logic approach to higher-order E-unification, Unification under a mixed prefix, On intuitionistic proof nets with additional rewrite rules and their approximations, Superposition with lambdas, Superposition with lambdas, Decidable higher-order unification problems, Theory and practice of minimal modular higher-order E-unification, Synthesis of rewrite programs by higher-order and semantic unification, Restricted combinatory unification, A decision algorithm for distributive unification, Decidability of behavioural equivalence in unary PCF, Higher order unification via explicit substitutions

Uses Software

• ETPS

Cites Work

• Simple second-order languages for which unification is undecidable
• A unification algorithm for second-order monadic terms
• The undecidability of the second-order unification problem
• On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Proving and applying program transformations expressed with second-order patterns
• Complete sets of transformations for general E-unification
• A unification-theoretic method for investigating the \(k\)-provability problem
• Complete sets of unifiers and matchers in equational theories
• Theorem Proving via General Matings
• An Efficient Unification Algorithm
• Natural deduction as higher-order resolution
• Semi-Automated Mathematics
• Resolution in type theory
• A Complete Mechanization of Second-Order Type Theory
• The undecidability of unification in third order logic
• Primitive recursion for higher-order abstract syntax
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item