An algorithm for reasoning about equality

Cited in

(26)

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

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)