![]() |
| |||
| решатель задач выполнимости формул в теориях (решает задачи выполнимости формул с учётом комбинации лежащих в их основе теорий | |||
| |||
| решатель задач выполнимости формул в теориях (решатель находит решения задач выполнимости логических формул, выраженных в классической логике первого порядка с равенством, при наличии дополнительных соотношений, заданных при помощи комбинации определённых теорий; часто используемыми на практике примерами теорий являются теории вещественных и целых чисел, а также теории поведения различных структур данных, таких как списки, массивы, битовые вектора и т.д. | |||