Изабелла - помощник доказательства для написания и проверки математических доказательств компьютером. Он позволяет выражать математические формулы на формальном языке и предоставляет инструменты для доказательства этих формул в логическом исчислении.
    Разработчик
    Larry Paulson and Tobias Nipkow