Resumen

El documento presenta una prueba formal de un teorema de máquina cerrada de TLA en el sistema de demostración de teoremas Coq. Se emplea un esquema de incrustación superficial para la prueba que es independiente de la sintaxis concreta. Se necesitan conceptos fundamentales para afirmar que los teoremas de máquina cerrada son abordados en la plataforma de prueba. Se diseña un patrón de prueba útil para construir una traza con propiedades deseadas. Se establecen una serie de bibliotecas reutilizables de Coq.

• Materias:Modelos matemáticos Conjuntos difusos Ecuaciones integrales Fusión de características Algoritmo de optimización
• Subjects:Mathematical models Fuzzy sets Integral equations Feature fusion Optimization algorithm
• Palabras claves:Prueba; Teorema cerrado de máquina; TLA; Coq; Esquema de incrustación superficial; Traza;
• Keywords:Proof; Machine closed theorem; TLA; Coq; Shallow embedding scheme; Trace;