Higher-order unification revisited: Complete sets of transformations
From MaRDI portal
Publication:1823936
DOI10.1016/S0747-7171(89)80023-9zbMATH Open0682.03034OpenAlexW1974087219MaRDI QIDQ1823936FDOQ1823936
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
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
simple theory of typeshigher-order unificationgeneralization of partial binding to higher-order substitutionsimitation rulemethod of transformations
Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- An Efficient Unification Algorithm
- Title not available (Why is that?)
- A unification-theoretic method for investigating the \(k\)-provability problem
- Resolution in type theory
- Title not available (Why is that?)
- Primitive recursion for higher-order abstract syntax
- Proving and applying program transformations expressed with second-order patterns
- Theorem Proving via General Matings
- Complete sets of unifiers and matchers in equational theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Natural deduction as higher-order resolution
- The undecidability of the second-order unification problem
- Complete sets of transformations for general E-unification
- Title not available (Why is that?)
- On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
- A unification algorithm for second-order monadic terms
- Title not available (Why is that?)
- Title not available (Why is that?)
- Semi-Automated Mathematics
- The undecidability of unification in third order logic
- Simple second-order languages for which unification is undecidable
- A Complete Mechanization of Second-Order Type Theory
- Mechanizing \(\omega\)-order type theory through unification
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
Cited In (41)
- Restricted combinatory unification
- Superposition with lambdas
- Higher-order unification, polymorphism, and subsorts
- Representing unification in a logical framework
- On intuitionistic proof nets with additional rewrite rules and their approximations
- Polymorphic rewriting conserves algebraic strong normalization
- Programming by example and proving by example using higher-order unification
- Higher order E-unification
- Extensional higher-order paramodulation in Leo-III
- Functions-as-constructors higher-order unification: extended pattern unification
- Context rewriting
- Normal forms in combinatory logic
- Theory and practice of minimal modular higher-order \(E\)-unification
- Decidability of behavioural equivalence in unary PCF
- Unification via the \(\lambda s_e\)-style of explicit substitutions
- Unification for \(\lambda\)-calculi without propagation rules
- Superposition with lambdas
- Efficient second-order matching
- Higher-order unification via combinators
- Regular patterns in second-order unification
- Higher order unification via explicit substitutions
- Tractable and intractable second-order matching problems
- Decidability of bounded second order unification
- Title not available (Why is that?)
- Synthesis of rewrite programs by higher-order and semantic unification
- Higher order disunification: Some decidable cases
- Transformation completeness properties of SVPC transformation sets
- Third order matching is decidable
- Decidable higher-order unification problems
- A decision algorithm for distributive unification
- Superposition with Delayed Unification
- Reduction and unification in lambda calculi with a general notion of subtype
- Conditional equational theories and complete sets of transformations
- Unification under a mixed prefix
- Higher-order narrowing with convergent systems
- Higher-order unification with dependent function types
- Modular higher-order E-unification
- From programming-by-example to proving-by-example
- Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
- Second-order unification in the presence of linear shallow algebraic equations
- A combinatory logic approach to higher-order E-unification
Uses Software
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)
