Estadísticas del PDF: Razonamiento automático en lógica de primer orden

Razonamiento automático en lógica de primer orden

Juan J. Arrabal, José A. Alonso, Delia Balbontín y Javier Herrera
Departamento de Álgebra, Computación, Geometría y Topología

Facultad de Matemáticas

Universidad de Sevilla

12 de Julio de 1992

1 Introducción

El objetivo del presente trabajo consiste en una
demostración de las posibilidades del programa
OTTER [McCune 90] para la demostración au-
tomática de teoremas de Lógica de primer or-
den. Para dicha demostración hemos elegi-
do como ca...