A proof theory for general unification

zbMath0746.03011MaRDI QIDQ1189467

Wayne Snyder

Publication date: 18 September 1992

Published in: Progress in Computer Science and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

transformationstreeshigher-order unification\(E\)-unificationeager variable eleminationequational proofsextensions of the Martelli- Monanari methodnarrowing methodunfailing completion

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Equational classes, universal algebra in model theory (03C05)

Related Items (11)

Unification in intuitionistic logic ⋮ Improving transformation systems for general E-unification ⋮ Higher-order narrowing with convergent systems ⋮ Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) ⋮ Equivariant unification ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ Lazy narrowing: strong completeness and eager variable elimination ⋮ Redundancy criteria for constrained completion ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Unification in an extensional lambda calculus with ordered function sorts and constant overloading ⋮ Higher-Order Multi-Valued Resolution

This page was built for publication: A proof theory for general unification