Матита - Matita

О реке в Румынии см. Матиня. Для румынской деревни Матиня см. Păcureți.
Матита
Логотип Matita
Интерфейс создания доказательств Matita.
Интерфейс создания доказательств Matita.
Разработчики)Команда Матита
изначальный выпуск1999
Написано вOCaml
Операционная системаGNU / Linux
Доступно ванглийский
ТипДоказательство теорем
ЛицензияGPL
Интернет сайтhttp://matita.cs.unibo.it

Матита[1]экспериментальный помощник доказательства в стадии разработки на Информатика Отдел Болонский университет. Это инструмент, помогающий в разработке формальных доказательств путем взаимодействия человека и машины, предоставляющий среду программирования, в которой естественным образом сосуществуют формальные спецификации, исполняемые алгоритмы и автоматически проверяемые сертификаты правильности.

Матита основана на зависимый тип Система, известная как исчисление (со) индуктивных построений (производная от Расчет конструкций ), и в некоторой степени совместим с Coq.

Слово «matita» в переводе с итальянского означает «карандаш» (простой и широко распространенный инструмент для редактирования). Это достаточно небольшое и простое приложение,[2] чья архитектурная и программная сложность предназначена для освоения студентами, предоставляя инструмент, особенно подходящий для тестирования инновационных идей и решений. Матита принимает тактика -предварительный режим редактирования; (XML -кодированные) объекты доказательства производятся для хранения и обмена.

Основные особенности

Экзистенциальные переменные встроены в Matita, что позволяет упростить управление зависимыми целями.[3]

Matita реализует двунаправленную вывод типа алгоритм[4] использование как предполагаемых, так и ожидаемых типов.

Возможности системы вывода типов (уточнения) дополнительно расширены механизмом подсказок.[5]что помогает в синтезе объединители в особых ситуациях, указанных пользователем.

Матита поддерживает изощренную стратегию устранения неоднозначности[6] на основе диалога между парсер и типограф.

На интерактивном уровне система реализует пошаговое выполнение структурированной тактики.[7]позволяя гораздо лучше управлять разработкой доказательства и, естественно, приводя к более структурированным и читаемым сценариям.

Приложения

Матита работала в CerCo (Сертифицированная сложность): a FP7 Европейский проект сосредоточился на разработке формально проверенного компилятора, сохраняющего сложность, от большого подмножества C до ассемблера MCS-51 микропроцессор.

Документация

Учебник по Матите[8] обеспечивает практическое введение в основные функции интерактивного средства доказательства теорем Matita, предлагая экскурсию по набору нетривиальных примеров в области спецификации и проверки программного обеспечения.

Смотрите также

Рекомендации

  1. ^ Андреа Асперти, Вильмер Риччиотти, Клаудио Сачердоти Коэн, Энрико Тасси. «Интерактивное средство доказательства теорем Matita»:CADE-23, LNCS 6803, 2011 г., стр. 64-69.
  2. ^ Asperti, A .; Ricciotti, W .; Sacerdoti Coen, C .; Тасси, Э. (2009). «Компактное ядро ​​для исчисления индуктивных конструкций». Садхана. 34: 71–144. Дои:10.1007 / s12046-009-0003-3.
  3. ^ Андреа Асперти, Вильмер Риччиотти, Си Сакердоти Коэн, Энрико Тасси. «Новый тип тактики»:Технический отчет UBLCS-2009-14. Июнь 2009 г.
  4. ^ Андреа Асперти, Вильмер Риччиотти, К. Сачердоти Коэн, Энрико Тасси. «Двунаправленный алгоритм уточнения для расчета (со) индуктивных построений»Логические методы в информатике, т.8, №1
  5. ^ Андреа Асперти, Вильмер Риччиотти, Си Сачердоти Коэн, Энрико Тасси. «Намеки на объединение»:LNCS V.5674, 2009, стр. 84-98
  6. ^ Клаудио Сачердоти Коэн, Стефано Заккироли «Эффективный неоднозначный анализ математических формул»LNCS V.3119, 2004, стр. 347-362
  7. ^ Клаудио Сачердоти Коэн, Энрико Тасси, Стефано Заккироли «Tinycals: Step by Step Tacticals»ENTCS V.174, №2, 2007, страницы 125–142
  8. ^ Андреа Асперти, Вильмер Риччиотти, Клаудио Сачердоти Коэн "Учебник по Матите"Журнал формализованных рассуждений, т.7, №2, 2014 г., страницы 91-199

внешняя ссылка