 | |
 Интерфейс создания доказательств Matita. | |
| Разработчики) | Команда Матита |
|---|---|
| Первый выпуск | 1999 г. |
| Написано в | OCaml |
| Операционная система | Linux |
| Доступно в | английский |
| Тип | Доказательство теорем |
| Лицензия | GPL |
| Веб-сайт | http://matita.cs.unibo.it |
Матита [1] - помощник по экспериментальному доказательству, разрабатываемый на факультете компьютерных наук Болонского университета . Это инструмент, помогающий в разработке формальных доказательств путем взаимодействия человека и машины, предоставляющий среду программирования, в которой естественным образом сосуществуют формальные спецификации, исполняемые алгоритмы и автоматически проверяемые сертификаты правильности.
Матита основана на системе зависимых типов , известной как исчисление (со) индуктивных построений (производное от исчисления построений ), и в некоторой степени совместима с Coq .
Слово «matita» в переводе с итальянского означает «карандаш» (простой и широко распространенный инструмент для редактирования). Это довольно небольшое и простое приложение [2] , архитектурная и программная сложность которого предназначена для освоения студентами, и предоставляет инструмент, особенно подходящий для тестирования инновационных идей и решений. Матита использует режим редактирования, основанный на тактике ; ( XML- закодированные) объекты доказательства создаются для хранения и обмена.
Основные особенности [ править ]
Экзистенциальные переменные встроены в Matita, что позволяет упростить управление зависимыми целями. [3]
Matita реализует алгоритм двунаправленного вывода типов [4], использующий как предполагаемые, так и ожидаемые типы.
Возможности системы вывода типов (уточнения) дополнительно дополняются механизмом подсказок [5], который помогает синтезировать унификаторы в конкретных ситуациях, заданных пользователем.
Matita поддерживает сложную стратегию устранения неоднозначности [6], основанную на диалоге между синтаксическим анализатором и проверкой типов .
На интерактивном уровне система реализует выполнение структурированной тактики за небольшой шаг [7], что позволяет гораздо лучше управлять разработкой доказательства и, естественно, приводит к созданию более структурированных и читаемых сценариев.
Приложения [ править ]
Матита использовалась в CerCo (Certified Complexity): европейском проекте FP7, сфокусированном на разработке официально проверенного, сохраняющего сложность компилятора от большого подмножества C до ассемблера микропроцессора MCS-51 .
Документация [ править ]
Учебник Matita [8] представляет собой практическое введение в основные функции интерактивного средства доказательства теорем Matita, предлагая экскурсию по набору нетривиальных примеров в области спецификации и проверки программного обеспечения .
См. Также [ править ]
- Интерактивное доказательство теорем
- Переписка Карри – Ховарда
- Интуиционистская теория типов
Ссылки [ править ]
- ^ Андреа Асперти, Вильмер Риччиотти, Клаудио Сакердоти Коэн, Энрико Тасси. «Интерактивное средство доказательства теорем Matita»: CADE-23, LNCS 6803, 2011, стр. 64-69 .
- ^ Асперти, А .; Ricciotti, W .; Sacerdoti Coen, C .; Тасси, Э. (2009). «Компактное ядро для исчисления индуктивных конструкций» . Садхана . 34 : 71–144. DOI : 10.1007 / s12046-009-0003-3 .
- ^ Андреа Асперти, Вильмер Риччиотти, C Сачердоти Коэн, Энрико Тасси. «Новый тип тактики»: Технический отчет UBLCS-2009-14. Июнь 2009 г.
- ^ Андреа Асперти, Вильмер Риччиотти, C Сачердоти Коэн, Энрико Тасси. "Двунаправленный алгоритм уточнения для исчисления (со) индуктивных конструкций" Логические методы в компьютерных науках, V.8, n1
- ^ Андреа Асперти, Вильмер Риччиотти, C Сачердоти Коэн, Энрико Тасси. «Советы по объединению»: LNCS V.5674, 2009, стр. 84-98.
- ^ Клаудио Сачердоти Коэн, Стефано Заккироли «Эффективный неоднозначный анализ математических формул» LNCS V.3119, 2004, стр. 347-362
- ^ Клаудио Сачердоти Коэн, Энрико Тасси, Стефано Заккироли "Tinycals: Step by Step Tacticals" ENTCS V.174, №2, 2007, страницы 125–142
- ^ Андреа Асперти, Вильмер Риччиотти, Клаудио Сачердоти Коэн "Учебник по Матите " Журнал формализованных рассуждений, V.7, номер 2, 2014, страницы 91-199
Внешние ссылки [ править ]
- Помощник Matita Proof
- CerCo Project
