Ищу любые материалы на тему: "доказать секвенцию исчисления высказываний постоением доказательства в виде дерева".

желательно алгоритмы решений и примеры.
Спасибо