Razón para aprender lógica proposicional y predicada

Puedo entender la importancia de que los informáticos o cualquier ingeniero relacionado con el desarrollo de software deberían haber entendido el estudio de la lógica básica como base.

Pero, ¿hay tareas / trabajos que requieran explícitamente el conocimiento sobre estos, aparte de las tareas que requieren algún tipo de representación de conocimiento Knowledge Base? Quiero escuchar los tipos de tareas, en lugar de respuestas conceptuales.

La razón por la que pregunto esto es solo por mi curiosidad. Mientras que los estudiantes de CS tienen que pasar una cierta cantidad de tiempo en este tema, algunos cursos intensivos en practicidad (por ejemplo , Clase AI ) omitieron este tema por completo. Y solo me pregunto que, por ejemplo, saber predicate logicpodría ayudar a dibujar, ER diagrampero podría no ser un requisito.

Actualización 27/05/2012) Gracias por las respuestas. Ahora creo que entiendo totalmente y estoy de acuerdo con la importancia de logicCS con su gran cantidad de aplicaciones. Acabo de elegir la mejor respuesta realmente de la impresionante que obtuve con la solución para el Windows'problema de la pantalla azul'.

Tiendo a gustarme la unificación y todo lo relacionado con ella. Si no conoce la lógica proposicional y de predicados, está omitiendo los conceptos básicos de la lógica. Si tiene interés en algo de la lista , sería como tener interés en las matemáticas y omitir la suma y la multiplicación. La lógica no es solo para la IA.

Como respuesta práctica, ¿recuerda el problema de coma flotante de Intel y cómo ya no los ve? Gracias al uso de demostradores de teoremas, son cosa del pasado. Recuerda la pantalla azul de la muerte de Microsoft . Gracias a los solucionadores SAT, la verificación de modelos y otras soluciones basadas en la lógica, son una especie en peligro de extinción.

Hay conexiones extremadamente profundas y penetrantes entre la lógica y la informática. Al comprender cuáles podrían ser, tenga en cuenta que la informática también se denomina "tecnología de la información" o "informática", lo que significa que los sistemas informáticos capturan, procesan y entregan información. Bueno, la lógica es una cosa similar. Estudia cómo se captura la información en las oraciones y cómo es posible que una declaración sea consecuencia de otra, es decir, cómo su contenido de información ya está presente en otra declaración (o colección de declaraciones). En ese sentido, la lógica y la informática son esencialmente las mismas.disciplina, centrándose en diferentes aspectos. Los lógicos (Church, Kleene, Turing, Post y sus estudiantes y colegas) crearon la disciplina de la informática, y muchos lógicos continúan haciendo contribuciones a la informática, especialmente Jean-Yves Girard y sus alumnos.

Aquí hay algunas aplicaciones estándar de lógica en informática:

• El diseño de los circuitos digitales se basa completamente en la lógica de la propuesta, tanto que sus ingenieros lo llaman "diseño lógico" en lugar de "diseño de circuito". Incluso se suele pensar que escribir un programa de computadora implica diseñar su "lógica". (Tenga en cuenta que "lógica" en este último sentido es una idea informal en lugar de lógica formal, utilizada para referirse al flujo de información a través del programa y si se está procesando correctamente).

• La lógica de predicados y su primo matemático, la teoría de conjuntos, se utilizan en una variedad de lenguajes de computación , por ejemplo, el lenguaje SQL para consultas de bases de datos relacionales. También hay lenguajes de programación basados ​​en lógica, llamados "lenguajes de programación lógica".

• La representación del conocimiento , que ya ha mencionado, tiene muchos formalismos basados ​​en la lógica. Incluso si usa formalismos no lógicos, muchos de ellos todavía tienen un significado lógico y, por lo tanto, se basan en la lógica.

• La lógica probabilística, donde las declaraciones no solo tienen valores verdaderos / falsos, sino niveles de certeza / incertidumbre, es cada vez más la base de los sistemas de aprendizaje automático .

• Si desea establecer formalmente lo que hace un programa, es decir, dar una especificación de programa , terminará usando alguna forma de lenguaje lógico. De hecho, hay muchos lenguajes de especificación de programas, como Z y B, que se basan en la lógica de predicados y la teoría de conjuntos. También hay lenguajes de especificación basados ​​en la lógica de la ecuación, como Larch. Los informáticos a menudo inventan nuevas lógicas para representar las necesidades de la informática, por ejemplo, la lógica de Hoare y la lógica de separación, o recogen y desarrollan varias formas infrautilizadas de lógicas tradicionales, como la lógica temporal y la lógica modal, y las desarrollan aún más.

• Si quieres verificar si un programa hace lo que se supone que debe hacer, entonces terminas usando no solo el lenguaje de la lógica, sino toda la maquinaria de la lógica: teoría de la prueba, teoría del modelo y procedimientos de decisión. La tecnología de verificación ahora está creciendo a pasos agigantados y espero que, en una década más o menos, se usen de forma rutinaria para casi todo el desarrollo de software.

De hecho, las conexiones entre la lógica y la informática son tan profundas y generalizadas que diría que es difícil ser un buen científico de la computación sin una comprensión profunda de la lógica.

