Matita

Matita ^{[ 1 ]} es un asistente de demostración experimental en desarrollo en el Departamento de Informática de la Universidad de Bolonia . Es una herramienta que facilita el desarrollo de demostraciones formales mediante la colaboración humano-máquina, proporcionando un entorno de programación donde coexisten de forma natural las especificaciones formales , los algoritmos ejecutables y los certificados de corrección verificables automáticamente.

Matita se basa en un sistema de tipos dependientes conocido como cálculo de construcciones (co)inductivas (un derivado del cálculo de construcciones ) y es compatible, hasta cierto punto, con Rocq .

La palabra «matita» significa «lápiz» en italiano (una herramienta de edición sencilla y muy extendida). Es una aplicación relativamente pequeña y sencilla, ^{[ 2 ]} cuya complejidad arquitectónica y de software está pensada para que los estudiantes la dominen, proporcionando una herramienta especialmente adecuada para probar ideas y soluciones innovadoras. Matita adopta un modo de edición basado en tácticas ; se generan objetos de prueba ( codificados en XML ) para su almacenamiento e intercambio.

Las variables existenciales son nativas en Matita, lo que permite una gestión más sencilla de los objetivos dependientes. ^{[ 3 ]}

Matita implementa un algoritmo de inferencia de tipos bidireccional ^{[ 4 ]} que explota tanto los tipos inferidos como los esperados.

El poder del sistema de inferencia de tipos (refinador) se ve aumentado aún más por un mecanismo de sugerencias ^{[ 5 ]} que ayuda a sintetizar unificadores en situaciones particulares especificadas por el usuario.

Matita admite una estrategia de desambiguación sofisticada ^{[ 6 ]} basada en un diálogo entre el analizador sintáctico y el verificador de tipos .

A nivel interactivo, el sistema implementa una ejecución paso a paso de tácticas estructuradas ^{[ 7 ]} que permite una gestión mucho mejor del desarrollo de la prueba y, naturalmente, conduce a scripts más estructurados y legibles.

Matita ha trabajado en CerCo (Certified Complexity): un proyecto europeo del FP7 centrado en el desarrollo de un compilador formalmente verificado que preserva la complejidad, desde un gran subconjunto de C al lenguaje ensamblador de un microprocesador MCS-51 .

El tutorial de Matita ^{[ 8 ]} proporciona una introducción pragmática a las principales funcionalidades del demostrador de teoremas interactivo Matita, ofreciendo un recorrido guiado a través de un conjunto de ejemplos no triviales en el campo de la especificación y verificación de software .

• Correspondencia entre Curry y Howard
• Demostración interactiva de teoremas
• Teoría de tipos intuicionista
• Lista de asistentes de prueba

• El Asistente de Pruebas de Matita en Wayback Machine (archivado el 4 de febrero de 2023)
• Proyecto CerCo en Wayback Machine (archivado el 21/05/2022)