Matita [1] es asistente de pruebas experimentales en desarrollo en el Departamento de Ciencias de la Computación de la Universidad de Bolonia . Es una herramienta que ayuda al desarrollo de pruebas formales mediante la colaboración hombre-máquina, proporcionando un entorno de programación donde coexisten de forma natural especificaciones formales, algoritmos ejecutables y 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 Coq .
La palabra "matita" significa "lápiz" en italiano (una herramienta de edición simple y generalizada). Es una aplicación razonablemente pequeña y simple, [2] cuya complejidad de arquitectura y software está destinada a ser dominada por los estudiantes, proporcionando una herramienta especialmente adecuada para probar ideas y soluciones innovadoras. Matita adopta un modo de edición basado en tácticas ; Los objetos de prueba ( codificados en XML ) se producen para su almacenamiento e intercambio.
Matita implementa un algoritmo de inferencia de tipo bidireccional [4] explotando tanto los tipos inferidos como los esperados.
El poder del sistema de inferencia de tipos (refinador) se ve reforzado por un mecanismo de sugerencias [5] que ayuda a sintetizar unificadores en situaciones particulares especificadas por el usuario.
Matita admite una sofisticada estrategia de desambiguación [6] basada en un diálogo entre el analizador y el comprobador de tipos .