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
type: CreativeWork
description: 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.|
abstract: 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: Ruiz Reina, José Luis
language: spa
license: http://creativecommons.org/licenses/by-nc-nd/4.0/
date published: 2001
date modified: 2026-07-24T04:29:54Z
provider: Universidad de Sevilla
publisher: Networked Digital Library of Theses and Dissertations
type: WebPage
source organization: Universidad de Sevilla

PropertyValue
property ID: Handle
value: http://hdl.handle.net/11441/23903