Unification in combinations of collapse-free regular theories

DOI10.1016/S0747-7171(87)80025-1zbMath0638.68105MaRDI QIDQ1099652

Katherine A. Yelick

Publication date: 1987

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

reasoning; associative-commutative operators; collapse-free regular theories; equational unification algorithms

Mathematics Subject Classification ID

08B05: Equational logic, Mal'tsev conditions

Related Items

Unification in a combination of arbitrary disjoint equational theories, Combining matching algorithms: The regular case, Boolean unification - the story so far, On equational theories, unification, and (un)decidability, Unification algorithms cannot be combined in polynomial time.

Uses Software

• REVE

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
• Proofs by induction in equational theories with constructors
• Properties of substitutions and unifications
• REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies
• CLU reference manual
• A theory of type polymorphism in programming
• Oriented equational clauses as a programming language
• Deciding Combinations of Theories
• Simplification by Cooperating Decision Procedures
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• Complete Sets of Reductions for Some Equational Theories
• A Machine-Oriented Logic Based on the Resolution Principle