Без заголовка

Боюсь что трудно будет объяснить. Все-таки верификация специфичная область. Но если в общих чертах, то: 1. нужно сделать обратную трансляцию из логических формул в конструкции целевого языка. Т.е. при верификации код программы определенным образом кодируется в логические формулы, но эти записи читать довольно-таки геморройно. Правда, для выражения некоторыъ формул, оригинальный язык нужно будет несколько расширить. 2. нужно сделать упрощение логических формул. Текущее состояние доказательства, либо контр-пример - это обычно куча формул, многие из которых лишние, многие вспомогательные. Вобщем, из них можно выкинуть кучу хлама, который только отвлекает, но избыточен для понимания сути. Это не всегда просто сделать, но какие-то эвристики можно сочинить. 3. графические интерфейсы более-менее разработаны, но какие-то мелкие улучшения можно придумать. Плюс надо интерфейс для сепарейшн лоджик.