On the relationship of congruence closure and unification

DOI10.1016/S0747-7171(89)80018-5MaRDI QIDQ1124338zbMATH OpenOpenAlexWikidataFDO

Authors Paris C. Kanellakis, P. Z. Revesz

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)

Recommendations

• Abstract congruence closure
• scientific article; zbMATH DE number 1614687
• Congruent closure algorithms for finite automata and some applications
• Conditional congruence closure over uninterpreted and interpreted symbols
• Computing congruent closures on terms

Cites work

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

Cited in

(5)

• scientific article; zbMATH DE number 2064226 (Why is no real title available?)
• Another variation on the common subexpression problem
• A closed-form evaluation for Datalog queries with integer (gap)-order constraints
• Abstract congruence closure
• Congruent closure algorithms for finite automata and some applications

This page was built for publication: On the relationship of congruence closure and unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1124338)