scientific article
From MaRDI portal
Publication:3782762
zbMath0641.68045MaRDI QIDQ3782762
Publication date: 1987
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
theorem provingrewritingtyped lambda-calculushigher-order unificationequational theoriesE-unificationcomplete sets of unifierstyped theory
Abstract data types; algebraic specification (68Q65) Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40) Word problems (aspects of algebraic structures) (08A50)
Related Items
A new approach to general E-unification based on conditional rewriting systems, An universal termination condition for solving goals in equational languages, Narrowing and unification in functional programming —An evaluation mechanism for absolute set abstraction, Goal directed strategies for paramodulation, Unification modulo an equality theory for equational logic programming, General \(E\)-unification with eager variable elimination and a nice cycle rule, Incremental constraint satisfaction for equational logic programming, Equational problems and disunification, Enumerating outer narrowing derivations for constructor-based term rewriting systems, Complete equational unification based on an extension of the Knuth-Bendix completion procedure, Conditional equational theories and complete sets of transformations, Unification in Boolean rings and Abelian groups, Unification in a combination of arbitrary disjoint equational theories, Completion for rewriting modulo a congruence, Complete sets of transformations for general E-unification, Synthesis of rewrite programs by higher-order and semantic unification, Higher-order unification revisited: Complete sets of transformations, Horn equational theories and paramodulation, Basic narrowing revisited
