Buscar
Mostrando ítems 1-7 de 7
Tesis Doctoral
Operadores de generalización para el aprendizaje clausal
(2002)
"En esta memoria hemos estudiado los procesos de generalización, el paso de lo particular a lo general, cuando la información está expresada en lenguaje clausal. Para ello hemos definido unos operadores adaptados a los ...
Tesis Doctoral
Tesis Doctoral
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
(2001)
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 ...
Tesis Doctoral
Verificación formal en ACL2 del Algoritmo de Buchberger
(2003-12-18)
En este trabajo se han desarrollado los elementos necesarios para especificar, implementar y verificar la correción del algoritmo de Buchberger para el cálculo de bases de Gröbner, utilizando para ello un sistema de ...
Tesis Doctoral
Teoría computacional (en ACL2) sobre cálculos proposicionales
(2002)
En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2.
Tesis Doctoral
Tesis Doctoral
Formalización en Isar de la metalógica de primer orden
(2012-06-12)
El objetivo del trabajo es formalizar razonamiento complejo de forma legible por los humanos y procesable por las máquinas. Más precisamente, formalizar en el sistema de razonamiento Isabelle/HOL/Isar la metateoría de la ...