Higher-order unification revisited: Complete sets of transformations
From MaRDI portal
Publication:1823936
Some approach to higher-order unification is presented. The approach is based on the method of transformation of terms and extends the approach developed by Martelli and Montanari in the context of first-order unification. The method of transformations for solving unification problems is much like the well-known Gaussian method used for solving systems of linear equations. Gaussian elimination and first-order unification are somewhat similar. But in the higher-order case the analogy breaks down. The most important differences to the first-order case have to do with the imitation rule and the generalization of the notion of a partial binding to higher-order substitutions.
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
- A Complete Mechanization of Second-Order Type Theory
- A unification algorithm for second-order monadic terms
- A unification algorithm for typed -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
- 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?)
- 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
(45)- Polymorphic rewriting conserves algebraic strong normalization
- Transformation completeness properties of SVPC transformation sets
- 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
- Functions-as-constructors higher-order unification: extended pattern unification
- Restricted combinatory unification
- Higher-order unification via combinators
- Tractable and intractable second-order matching problems
- Extensional higher-order paramodulation in Leo-III
- Unification via the s_e-style of explicit substitutions
- Unification for -calculi without propagation rules
- Regular patterns in second-order unification
- scientific article; zbMATH DE number 8800 (Why is no real title available?)
- scientific article; zbMATH DE number 1088023 (Why is no real title available?)
- On intuitionistic proof nets with additional rewrite rules and their approximations
- Efficient full higher-order unification
- Higher-order unification with dependent function types
- 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
- From programming-by-example to proving-by-example
- Higher order disunification: some decidable cases
- Higher-order narrowing with convergent systems
- Decidable higher-order unification problems
- Theory and practice of minimal modular higher-order \(E\)-unification
- Context rewriting
- Higher-order unification, polymorphism, and subsorts
- Second-order unification in the presence of linear shallow algebraic equations
- Superposition with lambdas
- Superposition with lambdas
- Higher order E-unification
- Programming by example and proving by example using higher-order unification
- Superposition with Delayed Unification
- Representing unification in a logical framework
- A combinatory logic approach to higher-order E-unification
- Efficient full higher-order unification
- Types, Tableaus and Gödel’s God in Isabelle/HOL
- Synthesis of rewrite programs by higher-order and semantic unification
- Conditional equational theories and complete sets of transformations
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)
