Matematické Fórum

Ahoj,

procházel jsem skripta Úvod do matematické logiky a nepochopil jsem důkaz věty o rezoluci (str. 23).

Věta říká, že konečná množina klauzulí [mathjax]T[/mathjax] je splnitelná právě tehdy, když její rezoluční obal [mathjax]\mathcal{R}(T)[/mathjax] neobsahuje kontradikci. V důkazu se konstruuje pravdivostní ohodnocení [mathjax]v[/mathjax] výrokových proměnných [mathjax]A_1, \ldots , A_k[/mathjax], které [mathjax]\mathcal{R}(T)[/mathjax] splňuje, stylem: pokud nějaká klauzule z [mathjax]\mathcal{R}(T)[/mathjax] sestává výhradně z [mathjax]\neg A_j[/mathjax] a z literálů ohodnocených opačně než při dosavadním ohodnocení, nechť [mathjax]v(A_j) = 0[/mathjax]. Nerozumím této formulaci.

Co je přesně myšleno literály ohodnocenými opačně než při dosavadním ohodnocení? Literály, které jsou negacemi už ohodnocených proměnných?

Děkuji za odpověď.

Placka03