3 ms·
> it's an undecidable problem In what sense? People often use SMT (Satisfiability modulo theories) but don't state _which_ theories. I often SMT-solve with dec
by maweki 3y ago
> it's an undecidable problem
In what sense? People often use SMT (Satisfiability modulo theories) but don't state _which_ theories. I often SMT-solve with decidable theories, like Presburger Arithmetic.
- xavxav 3y agoI almost exclusively use it with quantifiers which makes it equivalent to FOL. But even without quantifiers, theory combinations can introduce undecidability. There’s the auxiliary problem that decidable but slow can often be equivalent to undecidable.