La lógica en informática cubre la superposición entre el campo de la lógica y el de la informática . Básicamente, el tema se puede dividir 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 importantes son la teoría de la computabilidad (anteriormente llamada teoría de la recursividad), 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 mostró por primera vez la existencia de problemas algorítmicamente irresolubles utilizando su noción de definibilidad lambda. Turing dio el primer análisis convincente de lo que se puede llamar un procedimiento mecánico y Kurt Gödel afirmó que encontraba 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 utilizar el término inteligencia artificial fue el sistema teórico de la lógica 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 enunciados en lógica y deducir el conclusiones (declaraciones 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 declaraciones pueden ser numerosas y complejas. Desde el principio se comprendió que este tipo de análisis podía mejorarse significativamente mediante el uso de ordenadores. El teórico de la lógica 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 demostraciones matemáticas. [7]
Siempre ha habido una fuerte influencia de la lógica matemática en el campo de la inteligencia artificial (IA). Desde el inicio del campo se comprendió que la tecnología para automatizar inferencias lógicas podría tener un gran potencial para resolver problemas y sacar conclusiones a partir de hechos. Ron Brachman ha descrito la lógica de primer orden (FOL) como la métrica mediante la cual 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 FOL en sí simplemente no se utiliza como lenguaje informático es que en realidad es demasiado expresivo , en el sentido de que FOL puede expresar fácilmente declaraciones que ninguna computadora, por poderosa que sea, podría resolver jamás. Por esta razón, toda forma de representación del conocimiento es, en cierto sentido, una compensación entre expresividad y computabilidad . Cuanto más expresivo sea el lenguaje, cuanto más cercano esté a FOL, más probable será que sea más lento y propenso a un bucle infinito. [8]
Por ejemplo, las reglas SI-ENTONCES 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 llaman modus ponens . Como resultado, los sistemas basados en reglas pueden admitir computación de alto rendimiento, especialmente si aprovechan los algoritmos de optimización y la compilación. [9]
Por otro lado, 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 un alto poder expresivo e implementaciones eficientes . En particular, el lenguaje de programación lógica Prolog es un lenguaje de programación completo de Turing . Datalog amplía 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 ) .
Otra área importante de investigación para la teoría lógica es la ingeniería de software . Proyectos de investigación como los programas Asistente de software basado en el conocimiento y Aprendiz de programador han aplicado la teoría lógica para validar la exactitud de las especificaciones del software . También han utilizado herramientas lógicas para transformar las especificaciones en código eficiente en diversas plataformas y 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 sistemas de armas, sistemas de seguridad y sistemas financieros en tiempo real, donde la falla del sistema tiene un costo humano o financiero excesivamente alto. Un ejemplo de tal dominio 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 marco y los clasificadores automáticos. Los lenguajes marco como KL-ONE se pueden asignar directamente a la teoría de conjuntos y la lógica de primer orden. Esto permite a los demostradores de teoremas especializados llamados clasificadores analizar las diversas declaraciones entre conjuntos , subconjuntos y relaciones en un modelo determinado. De esta manera se puede validar el modelo y marcar cualquier definición inconsistente. El clasificador también puede inferir nueva información, por ejemplo definir nuevos conjuntos basándose en información existente y cambiar la definición de conjuntos existentes basándose en nuevos datos. El nivel de flexibilidad es ideal para manejar el mundo en constante cambio de Internet. La tecnología de clasificación se basa en lenguajes como Web Ontology Language para permitir un nivel semántico lógico además de Internet existente. Esta capa se llama Web Semántica . [12] [13]
La lógica temporal se utiliza para el razonamiento en sistemas concurrentes . [14]
La buena noticia al reducir el servicio KR a la demostración de teoremas es que ahora tenemos una noción muy clara y específica de lo que debería hacer el sistema KR; 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.