Lógica en informática

La lógica en informática o Lógica en las ciencias de la computación 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:

• Fundamentos teóricos y análisis
• Uso de la tecnología informática para ayudar a los lógicos.
• Uso de conceptos de la lógica para aplicaciones informáticas

Fundamentos teóricos y análisis

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 (anteriormente 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. 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 puede llamarse un procedimiento mecánico y Kurt Gödel afirmó que encontró el análisis de Turing "perfecto". Además, algunas otras áreas importantes de superposición teórica entre la lógica y la informática son:

• El teorema de incompletitud de Gödel prueba que cualquier sistema lógico lo suficientemente poderoso como para caracterizar la aritmética contendrá enunciados que no se pueden probar ni refutar dentro de ese sistema. Esto tiene una aplicación directa a cuestiones teóricas relacionadas con la viabilidad de probar la integridad y corrección del software.
• El problema del marco es un problema básico que debe superarse cuando se utiliza la lógica de primer orden para representar los objetivos y el estado de un agente de inteligencia artificial.
• La correspondencia de Curry-Howard es una relación entre los sistemas lógicos y el software. Esta teoría establecía una correspondencia precisa entre pruebas y programas. En particular, mostró que los términos en el cálculo lambda de tipo simple corresponden a pruebas de lógica proposicional intuicionista.
• La teoría de categorías representa una visión de las matemáticas que enfatiza las relaciones entre estructuras. Está íntimamente ligado a muchos aspectos de la informática: sistemas de tipos para lenguajes de programación, la teoría de sistemas de transición, modelos de lenguajes de programación y la teoría de la semántica de lenguajes de programación.

Computadoras para ayudar a los lógicos

Una de las primeras aplicaciones en usar el término inteligencia artificial fue el sistema Logic Theorist desarrollado por Allen Newell, JC Shaw y Herbert Simon en 1956. Una de las cosas que hace un lógico es tomar un conjunto de declaraciones en lógica y deducir las conclusiones (enunciados adicionales) que deben ser verdaderas según las leyes de la lógica. Por ejemplo, si se da un sistema lógico que dice "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. Se comprendió desde el principio que este tipo de análisis podría verse significativamente ayudado por el uso de computadoras.Principia Mathematica. Además, los lógicos han utilizado sistemas posteriores para validar y descubrir nuevos teoremas y demostraciones lógicas.

Aplicaciones lógicas para computadoras

Siempre ha habido una fuerte influencia de la lógica matemática en el campo de la inteligencia artificial (IA). Desde el comienzo del campo se percibió que la tecnología para automatizar inferencias lógicas podría tener un gran potencial para resolver problemas y sacar conclusiones de los 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 IA. No existe un método conocido más general o poderoso para describir y analizar información que FOL. La razón por la que FOL en sí mismo simplemente no se usa como un lenguaje informático es que en realidad es demasiado expresivo, en el sentido de que FOL puede expresar fácilmente declaraciones que ninguna computadora, sin importar cuán poderosa sea, podría resolver. Por esta razón, toda forma de representación del conocimiento es, en cierto sentido, un compromiso entre expresividad y computabilidad. Cuanto más expresivo es el lenguaje, cuanto más cerca está de FOL, más probable es que sea más lento y propenso a un bucle infinito.

Por ejemplo, las reglas IF THEN utilizadas en los 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 admitir computación de alto rendimiento, especialmente si aprovechan los algoritmos de optimización y la compilación.

Otra área importante de investigación para la teoría lógica fue la ingeniería de software. Los proyectos de investigación como los programas Asistente de software basado en conocimientos y Aprendiz de programador aplicaron la teoría lógica para validar la corrección de las especificaciones de software. También los utilizaron para transformar las especificaciones en código eficiente en diversas plataformas y para probar la equivalencia entre la implementación y la especificación. Este enfoque impulsado por la transformación formal a menudo requiere 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 la falla del sistema tiene un costo humano o financiero excesivamente alto. Un ejemplo de dicho 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 es catastrófico. A diferencia del software, los chips no se pueden parchear ni actualizar. Como resultado, existe una justificación comercial para usar métodos formales para demostrar que la implementación corresponde a la especificación.

Otra importante aplicación de la lógica a la tecnología informática ha sido en el área de los lenguajes de marcos y los clasificadores automáticos. Los lenguajes de marcos como KL-ONE tienen una semántica rígida. Las definiciones en KL-ONE se pueden asignar directamente a la teoría de conjuntos y al cálculo de predicados. 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 forma, 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 en función de la 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 Web Ontology Language para permitir un nivel semántico lógico en Internet existente. Esta capa de se llama la web semántica.

La lógica temporal se utiliza para razonar en sistemas concurrentes.