Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions
Abstract elided by the publisher.
Related papers
- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations CAV 2001
- BDD Based Procedures for a Theory of Equality with Uninterpreted Functions CAV 1998
- Revisiting Positive Equality TACAS 2004
- Decidable verification of uninterpreted programs POPL 2019
- Deciding equivalence with sums and the empty type POPL 2017
- Tactics for Reasoning Modulo AC in Coq CPP 2011
- Dependently-Typed Programming with Logical Equality Reflection ICFP 2023
- Simplification by Cooperating Decision Procedures TOPLAS 1979