Complete sets of transformations for general E-unification

DOI10.1016/0304-3975(89)90004-2zbMath0686.68024OpenAlexW2065794924WikidataQ60305319 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 provingrewritingtyped lambda-calculushigher-order unificationequational theoriesE-unificationcomplete sets of unifierstyped theory

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) 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 inference system for horn clause logic with equality ⋮ Higher-order unification via combinators ⋮ Goal directed strategies for paramodulation ⋮ Modular higher-order E-unification ⋮ Improving transformation systems for general E-unification ⋮ Unification of kinded infinite trees ⋮ General \(E\)-unification with eager variable elimination and a nice cycle rule ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ Superposition-based equality handling for analytic tableaux ⋮ Equation solving in conditional AC-theories ⋮ Modular AC unification of higher-order patterns ⋮ Lazy narrowing: Strong completeness and eager variable elimination (extended abstract) ⋮ Unification and Matching in Hierarchical Combinations of Syntactic Theories ⋮ Conditional equational theories and complete sets of transformations ⋮ Connection tableaux with lazy paramodulation ⋮ Polymorphic rewriting conserves algebraic strong normalization ⋮ E-generalization using grammars ⋮ Lazy narrowing: strong completeness and eager variable elimination ⋮ A combinatory logic approach to higher-order E-unification ⋮ Average-case analysis of unification algorithms ⋮ An improved general \(E\)-unification method ⋮ Variant-Based Satisfiability in Initial Algebras ⋮ Combination techniques for non-disjoint equational theories ⋮ Theory and practice of minimal modular higher-order E-unification ⋮ A refined version of general E-unification ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Pattern-directed invocation with changing equations

Cites Work

• 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
• 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