Evaluación automatica de fórmulas del sistema K1
Informatica e Diritto › Numero 1983-2, Giugno 1983
Legato come :
Riassunto
Evaluación automatica de fórmulas del sistema K1
El programa que presentamos aquí constituye una version simplificada de un programa más amplio que incluye además de las rutinas que componen el que aquí exponemos, una rutina para lñ comprobación de sí la fórmula que se pretende probar está bien formada o no (en esta versión más simple sólo se pueden introducir como datos fórmulas bien formadas), y otra rutina para la eliminación de negadores múltiplo en caso de que los hubiera. Asimismo las subratinas de fautores deóntícos y de juntores diádicos están elaboradas en esta versión de forma a que estén lo más próximas posible a la intuición. Nos han parecido oportunas todas estas simplificaciones dado el carácter introductorio de las jornadas.
La posibilidad de computar ciertos aspectos de la lógica tiene ya una larga historia cuyo comienzo puede situarse en los trabajos de Newell-Shtw-Si-mon (1957), y de Hao Wang (1960). Nos gustaría subrayar la importancia de este tipo de trabajos con unas palabras del profesor Quine que nos parecen sumamente significativas: «(...) la programación llega a ser la prueba del formalismo. Estar totalmente formalizado es estar programado, (...) Un programa tiene que ser el análisis ultimo de un formalismo, debido a la falta de intuición por parte de la máquina»1. Por supuesto que el programa que presentamos no constituye el análisis ultimo del sistema K1, pero...Vedere l´intero contenuto di questo documento
Collegamenti sponsorizzati
