diff --git a/equivalence_checking/0008_sol.tex b/equivalence_checking/0008_sol.tex index be827f9..588d39b 100644 --- a/equivalence_checking/0008_sol.tex +++ b/equivalence_checking/0008_sol.tex @@ -18,7 +18,7 @@ $$ \begin{align*} \varphi' = \ &x_\phi \land \\ - &\tseitinAnd{x_\varphi}{x_1}{x_2} \land \\ + &\tseitinOr{x_\varphi}{x_1}{x_2} \land \\ &\tseitinNot{x_1}{x_3} \land \\ &\tseitinOr{x_3}{a}{x_4} \land \\ &\tseitinAnd{x_2}{x_5}{c} \land \\ diff --git a/util/chapter.tex b/util/chapter.tex index 4fa482d..859546e 100644 --- a/util/chapter.tex +++ b/util/chapter.tex @@ -2,10 +2,10 @@ %\chapterproplogictrue %\chaptersatsolvertrue %\chapterndproptrue -\chapterpredlogictrue +%\chapterpredlogictrue %\chapterndpredtrue %\chaptersmttrue %\chapterbddtrue -%\chaptereqcheckingtrue +\chaptereqcheckingtrue %\chaptersymbenctrue %\chaptertemporaltrue