[MÚSICA] La inferencia se refiere a cómo podemos razonar con respecto a la semántica que dimos. Una regla de inferencia nos dice qué podemos deducir a partir de qué en un solo paso. La idea para poder deducir una fórmula a partir de otras en varios pasos es aplicar sucesivamente reglas de inferencia. Hay dos partes en una regla de inferencia, dadas las fórmulas de arriba de la línea, deducimos la fórmula de abajo de la línea. Como un ejemplo damos esta regla de inferencia, que por cierto you tenía teníamos. A partir de a y b, implica c por un lado, y a por otro, es correcto deducir que b implica c. La deducción natural tiene muchas reglas de inferencia y aquí solo listamos unas cuantas. Vemos por ejemplo que a partir de alfa y beta podemos deducir alfa. Similarmente a partir de dos fórmulas alfa y beta, podemos deducir la fórmula alfa y beta. Una regla importante que todavía conserva su nombre en latín es modus ponens, que podemos llamar eliminación de la implicación. Hay otra regla para introducir la implicación, reglas para eliminar e introducir la disyunción y la negación. De manera similar a la consecuencia lógica, ahora utilizamos este otro torniquete que se lee como infieren. Y afirma que a partir de la conjunción de las fórmulas del lado izquierdo podemos inferir el lado derecho aplicando reglas de inferencia. Un sistema de inferencia es un conjunto de reglas de inferencia. No forzosamente las reglas de la deducción natural. Vamos a decir que un sistema de inferencia es correcto si todo lo que podemos inferir con ese sistema es consecuencia lógica. Similarmente, un sistema de inferencia es completo si nos permite inferir todo lo que es consecuencia lógica. Queremos entonces sistemas de inferencia que sean tanto correctos como completos. Pasamos ahora al problema SAT. Un problema importante es saber si una fórmula dada es satisfactible o no. O sea, si existen o no modelos que la hagan cierta. Supongamos primero que la fórmula dada está en forma normal disyuntiva. Intuitivamente vemos que saber si esa fórmula es satisfactible es directo. Para que esa fórmula sea cierta basta con que cualquiera de sus términos sea cierto. Y para que un término sea cierto podemos elegir los valores de sus variables como sigue. Si una variable ocurre de manera positiva en una literal le asignamos cierto. Si ocurre de manera negativa, le asignamos falso. Es entonces fácil decidir si una fórmula en forma normal disyuntiva es satisfactible o no. Veamos ahora una fórmula en forma normal conjuntiva. Aquí debemos encontrar una asignación de variables que haga ciertas a todas las cláusulas simultáneamente. Y para que una cláusula sea cierta basta con hacer cualquiera de sus literales cierta. Sin embargo, intuitivamente esto es dificil porque al elegir el valor de una variable en una cláusula se restringen los valores de las otras ocurrencias de esa variable en otras cláusulas. Vamos a definir el problema SAT como satisfactivilidad para fórmulas en forma normal conjuntiva. Vamos ahora a hablar de la dificultad para resolver SAT. Consideremos dos problemas. El primero es SAT, es decir, dada una fórmula alfa en forma normal conjuntiva, ¿existe un modelo que haga cierta a alfa? Para contestar, debemos buscar modelos. El segundo problema se llama verificación de modelos. Ahora nos dan no solo la fórmula sino un modelo en particular y nos preguntan si ese modelo hace cierta a la fórmula. Intuitivamente es más fácil resolver el problema de la verificación de modelos, pues no es necesario buscar modelos. Basta con aplicar mecánicamente la definición de satisfacción. Formalmente decimos que toma un tiempo polinomial en la longitud de la fórmula. Actualmente sí es más fácil resolver la verificación de modelos que SAT. Todos los algoritmos que conocemos para SAT toman un tiempo exponencial en la longitud de la fórmula en el peor de los casos, que es más ineficiente que los algoritmos de tiempo polinomial. Sin embargo, sorprendentemente nadie ha demostrado que no existan algoritmos polinomiales, es decir, eficientes para resolver SAT. SAT pertenece a una clase importante de problemas llamada problemas NP-completos. Al igual que SAT, nadie a demostrado que no existan algoritmos más eficientes que exponenciales, en el peor de los casos, para resolver estos problemas. Esta es una de las preguntas más importantes sin contestar en la ciencia de la computación. Hay problemas que podemos resolver de manera directa, sin tener que hacer búsqueda, como por ejemplo el problema de ordenamiento de una sucesión de números. Sin embargo, para resolver un problema NP-completo debemos en general hacer búsqueda y es en problemas como estos en los que se concentra la inteligencia artificial. [MÚSICA] [MÚSICA] [MÚSICA]
