Philip Zucker[New Blog Post] Implementing E Unification using SMT https://www.philipzucker.com/smt_unify/ #logic #automatedreasoning #smt
back in the saddle
Jamey Sharp@sandmouth I'm far from an expert on this, but isn't the first section ("Using an SMT solvers as a boolean propagator") basically describing CEGAR?
@jamey you could see it that way. Iām asking for counterexamples to fogure out which atoms have to be true. SMT itself is arguably cegar-ish (theories refine the boolean abstraction) or so is anything that asks for models and then does some other solve. I was kind of thinking the second part was more cegarish myself.
@jamey Or the undigested idea of anti-unifying models alluded to at the bottom.
@sandmouth I read that, but by that point you were well into jargon I'm not familiar with š