Vervulbaarheidsequivalentie

In de klassieke logica zijn twee proposities vervulbaarheidsequivalent als er voor beide wel (of niet) een toekenning van waar of onwaar aan de atomaire formules bestaat waardoor de proposities waar zijn (dit wordt ook wel het vervullen van een formule of propositie genoemd). Anders geformuleerd houdt het in dat als de ene formule vervulbaar is (of niet) dan is de andere dat ook (niet) en andersom. Vervulbaarheidsequivalentie wordt soms genoteerd als ≡_sat waarbij sat verwijst naar het Engelse woord voor vervulbaarheid: satisfiability.

Verschil met logische equivalentie

Een verschil met logische equivalentie is dat het bij twee vervulbaarheidsequivalente formules wel mogelijk kan zijn om de ene formule te vervullen terwijl de andere met dezelfde toekenning niet vervuld wordt. Bij logische equivalentie geeft elke toekenning van waar of onwaar aan de atomaire formules dezelfde waarheidswaarde voor beide proposities. Logische equivalentie is in dat opzicht strikter dan vervulbaarheidsequivalentie.

Voorbeeld

De formules $P\land (\neg P\lor A)$ en $A$ zijn niet logisch equivalent, want voor $A=\mathrm {waar}$ en $P=\mathrm {onwaar}$ is $A$ waar, terwijl :$P\land (\neg P\lor A)$ onwaar is. Dit is te zien in de waarheidstabel (T = waar (true) en F = onwaar (false)):

$P$	$A$	$\neg P$	$\neg P\lor A$	$P\land (\neg P\lor A)$
T	T	F	T	T
T	F	F	F	F
F	T	T	T	F
F	F	T	T	F

Ze zijn wel vervulbaarheidsequivalent:

$P\land (\neg P\lor A)\equiv _{sat}A$,

want er bestaat een toekenning die beide formules waar maakt, namelijk $A=\mathrm {waar}$ en $P=\mathrm {waar}$. Dit is te zien in de bovenste rij van de waarheidstabel.

Gebruik

Vervulbaarheidsequivalentie wordt bijvoorbeeld gebruikt in automatische stellingbewijzers om aan te tonen dat een propositie onvervulbaar is. De algoritmen herschrijven proposities naar vervulbaarheidsequivalente proposities en deze hoeven niet logisch equivalent te zijn aangezien dit niet vereist is voor hetgeen men wil aantonen. Een voorbeeld hiervan is de Tseitin-transformatie. Ook bij het vereenvoudigen van een propositie kan men de eis van logische equivalentie laten vallen in ruil voor vervulbaarheidsequivalentie, zoals bij monotone variable fixing en de one-literal rule.