Resumen

La demostración de teoremas es un enfoque importante en la verificación formal. La lógica de orden superior es una forma de lógica de predicados que se distingue de la lógica de primer orden por tener cuantificadores adicionales y una semántica más fuerte. La lógica de orden superior es más expresiva. Este artículo presenta la formalización de la teoría de espacios lineales en HOL4. Un conjunto de propiedades es caracterizado en HOL4. Este resultado se utiliza para sentar las bases para la aplicación de la lógica de orden superior en un espectro más amplio de aplicaciones de ingeniería.

• Materias:Modelado matemático Modelo de red neuronal Tasa de convergencia Aritmética Ondículas libres
• Subjects:Mathematical modeling Neural network model Convergence rate Arithmetic Free wavelets
• Palabras claves:Demostración de teoremas; Verificación formal; Lógica de orden superior; Lógica de predicados; HOL4; Aplicaciones en ingeniería
• Keywords:Theorem proving; Formal verification; Higher-order logic; Predicate logic; HOL4; Engineering applications