2 papers
cs.AI2026
Extending SMT Solving with Non-Ground Clause Learning
Yasmine Briefs, Christoph Weidenbach
Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style…
cs.LO2024
Non-Ground Congruence Closure
Hendrik Leidinger, Christoph Weidenbach
Congruence closure on ground equations is a well-established and efficient algorithm for deciding ground equalities. It constructs an explicit representation of ground equivalence…