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

El 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.|

Author dc:creator

• Ruiz Reina, José Luis

Advisor dc:contributor.advisor

• Alonso Jiménez, José Antonio

Statement dc:rights

• Atribución-NoComercial-SinDerivadas 4.0 España

Licence dc:rights.uri

• http://creativecommons.org/licenses/by-nc-nd/4.0/

Language dc:language.iso

spa

Handle dc:identifier.uri

http://hdl.handle.net/11441/23903

OAI identifier oai:identifier

oai:idus.us.es:11441/23903