Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades

Alonso Jiménez, José AntonioRuiz Reina, José Luis2015-04-162015-04-162001Ruiz Reina, J.L. (2001). Una teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedades. (Tesis Doctoral Inédita). Universidad de Sevilla, Sevilla.http://hdl.handle.net/11441/23903El objetivo principal de la Tesis es el desarrollo de una teoría computacional acerca de la lógica ecuacional, usando para ello el sistema ACL2. Es decir, se usa ACL2 para definir formalmente algoritmos y conceptos relacionados con la lógica ecuacional, y se llevan a cabo demostraciones automáticas de teoremas acerca de estos algoritmos y conceptos. Este trabajo de verificación formal se realiza en un entorno en el que se pueden combinar la demostración de teoremas con la ejecución de funciones.|application/pdfspaAtribución-NoComercial-SinDerivadas 4.0 Españahttp://creativecommons.org/licenses/by-nc-nd/4.0/ACL2 (Lenguaje de programación)Ecuaciones, Teoría deUna teoría computacional acerca de la lógica ecuacional formalización en ACL2 de la lógica ecuacional y demostración automática de sus propiedadesinfo:eu-repo/semantics/doctoralThesisinfo:eu-repo/semantics/openAccess