Fundamentos de demostración automática de teoremas

Abstract

La Demostración Automática de Teoremas es actualmente un área de interés dentro de la Inteligencia Artificial. El problema general que se plantea en la Demostración Automática de Teoremas es el de encontrar métodos mecánicos para demostrar teoremas que se puedan llevar a la práctica. Los primeros avances importantes en este campo son debidos a Herbrand, que en el año 1930 presentó un primer método de demostración automática. De este método presentado por Herbrand se deduce que, bajo ciertas condiciones, es posible construir un programa de tal forma que si le suministramos como entrada una condición formal convenientemente codificada, el programa nos da una demostración de esa condición, en el caso en que dicha condición sea cierta. Las condiciones formales para las que se puede utilizar este método de demostración automática son enunciados que se pueden describir mediante fórmulas de un lenguaje de predicados sin el símbolo de identidad.. Sin embargo, se vio más adelante que dicho método resultaba ineficiente a la hora de llevarlo a la práctica. En el año 1965, Robinson introdujo el método de Resolución, que es un refinamiento del método desarrollad.o anteriormente por Herbrand. Sin embargo, el método de Resolución resultó ser mucho más eficiente que los métodos de demostración automática que se habían desarrollado hasta entonces. Actualmente, es un método básico de demostración automática que se utiliza en problemas de Inteligencia Artificial...