Higher-order unification revisited: Complete sets of transformations

DOI10.1016/S0747-7171(89)80023-9MaRDI QIDQ1823936zbMATH OpenOpenAlexFDO

Authors Wayne Snyder, Jean 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)

Recommendations

• Complete sets of transformations for general E-unification
• Higher-order unification via combinators
• Higher order unification via explicit substitutions
• Conditional equational theories and complete sets of transformations
• scientific article; zbMATH DE number 3867289
• Complete sets of unifiers and matchers in equational theories
• Improving transformation systems for general E-unification
• Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
• Unifications, deunifications, and their complexity
• Rewriting, and equational unification: the higher-order cases

Cites work

• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 3878393 (Why is no real title available?)
• scientific article; zbMATH DE number 3935004 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 4045129 (Why is no real title available?)
• scientific article; zbMATH DE number 4053062 (Why is no real title available?)
• scientific article; zbMATH DE number 3577189 (Why is no real title available?)
• scientific article; zbMATH DE number 1158760 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3999882 (Why is no real title available?)
• scientific article; zbMATH DE number 3362981 (Why is no real title available?)
• scientific article; zbMATH DE number 3412189 (Why is no real title available?)
• A Complete Mechanization of Second-Order Type Theory
• A unification algorithm for second-order monadic terms
• A unification algorithm for typed \(\overline\lambda\)-calculus
• A unification-theoretic method for investigating the \(k\)-provability problem
• An Efficient Unification Algorithm
• Complete sets of transformations for general E-unification
• Complete sets of unifiers and matchers in equational theories
• Mechanizing \(\omega\)-order type theory through unification
• Natural deduction as higher-order resolution
• On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
• Primitive recursion for higher-order abstract syntax
• Proving and applying program transformations expressed with second-order patterns
• Resolution in type theory
• Semi-Automated Mathematics
• Simple second-order languages for which unification is undecidable
• The undecidability of the second-order unification problem
• The undecidability of unification in third order logic
• Theorem Proving via General Matings

Cited in

(41)

• Programming by example and proving by example using higher-order unification
• Decidability of behavioural equivalence in unary PCF
• scientific article; zbMATH DE number 7471678 (Why is no real title available?)
• Unification via the \(\lambda s_e\)-style of explicit substitutions
• Conditional equational theories and complete sets of transformations
• On intuitionistic proof nets with additional rewrite rules and their approximations
• Third order matching is decidable
• Extensional higher-order paramodulation in Leo-III
• Higher order unification via explicit substitutions
• Higher-order unification with dependent function types
• Modular higher-order E-unification
• Superposition with Delayed Unification
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Higher-order unification via combinators
• A combinatory logic approach to higher-order E-unification
• Context rewriting
• Normal forms in combinatory logic
• Tractable and intractable second-order matching problems
• Synthesis of rewrite programs by higher-order and semantic unification
• Decidability of bounded second order unification
• Theory and practice of minimal modular higher-order \(E\)-unification
• Unification for \(\lambda\)-calculi without propagation rules
• Regular patterns in second-order unification
• From programming-by-example to proving-by-example
• Transformation completeness properties of SVPC transformation sets
• Superposition with lambdas
• Unification under a mixed prefix
• Higher order disunification: some decidable cases
• Higher-order narrowing with convergent systems
• Decidable higher-order unification problems
• Superposition with lambdas
• A decision algorithm for distributive unification
• Higher-order unification, polymorphism, and subsorts
• Polymorphic rewriting conserves algebraic strong normalization
• Functions-as-constructors higher-order unification: extended pattern unification
• Restricted combinatory unification
• Efficient second-order matching
• Second-order unification in the presence of linear shallow algebraic equations
• Representing unification in a logical framework
• Higher order E-unification
• Reduction and unification in lambda calculi with a general notion of subtype

Describes a project that uses

Uses Software

• ETPS

This page was built for publication: Higher-order unification revisited: Complete sets of transformations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1823936)