An algorithm for reasoning about equality

DOI10.1145/359545.359570zbMath0378.68044OpenAlexW2036915776MaRDI QIDQ4157961

Robert E. Shostak

Publication date: 1978

Published in: Communications of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/359545.359570

Mathematics Subject Classification ID

Related Items (25)

Congruence Closure of Compressed Terms in Polynomial Time ⋮ Efficient ground completion ⋮ Monadic simultaneous rigid E-unification and related problems ⋮ Fast congruence closure and extensions ⋮ Complexity, convexity and combinations of theories ⋮ Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties ⋮ On rewriting rules in Mizar ⋮ A taxonomy of exact methods for partial Max-SAT ⋮ On quasitautologies ⋮ A framework for using knowledge in tableau proofs ⋮ Monadic simultaneous rigid \(E\)-unification ⋮ Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Path constraints in semistructured data ⋮ Inference rules for proving the equivalence of recursive procedures ⋮ On Shostak's decision procedure for combinations of theories ⋮ Zero, successor and equality in BDDs ⋮ Order-Sorted Rewriting and Congruence Closure ⋮ EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas ⋮ What you always wanted to know about rigid E-unification ⋮ Decidability and complexity of simultaneous rigid E-unification with one variable and related results ⋮ A strong version of Herbrand's theorem for introvert sentences ⋮ 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 ⋮ Deduction, Strategies, and Rewriting ⋮ Book review of: Daniel Kroening and Ofer Strichman, Decision procedures: an algorithmic point of view

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