Lógica en informática.

La lógica en la 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:

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

Fundaciones y análisis teóricos

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 programación lógica, 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 se puede llamar un procedimiento mecánico y Kurt Gödel afirmó que encontraba el análisis de Turing "perfecto". La programación lógica se basa en la evidencia de que la lógica se puede utilizar tanto para la representación del conocimiento como como lenguaje de programación. Esta conexión sigue evolucionando hacia la lógica computacional. Además, algunas otras áreas importantes de superposición teórica entre la lógica y la informática son:

• El teorema de incompleto de Gödel demuestra que cualquier sistema lógico lo suficientemente poderoso para caracterizar aritmética contendrá declaraciones que no pueden ser probadas ni refutadas dentro de ese sistema. Esto tiene 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 al usar la lógica de primer orden para representar los objetivos y el estado de un agente de inteligencia artificial.
• La correspondencia Curry-Howard es una relación entre los sistemas lógicos y el software. Esta teoría estableció una correspondencia precisa entre pruebas y programas. En particular mostró que los términos en el cálculo de lambda simplemente escrito corresponden a pruebas de la lógica proposición intuitionista.
• La teoría de la categoría representa una visión de las matemáticas que enfatiza las relaciones entre las estructuras. Está íntimamente ligada a muchos aspectos de la ciencia informática: sistemas de tipo 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 lenguaje de programación.

Ordenadores para ayudar a los lógicos

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 las conclusiones (declaraciones adicionales) que deben ser verdaderas según las leyes de la lógica. Por ejemplo, si se le 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 lógicas.

Aplicaciones lógicas para ordenadores

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. 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í 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.

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.

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-difíciles).

Otra área importante de investigación de 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. 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.

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 al cálculo de predicados. 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.

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