Complete sets of transformations for general E-unification

DOI10.1016/0304-3975(89)90004-2zbMath0686.68024WikidataQ60305319 ScholiaQ60305319MaRDI QIDQ1262754

Jean H. Gallier, Wayne Snyder

Publication date: 1989

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1816&context=cis_reports

zbMATH Keywords

theorem proving; rewriting; typed lambda-calculus; higher-order unification; equational theories; E-unification; complete sets of unifiers; typed theory

Mathematics Subject Classification ID

68W30: Symbolic computation and algebraic computation

68Q65: Abstract data types; algebraic specification

03B35: Mechanization of proofs and logical operations

03B40: Combinatory logic and lambda calculus

08A50: Word problems (aspects of algebraic structures)

Related Items

Lazy narrowing: strong completeness and eager variable elimination, A combinatory logic approach to higher-order E-unification, Average-case analysis of unification algorithms, Pattern-directed invocation with changing equations, Superposition-based equality handling for analytic tableaux, Conditional equational theories and complete sets of transformations, Connection tableaux with lazy paramodulation, Polymorphic rewriting conserves algebraic strong normalization, An improved general \(E\)-unification method, Unification of kinded infinite trees, Higher-order unification revisited: Complete sets of transformations, Combination problems for commutative/monoidal theories or how algebra can help in equational unification, Higher-order unification via combinators, E-generalization using grammars, General \(E\)-unification with eager variable elimination and a nice cycle rule

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Termination of rewriting
• Linear unification
• Complete sets of unifiers and matchers in equational theories
• Basic narrowing revisited
• Extending SLD resolution to equational horn clauses using E-unification
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• An Efficient Unification Algorithm
• Positive First-Order Logic Is NP-Complete
• Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity
• A Machine-Oriented Logic Based on the Resolution Principle
• Equality, types, modules, and (why not?) generics for logic programming