An algorithm for reasoning about equality

Cited in

(27)

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

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)