I'm looking for a software which can prove a tautology using logical equivalences.
Ideally, it can show each step. One step would be, for example, to use absorption, distributivity and the like.
Here is an example: \begin{align} (p\to q)\to(\neg q\to\neg p)&\equiv\neg(\neg p\lor q)\lor(q\lor\neg p)\tag{material implication}\\[1em] &\equiv\neg(\neg p\lor q)\lor(\neg p\lor q)\tag{commutativity}\\[1em] &\equiv \neg M\lor M\tag{$M:\neg p\lor q$}\\[1em] &\equiv \mathbf{T}.\tag{negation law} \end{align}