Equisatisfabilidad


En la lógica matemática (un subtema dentro del campo de la lógica formal ), dos fórmulas son equisatisfables si la primera fórmula es satisfactoria siempre que la segunda lo sea y viceversa; en otras palabras, ambas fórmulas son satisfactorias o ambas no. [1] Sin embargo, las fórmulas que se pueden igualar pueden no estar de acuerdo para una elección particular de variables. Como resultado, la equisatisfacción es diferente de la equivalencia lógica , ya que dos fórmulas equivalentes siempre tienen los mismos modelos. Mientras que dentro de las fórmulas equisatisfables, sólo se valora la proposición primitiva que impone la fórmula.

La equisatisfabilidad se utiliza generalmente en el contexto de la traducción de fórmulas, de modo que se puede definir que una traducción es correcta si las fórmulas original y resultante son equisatisfactorias. Ejemplos de traducciones que involucran este concepto son Skolemization y algunas traducciones en forma normal conjuntiva .

Una traducción de la lógica proposicional a la lógica proposicional en la que cada disyunción binaria es reemplazada por , donde hay una nueva variable (una para cada disyunción reemplazada) es una transformación en la que se conserva la satisfacibilidad: las fórmulas original y resultante son equisatisfables. Tenga en cuenta que estas dos fórmulas no son equivalentes: la primera fórmula tiene el modelo en el que es verdadero mientras y son falsos (el valor de verdad del modelo por ser irrelevante para el valor de verdad de la fórmula), pero este no es un modelo de la segunda fórmula , en lo que tiene que ser cierto en este caso.