Resumen

Las matrices de funciones, en las cuales los elementos son funciones en lugar de números, se utilizan ampliamente en el análisis de modelos de sistemas dinámicos como sistemas de control y robótica. En aplicaciones críticas de seguridad, se requiere analizar formal y exactamente los sistemas dinámicos para garantizar su corrección y seguridad. La demostración de teoremas de lógica de orden superior (HOL) es una técnica prometedora para cumplir con este requisito. Este artículo propone una formalización de la lógica de orden superior de la teoría de vectores de funciones y matrices de funciones utilizando el demostrador de teoremas HOL, incluyendo tipos de datos, operaciones y sus propiedades, y además presenta una formalización de la diferenciación e integración de vectores de funciones y matrices de funciones. La formalización se implementa como una biblioteca en el sistema HOL. Se presenta un estudio de caso, un análisis formal de la diferenciación de funciones cuadráticas, para mostrar la utilidad de la formalización propuesta.

• 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:Funciones de matrices; Sistemas dinámicos; Sistemas de control; Robótica; Lógica de orden superior; Demostración de teoremas
• Keywords:Function matrices; Dynamic systems; Control systems; Robotics; Higher-order logic; Theorem proving