La razón por la que algunos científicos de IA subestiman la lógica en este momento es que algunos de los primeros desarrolladores de IA habían propuesto la lógica comercial como una herramientaen lugar de una base. La IA, por su propia naturaleza, promete entregar magia. No tenemos que hacer el trabajo duro de los sistemas de programación para entregar resultados. Podrían descubrir por sí mismos cómo producir soluciones porque serían "inteligentes". La lógica parecía indicar el camino porque si los sistemas informáticos entendieran la lógica y supieran cómo procesar la información utilizando las reglas de la lógica, serían capaces de entregar magia. Ese tipo de fe en la lógica fue, en retrospectiva, fuera de lugar. En primer lugar, la lógica estándar es demasiado fuerte y demasiado débil al mismo tiempo. Es demasiado fuerte en el sentido de que las reglas de la lógica son demasiado generales para idear procedimientos efectivos. También es demasiado débil porque es la lógica ideada por los matemáticos para las necesidades de las matemáticas y no No tiene el vocabulario necesario para lidiar con muchos otros tipos de información del mundo real que los sistemas de IA deben manejar (como la incertidumbre, la información contextual como el tiempo, el cambio, el conocimiento, la agencia, etc.). Entonces, AI está experimentando una reacción violenta contra la lógica. Pero creo que, cuando superen esa reacción violenta, los científicos de IA se darán cuenta de que todos los métodos más nuevos todavía se basan enlógica, ampliamente interpretada .

La lógica es fundamental para toda la informática teórica. Sin aprender esto, no podrá comprender adecuadamente la semántica del lenguaje de programación, las máquinas de Turing, la programación lógica, la computabilidad, etc. Incluso razonar sobre sus programas será más difícil sin él. Ciertamente, tratar de hacer una prueba matemática de algún concepto de CS es prácticamente imposible.

O tal vez está preguntando sobre usos en la industria. La lógica de aprendizaje forma la base para aprender a razonar claramente y ver agujeros en los argumentos de otras personas. La lógica es fundamental, ya sea que use los símbolos formales o no.

Una de las tareas repetitivas que enfrentan los teóricos y profesionales de CS es ganar confianza en la exactitud de su código.

Hay dos enfoques principales:

1. Prueba: cree una prueba lógica de que parte de un sistema tiene ciertas propiedades, posiblemente ayudadas por precondiciones, diseño por contrato, verificadores de código.
2. Prueba: compruebe que ciertas propiedades se mantienen para una variedad de entradas y luego induzca que esa propiedad se mantenga para otras entradas.

La primera, basada en métodos lógicos, suele ser la única opción cuando

1. No hay entrada típica. Por ejemplo, cuando se prueban las propiedades de seguridad, son las entradas atípicas de las que debe preocuparse, a menos que pueda razonar lógicamente sobre qué entradas son atípicas, es poco probable que obtenga una buena cobertura.
2. El espacio de configuración es muy grande, por lo que debe descomponerlo en partes razonando lógicamente qué partes pueden afectar a qué otras partes antes de realizar la prueba localmente.
3. Solo tiene documentación que describe el comportamiento de casos extremos de sistemas fuera de su control. Es posible que pueda simularlos, pero no puede probar qué sucede cuando falla una dependencia externa porque no es capaz de hacer que falle por razones legales o éticas.

La prueba empírica en ausencia de una prueba es básicamente un sustituto de la prueba. Cuando diseña un sistema para que sea comprobable, está creando un boceto de prueba en el que completa partes de la prueba con "prueba X, Y y Z aquí". La capacidad de razonar lógicamente es esencial para poder diseñar un sistema comprobable. Si el sistema no es comprobable o demostrable, entonces su diseñador / arquitecto no tiene por qué decir que es apto para su uso previsto.

Los dos campos más importantes en los que la lógica juega un papel vital son:

1. Especificación y verificación del lenguaje formal .
2. Parámetros fijos clases manejables .

Parece que necesita alguna aclaración, en los lenguajes formales debe trabajar extremadamente en la lógica, para aclarar, eche un vistazo a: 1. Lenguaje formal . 2. Introducción a$Z$.

En resumen: 1. La definición del lenguaje necesita lógica, 2: la justicia de sus procedimientos necesita lógica, 3. los procedimientos de verificación necesitan lógica.

Debo mencionar que esto es diferente del diseño del compilador o ..., esta es una definición "formal" de los idiomas, la razón principal para hacerlo es demostrar la corrección del lenguaje o modelo, también tener una prueba formal. Esto puede usarse para verificar modelos de software, encontrar errores antes de implementar, encontrar puntos muertos nuevamente antes de implementar ... Para software que simule esto, puede echar un vistazo a NModel .

Ahora, ¿por qué en los problemas manejables de parámetros fijos necesita trabajar con lógica? Puede dividir las clases de manejabilidad de parámetros fijos con diferentes niveles de lógica, se pueden convertir entre sí: lógica a autómata, autómata a gráfico y viceversa, pero si ser un experto en lógica puede dividir y decidir sobre ellos simplemente, el teorema más importante (después del teorema de Robertson y Seymour ), en este campo es el teorema de Courcelle . para más información lea la encuesta del Teorema Algorítmico Meta .