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

Мне очень импонирует подход использованный в системе Jahob http://lara.epfl.ch/dokuwiki/doku.php?id=jahob_system : специфицировать все в ХОЛ логике, генерировать теоремы, а потом анализировать их на предмет преобразоания в решаемые фрагменты. Действительно, большинство подформул решабельно автоматически тем или иным методом, даже если изначально запись в ХОЛ. Ну а то что осталось можно и ручками добить. Причем, я так думаю, что под предметную область можно сделать набор теорем, которые будут пригождаться в аналогичных случаях. Т.е. фактически получаем кастомизированные домейн-специфик пруверы. Раньше мне казалось что ХОЛ подход очень сложен, хотя и заманчив. Но сейчас я думаю, что он даже более перспективен в русле серьезной системной инженерии, ибо он на самом деле экономит усилия человека: ведь чтобы что-то серьезное выразить в ФОЛ или ДЛ логиках надо потрудится. Плюс надо потрудится для того чтобы это все сопровождать. Лучше уж экономить человеческий труд, но извлекать решаемые фрагменты авто-тулзами, тем более, что большинство теорем будут очень простыми.