Canonized Rewriting and Ground AC Completion Modulo Shostak Theories
No abstract available.
Related papers
- A verified decision procedure for the first-order theory of rewriting for linear variable-separated rewrite systems CPP 2021
- A verified ground confluence tool for linear variable-separated rewrite systems in Isabelle/HOL CPP 2019
- Canonicity for 2-dimensional type theory POPL 2012
- Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting TACAS 2020
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories CAV 2009
- Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories CAV 2016
- Sound and Complete Concolic Testing for Higher-order Functions ESOP 2021
- Higher Order Bayesian Networks, Exactly POPL 2024