Saber si una fórmula (µ) es satisfacible o no

Tabla de verdad
1. El número de la tabla crece exponencialmente según el numero de variables.
2. 1.Según el número de variables, se enlistan todas las combinaciones posibles de valores de verdad.
  1. 2.Dichas combinaciones se evalúan en la fórmula.
    1. 3.Cada fila de la tabla escupe que valor de verdad que toma la fórmula según el estado de las variables.
      1. Sí todas las casillas que correspondientes a la formula están evaluadas a verdadero.
        Si todas se evalúan a falso.
        Otro caso.
        Es satisfacible, pues sabemos que existe aunque sea un modelo.
        Es contradicción y no es satisfacible.
        Es una tautología y la fórmula es satisfacible.
Tableau
1. Negamos la fórmula
  1. Eliminamos equivalencias e implicaciones
2. Se construye en forma de árbol.
3. Si tenemos una conjunción el árbol crece 2 ramas hacia abajo.
4. Si tenemos una disyunción se desglosa en 2 ramas.
5. Buscamos cerrar ramas encontrando contradicciones.
6. Si logramos cerrar todas las ramas o algunas, µ es satisfacible.
7. En otro caso no lo es.
Resolución binaria
1. Se lleva a µ a su forma normal conjuntiva
  1. Una vez hecho esto se enlistan las cláusulas
    1. Y usando la reducción Binaria de Robinson se busca llegar a tener una literal y su complemento.
      1. Si esto ocurre, la cláusula vacía nos dice que µ es insatisfacible.
        Si no se puede llegar a la cláusula vacía µ es satisfacible.
        Puede usarse refutación
Interpretaciones
1. Se propone que el valor de verdad de la fórmula es verdadero.
2. Se busca encontrar una combinación de valores de verdad en las variables.
3. Tal que dicha combinación sea un modelo en µ
4. Si es posible dar con el modelo, entonces µ es satisfacible, en otro caso es una contradicción.
Equivalencias
1. Dadas ciertas reglas descomponemos una formula a expresiones más sencillas
2. buscamos hacer la fórmula lo mas pequeña posible
3. logrado eso, si tenemos T ó una fórmula es satisfacible
4. Si llegamos a una contradicción no es satisfacible.

Próximo

Saber si una fórmula (µ) es satisfacible o no

Descrição

Resumo de Recurso

Semelhante

	Criado por belyy volk quase 7 anos atrás