Как раскрыть импликацию в алгебре логики? Выражение вида X -> Y

По условию задачи нужно упрощением выражения решать. К примеру X ~ Y = (X ^ Y) v ((not ^ (not Y)). Есть ли похожий способ раскрытия импликации?