La lógica en informática cubre la superposición entre el campo de la lógica y el de la informática . El tema se puede dividir esencialmente en tres áreas principales:
La lógica juega un papel fundamental en la informática. Algunas de las áreas clave de la lógica que son particularmente significativas son la teoría de la computabilidad (antes llamada teoría de la recursión), la lógica modal y la teoría de categorías . La teoría de la computación se basa en conceptos definidos por lógicos y matemáticos como Alonzo Church y Alan Turing . [1] [2] Church fue el primero en demostrar la existencia de problemas algorítmicamente irresolubles utilizando su noción de definibilidad lambda. Turing realizó el primer análisis convincente de lo que puede llamarse un procedimiento mecánico y Kurt Gödel afirmó que encontró el análisis de Turing "perfecto". [3] Además, algunas otras áreas importantes de superposición teórica entre la lógica y la informática son:
Una de las primeras aplicaciones en las que se utilizó el término inteligencia artificial fue el sistema Logic Theorist desarrollado por Allen Newell , Cliff Shaw y Herbert Simon en 1956. Una de las cosas que hace un lógico es tomar un conjunto de afirmaciones en lógica y deducir las conclusiones (afirmaciones adicionales) que deben ser verdaderas según las leyes de la lógica. Por ejemplo, si se dan las afirmaciones "Todos los humanos son mortales" y "Sócrates es humano", una conclusión válida es "Sócrates es mortal". Por supuesto, este es un ejemplo trivial. En los sistemas lógicos reales, las afirmaciones pueden ser numerosas y complejas. Se comprendió desde el principio que este tipo de análisis podría verse significativamente facilitado por el uso de computadoras. Logic Theorist validó el trabajo teórico de Bertrand Russell y Alfred North Whitehead en su influyente trabajo sobre lógica matemática llamado Principia Mathematica . Además, los lógicos han utilizado sistemas posteriores para validar y descubrir nuevos teoremas y pruebas matemáticas. [7]
La lógica matemática siempre ha ejercido una fuerte influencia en el campo de la inteligencia artificial (IA). Desde el comienzo de este campo, se comprendió que la tecnología para automatizar inferencias lógicas podría tener un gran potencial para resolver problemas y extraer conclusiones de los hechos. Ron Brachman ha descrito la lógica de primer orden (FOL) como la métrica con la que se deben evaluar todos los formalismos de representación del conocimiento de la IA . La lógica de primer orden es un método general y poderoso para describir y analizar información. La razón por la que la FOL en sí misma simplemente no se utiliza como lenguaje informático es que, en realidad, es demasiado expresiva , en el sentido de que puede expresar fácilmente afirmaciones que ninguna computadora, por potente que sea, podría resolver jamás. Por esta razón, toda forma de representación del conocimiento es, en cierto sentido, un equilibrio entre expresividad y computabilidad . Cuanto más expresivo sea el lenguaje, cuanto más se acerque a la FOL, más probabilidades hay de que sea más lento y propenso a un bucle infinito. [8]
Por ejemplo, las reglas IF-THEN utilizadas en sistemas expertos se aproximan a un subconjunto muy limitado de FOL. En lugar de fórmulas arbitrarias con toda la gama de operadores lógicos, el punto de partida es simplemente lo que los lógicos denominan modus ponens . Como resultado, los sistemas basados en reglas pueden soportar cálculos de alto rendimiento, especialmente si aprovechan los algoritmos de optimización y la compilación. [9]
Por otra parte, la programación lógica , que combina el subconjunto de cláusulas de Horn de la lógica de primer orden con una forma no monótona de negación , tiene tanto un alto poder expresivo como implementaciones eficientes . En particular, el lenguaje de programación lógica Prolog es un lenguaje de programación completo de Turing . Datalog extiende el modelo de base de datos relacional con relaciones recursivas, mientras que la programación de conjuntos de respuestas es una forma de programación lógica orientada a problemas de búsqueda difíciles (principalmente NP-hard ) .
Otro campo importante de investigación de la teoría lógica es la ingeniería de software . Proyectos de investigación como el Asistente de Software Basado en Conocimiento y los programas Aprendiz de Programador han aplicado la teoría lógica para validar la exactitud de las especificaciones de software . También han utilizado herramientas lógicas para transformar las especificaciones en código eficiente en diversas plataformas y para demostrar la equivalencia entre la implementación y la especificación. [10] Este enfoque formal impulsado por la transformación suele requerir mucho más esfuerzo que el desarrollo de software tradicional. Sin embargo, en dominios específicos con formalismos apropiados y plantillas reutilizables, el enfoque ha demostrado ser viable para productos comerciales. Los dominios apropiados suelen ser aquellos como los sistemas de armas, los sistemas de seguridad y los sistemas financieros en tiempo real donde el fallo del sistema tiene un coste humano o financiero excesivamente alto. Un ejemplo de un dominio de este tipo es el diseño integrado a muy gran escala (VLSI) , el proceso para diseñar los chips utilizados para las CPU y otros componentes críticos de los dispositivos digitales. Un error en un chip puede ser catastrófico. A diferencia del software, los chips no se pueden parchear ni actualizar. Como resultado, existe una justificación comercial para utilizar métodos formales para demostrar que la implementación corresponde a la especificación. [11]
Otra aplicación importante de la lógica a la tecnología informática ha sido en el área de los lenguajes de marco y los clasificadores automáticos. Los lenguajes de marco como KL-ONE se pueden mapear directamente a la teoría de conjuntos y la lógica de primer orden. Esto permite que los probadores de teoremas especializados llamados clasificadores analicen las diversas declaraciones entre conjuntos , subconjuntos y relaciones en un modelo dado. De esta manera, el modelo se puede validar y cualquier definición inconsistente se puede marcar. El clasificador también puede inferir nueva información, por ejemplo, definir nuevos conjuntos basados en información existente y cambiar la definición de conjuntos existentes en función de nuevos datos. El nivel de flexibilidad es ideal para manejar el mundo en constante cambio de Internet. La tecnología de clasificadores se basa en lenguajes como el lenguaje de ontología web para permitir un nivel semántico lógico sobre la Internet existente. Esta capa se llama Web semántica . [12] [13]
La lógica temporal se utiliza para razonar en sistemas concurrentes . [14]
La buena noticia de reducir el servicio de KR a la demostración de teoremas es que ahora tenemos una noción muy clara y muy específica de lo que el sistema de KR debería hacer; la mala noticia es que también está claro que los servicios no se pueden proporcionar... decidir si una oración en FOL es o no un teorema... es irresoluble.