Fast Decision Procedures Based on Congruence Closure.

Greg Nelson Derek C. Oppen

Published in: J. ACM (1980)

Keyphrases

decision procedures
theorem proving
modal logic
automated reasoning
reasoning problems
conjunctive queries
query containment
artificial intelligence
satisfiability problem
logic programs
fixpoint
tight complexity bounds