Carregant...
Fitxers
Tipus de document
ArticleVersió
Versió enviadaData de publicació
Si us plau utilitzeu sempre aquest identificador per citar o enllaçar aquest document: https://hdl.handle.net/2445/152102
Fundamentos de demostración automática de teoremas
Títol de la revista
Autors
ISSN de la revista
Títol del volum
Resum
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...
Descripció
Preprint enviat per a la seva publicació en una revista científica.
Matèries (anglès)
Citació
Citació
MARTÍNEZ ALONSO, Juan carlos. Fundamentos de demostración automática de teoremas. [consulta: 26 de novembre de 2025]. [Disponible a: https://hdl.handle.net/2445/152102]