существуют ли решатели SMT, поддерживающие теории дифференциальных уравнений?

Question

если ответ да, как они работают?Я пытался найти информацию о решателе z3, но о дифференциальных уравнениях ничего не смог найти.

Answer 1

Я думаю dReal (http://dreal.github.io/) - единственный решатель, который обеспечивает поддержку ODE, хотя я не эксперт в этом.

Также см. Эту статью для получения дополнительной информации: https://arxiv.org/pdf/1310.8278.pdf