BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
No abstract available.
DOI 10.1007/bfb0028749
Related papers
- Simplification by Cooperating Decision Procedures TOPLAS 1979
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions CAV 1999
- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations CAV 2001
- Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic VMCAI 2011
- Tactics for Reasoning Modulo AC in Coq CPP 2011
- Alternating Automata Modulo First Order Theories CAV 2019
- A Simplifier Based on Efficient Decision Algorithms POPL 1978
- Decidable verification of uninterpreted programs POPL 2019