On the relationship of congruence closure and unification

DOI10.1016/S0747-7171(89)80018-5zbMath0678.68041OpenAlexW1964892433WikidataQ57641786 ScholiaQ57641786MaRDI QIDQ1124338

Peter Z. Revesz, Paris C. Kanellakis

Publication date: 1989

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

Full work available at URL: https://doi.org/10.1016/s0747-7171(89)80018-5

zbMATH Keywords

PTIMElog-space completeCongruence closureparallel complexity class NCUnification closure

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Symbolic computation and algebraic computation (68W30)

Related Items

Another variation on the common subexpression problem, A closed-form evaluation for Datalog queries with integer (gap)-order constraints

Cites Work

• Unnamed Item
• Unnamed Item
• A parallel algorithm for the monadic unification problem
• Tree-size bounded alternation
• Linear unification
• On the sequential nature of unification
• Parallel Algorithms for Term Matching
• Fast Decision Procedures Based on Congruence Closure
• Variations on the Common Subexpression Problem
• Reasoning About Recursively Defined Data Structures
• An Efficient Unification Algorithm
• Efficiency of a Good But Not Linear Set Union Algorithm
• Assignment Commands with Array References
• New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
• Parallelism in random access machines
• A Machine-Oriented Logic Based on the Resolution Principle
• Generalized finite automata theory with an application to a decision problem of second-order logic