Описание тега alt-ergo

Alt-Ergo - это автоматическое средство доказательства теорем с открытым исходным кодом, предназначенное для проверки программ. См. http://alt-ergo.lri.fr/ для получения дополнительной информации. Это решатель SMT, основанный на CC(X): алгоритм замыкания сравнения, параметризованный эквациональной теорией X. Alt-Ergo основан на самодельном SAT-решателе и реализует механизм создания экземпляров для количественных формул.