Lógica en informática - Logic in computer science

Para la conferencia académica LICS, consulte Simposio sobre lógica en informática .
Representación esquemática de puertas lógicas informáticas.

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:

  • Fundamentos teóricos y análisis
  • Uso de 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 (antes 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 . Church mostró por primera vez la existencia de problemas sin solución algorítmica 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". Además, algunas otras áreas importantes de superposición teórica entre la lógica y la informática son:

  • El teorema de la incompletitud de Gödel demuestra 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 demostrar 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 Curry-Howard es una relación entre sistemas lógicos y software. Esta teoría estableció 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, teoría de sistemas de transición, modelos de lenguajes de programación y teoría de la semántica de lenguajes de programación.

Computadoras para ayudar a los lógicos

Una de las primeras aplicaciones en utilizar el término inteligencia artificial fue el sistema lógico teórico 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 afirmaciones 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 le 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. Desde el principio se advirtió que este tipo de análisis podría ser de gran ayuda mediante el uso de computadoras. 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 computadoras

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 podí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í mismo simplemente no se usa como lenguaje de computadora 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, una compensación entre expresividad y computabilidad. Cuanto más expresivo es el lenguaje, más cercano está a FOL, más probable es que sea más lento y propenso a un bucle infinito.

Por ejemplo, SI ENTONCES las reglas utilizadas en los sistemas expertos se aproximan a un subconjunto muy limitado de FOL. En lugar de fórmulas arbitrarias con la gama completa 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 cálculos 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. Proyectos de investigación como los programas Knowledge Based Software Assistant y Programmer's Apprentice aplicaron la teoría lógica para validar la exactitud de las especificaciones del 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 formal impulsado por la transformación 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 tal dominio es el diseño de Very Large Scale Integrated (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 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 lenguajes de marco y clasificadores automáticos. Los lenguajes de marco 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 a los probadores de teoremas especializados llamados clasificadores analizar las diversas declaraciones entre conjuntos, subconjuntos y relaciones en un modelo dado. De esta manera, el modelo se puede validar y marcar las definiciones inconsistentes. 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 basada en nuevos datos. El nivel de flexibilidad es ideal para manejar el cambiante mundo de Internet. La tecnología de clasificador se basa en lenguajes como el lenguaje de ontología web para permitir un nivel semántico lógico en la Internet existente. Esta capa de se llama Web Semántica .

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

Ver también

Referencias

Otras lecturas

enlaces externos