De Wikipedia, la enciclopedia libre
Saltar a navegación Saltar a búsqueda
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 [ editar ]

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 . [1] [2] 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".[3] 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 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 demostrar la integridad y corrección del software. [4]
  • 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. [5]
  • 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. [6]

Computadoras para ayudar a los lógicos [ editar ]

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 deBertrand 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. [7]

Aplicaciones lógicas para computadoras [ editar ]

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 por la cual toda la representación del conocimiento de la IAdeben evaluarse los formalismos. 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. [8]

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. [9]

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. [10] 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 Very Large Scale Integrated (VLSI)diseño: 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. [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. Lenguajes de marco como KL-ONEtienen 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 clasificadores 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 .[12] [13]

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

Ver también [ editar ]

  • Razonamiento automatizado
  • Lógica computacional
  • Programación lógica

Referencias [ editar ]

  1. ^ Lewis, Harry R. (1981). Elementos de la teoría de la computación . Prentice Hall .
  2. ^ Davis, Martin (11 de mayo de 1995). "Influencias de la lógica matemática en la informática" . En Rolf Herken (ed.). La máquina universal de Turing . Springer Verlag. ISBN 9783211826379. Consultado el 26 de diciembre de 2013 .
  3. ↑ Kennedy, Juliette (21 de agosto de 2014). Interpretando a Godel . Prensa de la Universidad de Cambridge. ISBN 9781107002661. Consultado el 17 de agosto de 2015 .
  4. ↑ Hofstadter, Douglas R. (5 de febrero de 1999). Gödel, Escher, Bach: una eterna trenza dorada . Libros básicos. ISBN 978-0465026562.
  5. ^ McCarthy, John ; PJ Hayes (1969). "Algunos problemas filosóficos desde el punto de vista de la inteligencia artificial" (PDF) . Inteligencia de máquina . 4 : 463–502.
  6. ^ Barr, Michael; Charles Wells (1998). Teoría de categorías para ciencias de la computación (PDF) . Centre de Recherches Mathématiques .
  7. ^ Newell, Allen; JC Shaw; HC Simon (1963). "Exploraciones empíricas con la máquina de teoría lógica" . En Ed Feigenbaum (ed.). Computadoras y pensamiento . McGraw Hill. págs.  109-133 . ISBN 978-0262560924.
  8. ^ Levesque, Héctor; Ronald Brachman (1985). "Una compensación fundamental en la representación y el razonamiento del conocimiento" . En Ronald Brachman y Hector J. Levesque (ed.). Lectura en representación del conocimiento . Morgan Kaufmann. pag. 49 . ISBN 0-934613-01-X. La buena noticia al reducir el servicio KR a la demostración de teoremas es que ahora tenemos una noción muy clara y muy 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.
  9. ^ Forgy, Charles (1982). "Rete: un algoritmo rápido para el problema de coincidencia de patrones de muchos patrones / muchos objetos *" (PDF) . Inteligencia artificial . 19 : 17–37. doi : 10.1016 / 0004-3702 (82) 90020-0 . Archivado desde el original (PDF) el 27 de diciembre de 2013 . Consultado el 25 de diciembre de 2013 .
  10. ^ Rich, Charles; Richard C. Waters (noviembre de 1987). "El proyecto de aprendiz de programador: una visión general de la investigación" (PDF) . Experto IEEE . Consultado el 26 de diciembre de 2013 .
  11. ^ Stavridou, Victoria (1993). Métodos formales en el diseño de circuitos . Sindicato de Prensa de la Universidad de Cambridge. ISBN 0-521-443369. Consultado el 26 de diciembre de 2013 .
  12. ^ MacGregor, Robert (junio de 1991). "Utilización de un clasificador de descripción para mejorar la representación del conocimiento". Experto IEEE . 6 (3): 41–46. doi : 10.1109 / 64.87683 . S2CID 29575443 . 
  13. ^ Berners-Lee, Tim ; James Hendler; Ora Lassila (17 de mayo de 2001). "La Web Semántica Una nueva forma de contenido web que es significativo para las computadoras desatará una revolución de nuevas posibilidades" . Scientific American . 284 : 34–43. doi : 10.1038 / scientificamerican0501-34 . Archivado desde el original el 24 de abril de 2013.
  14. ^ Colin Stirling (1992). "Lógicas modal y temporal". En S. Abramsky; DM Gabbay; TSE Maibaum (eds.). Manual de Lógica en Informática . II . Prensa de la Universidad de Oxford. págs. 477–563. ISBN 0-19-853761-1.

Lectura adicional [ editar ]

  • Ben-Ari, Mordejai (2012). Lógica matemática para la informática (3ª ed.). Springer-Verlag. ISBN 978-1447141280.
  • Harrison, John (2009). Manual de lógica práctica y razonamiento automatizado (1ª ed.). Prensa de la Universidad de Cambridge. ISBN 978-0521899574.
  • Huth, Michael; Ryan, Mark (2004). Lógica en Ciencias de la Computación: Modelado y Razonamiento de Sistemas (2ª ed.). Prensa de la Universidad de Cambridge. ISBN 978-0521543101.
  • Burris, Stanley N. (1997). Lógica para las matemáticas y la informática (1ª ed.). Prentice Hall. ISBN 978-0132859745.

Enlaces externos [ editar ]

  • Artículo sobre lógica e inteligencia artificial en la Enciclopedia de Filosofía de Stanford .
  • Simposio IEEE sobre Lógica en Ciencias de la Computación (LICS)
  • Alwen Tiu, Introducción a la grabación de video de lógica de una conferencia en ANU Logic Summer School '09 (dirigida principalmente a científicos informáticos)