Contribución al estudio de la demostración automática

Abstract

La memoria empieza con un breve estudio de los procedimientos convencionales de demostracion automatica, se idea un sistema novedoso llamado de inferencia directa, que se caracteriza por basar la deduccion en el concepto de pertenencia a un conjunto. Se estudia la manera de representar los conceptos logicos de la logica de predicados monadicos con el nuevo lenguaje que surge a partir de la inferencia directa. Se crea asimismo el concepto de codicion restrictiva para completar el conocimiento existente en una manifestacion logica. Se estudia y deduce una operacion entre manifestaciones llamada operacion de acumulacion, para establecer el conjunto a partir del cual queremos extraer las conclusiones. Un nuevo concepto de conclusion ayudara a realizar la inferencia de una forma rapida y eficaz. El calculo creado se extiende de forma inmediata a las manifestaciones de la logica proposicional y a la logica de predicados monadicos plurivariables. En este ultimo caso deben crearse las premisas asumidas que deben añadirse a la acumulacion de las premisas originales, y las preguntas asumientes que deben añadirse a la conclusion original. Se crean dos programas para mecanizar el proceso de demostracion y se hace un estudio de la bondad y eficacia de los mismos.