Finite Instantiations in Equivalence Logic with Uninterpreted Functions
No abstract available.
Related papers
- Augmenting Model-Based Instantiation with Fast Enumeration TACAS 2025
- Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions CAV 1999
- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions CAV 2002
- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations CAV 2001
- Axe 'Em: Eliminating Spurious States with Induction Axioms POPL 2025
- Foundations for natural proofs and quantifier instantiation POPL 2018
- VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints OOPSLA 2024
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic VMCAI 2017