Unification in combinations of collapse-free regular theories

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

Katherine A. Yelick

Publication date: 1987

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(87)80025-1

zbMATH Keywords

reasoningassociative-commutative operatorscollapse-free regular theoriesequational unification algorithms

Mathematics Subject Classification ID

Equational logic, Mal'tsev conditions (08B05)

Related Items

Second-order unification in the presence of linear shallow algebraic equations, An overview of LP, the Larch Prover, Modular higher-order E-unification, Combining matching algorithms: The regular case, Unification algorithms cannot be combined in polynomial time, Unification theory, Combining matching algorithms: The regular case, Unification in a combination of arbitrary disjoint equational theories, Boolean unification - the story so far, On equational theories, unification, and (un)decidability, Unification algorithms cannot be combined in polynomial time., Terminating non-disjoint combined unification

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