Liketilfredsstillelse

I logikk er to formler liketilfredsstillende hvis den første formelen er tilfredsstillende så lenge den andre formelen også er tilfredsstillende, og omvendt. Med andre ord: enten er de to formlene tilfredsstillende eller heller ikke. To likeverdige formler kan ha forskjellige modeller , siden ingen av dem eller begge har en viss stil. Som et resultat har vi at liketilfredsstillelse er forskjellig fra logisk ekvivalens fordi to logisk ekvivalente formler alltid har de samme modellene.

Generelt brukes begrepet equisatisfiability i konverteringen av formler, det vil si at det kan bekreftes at en konvertering er korrekt hvis den opprinnelige formelen og den resulterende er ekquisatisfiable. Eksempler på konverteringer som involverer dette konseptet er skolemisering og noen transformasjoner for å nå konjunktiv normalform .

Eksempler

En konvertering fra proposisjonell logikk til proposisjonell logikk der hver binær disjunksjon er erstattet med , hvor er en ny variabel (en for hver substituert disjunksjon) er en tilfredsstillelsesbevarende transformasjon, det vil si at den opprinnelige formelen og resultatet er ekvisatisfiable. Merk at disse to formlene ikke er ekvivalente: den første formelen har modellen som er sann, mens og er usann, og dette er ikke en modell av den andre formelen, der , i dette tilfellet, må være sann