An algorithm for reasoning about equality

Cited In (26)

Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
Path constraints in semistructured data
Simultaneous rigid E-unification is undecidable
Fast congruence closure and extensions
A framework for using knowledge in tableau proofs
Conditional congruence closure over uninterpreted and interpreted symbols
A taxonomy of exact methods for partial Max-SAT
Decidability and complexity of simultaneous rigid E-unification with one variable and related results
Monadic simultaneous rigid \(E\)-unification and related problems
Complexity, convexity and combinations of theories
Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view
On quasitautologies
What you always wanted to know about rigid \(E\)-unification
On Shostak's decision procedure for combinations of theories
Zero, successor and equality in BDDs
Deduction, strategies, and rewriting
EufDPLL -- a tool to check satisfiability of equality logic formulas
On rewriting rules in Mizar
Monadic simultaneous rigid \(E\)-unification
Inference rules for proving the equivalence of recursive procedures
Order-Sorted Rewriting and Congruence Closure
Efficient ground completion
Congruence closure of compressed terms in polynomial time
Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols
Deciding the word problem for ground identities with commutative and extensional symbols
A strong version of Herbrand's theorem for introvert sentences

This page was built for publication: An algorithm for reasoning about equality

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