Demostracion Acl2

Universidad de Cádiz Departamento de Lenguajes y Sistemas Informáticos

Razonamiento automático La Lógica Computacional ACL 2: El demostrador de teoremas

Profesores Inmaculada Medina BuloFrancisco Palomo Lozano

El demostrador de teoremas ACL 2
ACL 2 es un demostrador de teoremas automatizado Técnicas de demostración (procesos )
Simplificación Eliminación de destructores

Uso deequivalencias

Usuario

Fórmulas

Generalización

Eliminación de irrelevancias Inducción

1

Razonamiento automático. I. Medina & F. Palomo

El demostrador de teoremas ACL 2
Definición deteoremas

(defthm nombre fórmula :rule-classes clases de reglas :hints consejos )
El demostrador es automatizado más que «automático» Conducido por la estrategia del usuario Tipos de reglas:reescritura (:rewrite); equivalencia (:equivalence); congruencia (:congruence); relación bien fundamentada (:well-founded-relation); eliminación de destructores (:elim); . . . Tipos de consejos:des/activaciones, inducciones, . . .

:in-theory, :do-not, :expand, :use, :induct, :cases, . . .
2 Razonamiento automático. I. Medina & F. Palomo

Técnicas o procesos de demostración
Simplificación Es elúnico proceso que puede devolver un conjunto vacío de fórmulas, demostrando así que su fórmula de entrada es un teorema Consta de procedimientos de decisión

− Lógica proposicional, igualdad,aritmética lineal
Sistema de reescritura de términos (usando definiciones,. . . ) Soporta también reescritura de términos basada en congruencias Información de tipos Eliminación de destructores Permite que lasvariables afectadas por operaciones destructoras sean sustituidas por términos formados por operaciones constructoras y varia3 Razonamiento automático. I. Medina & F. Palomo

bles nuevas Sesustituyen términos complicados por otros más simples Uso de equivalencias Controla heurísticamente cuándo se deben utilizar y descartar una hipótesis de igualdad Si la hipótesis de igualdad proviene de...