Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning
No abstract available.
Related papers
- babble: Learning Better Abstractions with E-Graphs and Anti-unification POPL 2023
- Better Together: Unifying Datalog and Equality Saturation PLDI 2023
- Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory JFP 2018
- Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by Equality Saturation POPL 2026
- Generically Automating Separation Logic by Functors, Homomorphisms, and Modules POPL 2025
- Parallel type-checking with haskell using saturating LVars and stream generators PPoPP 2016
- The graphical theory of monads JFP 2025
- Equality Saturation Theory Exploration à la Carte OOPSLA 2023