Здравствуйте, я натолкнулся на одну проблему при доказательстве формулы резолюцией:
как привести даное выражение к виду КНФ:
(|A^C) &B&|C^(|B^C)&A&|C
|-отрицание,
вроде бы по закону дистрибутивности действовать надо, но когда начинаю выходит что-то не то...
Распишите пожалуйста поподробнее, если сможете решить пример...

Если & - конъюнкция, а ^ дизъюнкция, тогда
(|A^C)&B&|C^(|B^C)&A&|C =
((|C&|A)^(|C&C))&B^((|C&|B)^(|C&C)) &A =
|C&|A&B^|C&|B&A =
|C&(|A&B^|B&A) =
|C&(A^B)&(|A^|B)