For classical propositional logic (and many other logics but I will stick to this for simplicity), this process can be done completely algorithmically/mechanically. One method for checking whether two things are equivalent in some sense is to find a notion of "canonical form" and a function that takes an arbitrary expression to its canonical form, usually operationalized as a collection of rewrite rules. A function $N$ is a normalization function for an equivalence relation $\sim$ iff for any arbitrary expression $t$, we have $N(N(t)) = N(t)$, and for arbitrary expressions $t_1$ and $t_2$, $N(t_1) = N(t_2) \iff t_1\sim t_2$.
In this case, the equivalence relation is logical equivalence. The normalization function can be taken as the mapping of a logical expression to full conjunctive (or disjunctive) normal form, Full (C/D)NF. We can take the logical equivalences you start with and orient them to produce a system of rewrite rules to produce CNF. For example, we can take the equivalence $\neg\neg P \equiv P$ and make it the rewrite rule, $\neg\neg P \leadsto P$. Wikipedia describes a conversion into CNF here (ignore the aspects involving quantifiers). For simplicity it omits uses of associativity and commutativity as will I. These are tedious but mechanical. Full CNF means each atomic proposition occurs exactly once in each conjunct. This means we need to additionally apply the equivalences $P\lor P \equiv P$, $P\lor\neg P \equiv \top$, $P\lor \top \equiv \top$, and potentially $\top\land P\equiv P$. If $P$ is an atomic proposition which occurs zero times in a conjunct, then add $P\land\neg P$ to that conjunct, i.e. use the equivalences $Q\equiv Q\lor\bot$ and $\bot\equiv P\land\neg P$, and then distribute to return to CNF. Once Full CNF is reached for each initial expression, they will be equal modulo the order of the conjuncts and disjuncts and the association if and only if they are logically equivalent. We can normalize further by right associating everything as much as possible, sorting the disjuncts of each conjunct via some arbitrary order on literals (i.e. atomic propositions or their negations), then sorting the conjuncts by the induced lexicographical order viewing the conjunct as a tuple of literals (we can remove duplicate conjuncts at this point as well as an instance of $P\land P\equiv P$). Now two expressions are logically equivalent if and only if these two normalized Full CNF expressions are syntactically equal.
It is not too hard to formalize this as a computer program, even a program that outputs a sequence of logical equivalences and where to apply them. This approach is not very human friendly, especially if you must spell out every single logical equivalence and even more especially if you need to explicitly commute and reassociate. CNF, let alone Full CNF, can also be exponentially larger than the original expression and so may be completely infeasible to produce. This is likely unavoidable in general in some sense. On the one hand, many exercise problems are likely to have much simpler proofs. On the other hand, many exercise problems involve relatively few atomic propositions, so an exponential increase is quite manageable.
The benefit of this approach is that it is systematic, and it will always succeed. This is important because if two expressions aren't logically equivalent, randomly applying logical equivalences may never convince you. Meanwhile, if two expressions have distinct Full CNFs, then they are not logically equivalent. In practice, in a translation by hand to Full CNF, you will not slavishly follow the process I've sketched above. Instead, you may perform some preliminary simplifications that stick out, particularly ones that decrease the number of atomic propositions. Then, as you perform the algorithm, you will opportunistically simplify when you can. It's easy to see, for example, that $P$ and $\neg P$ occurs in a conjunct in which case that whole conjunct can be dropped immediately. Similarly, duplicate atomic propositions in a conjunct can be quickly eliminated.
In your example, the Full CNF we get is: $(p\lor \neg q)\land(p\lor q)$. On the left hand side, we get this in by applying deMorgan on the left conjunct and then a double negation elimination. On the right hand side, we have a conjunct with zero occurrences of $q$, so we rewrite to $p\lor(\neg q\land q)$ and distribute. In this case, the systematic approach exactly corresponds to starting at the beginning and end of your proof and having them meet in the middle.
Your problem can be solved very easily using the Consensus Theorem, which states that:
$(X \lor Y) \land (\neg Y \lor Z) \land (X \lor Z) \Leftrightarrow (X \lor Y) \land (\neg Y \lor Z)$
(this law is most easily remembered by going from right to left: with the $(X \lor Y)$ term containing a $Y$, and the $(\neg Y \lor Z)$ term containing a $\neg Y$, you can put together the other parts ($X$ and $Z$) into a new term $(X \lor Z)$ and just add that as a third term.
So with that:
$$(A\land\lnot B)\lor(B\land\lnot C)$$
$$\overset{Distribution}{\Leftrightarrow}$$
$$(A\lor B)\land(A\lor\lnot C)\land(\lnot B\lor B)\land(\lnot B\lor\lnot C)$$
$$\overset{Tautology}{\Leftrightarrow}$$
$$(A\lor B)\land(A\lor\lnot C)\land(\lnot B\lor\lnot C)$$
$$\overset{Consensus}{\Leftrightarrow}$$
$$(A\lor B)\land(\lnot B\lor\lnot C)$$
$$\overset{DeMorgan}{\Leftrightarrow}$$
$$(A\lor B)\land \lnot (B\land C)$$
If you are not allowed to use Consensus in one step, please know that it is easily derived as follows:
$$(X \lor Y) \land (\neg Y \lor Z) \land (X \lor Z)$$
$$\overset{Adjacency}{\Leftrightarrow}$$
$$(X \lor Y) \land (\neg Y \lor Z) \land (X \lor Z \lor Y) \land (X \lor Z \lor \neg Y)$$
$$\overset{Absorption \ x \ 2}{\Leftrightarrow}$$
$$(X \lor Y) \land (\neg Y \lor Z)$$
Best Answer
Since $A \leftrightarrow B$ is logically equivalent to $(\lnot A \lor B) \land (\lnot B \lor A)$, we have: \begin{align} \lnot (a \land \lnot b) \leftrightarrow c &\equiv ( \lnot \lnot (a \land \lnot b) \lor c) \land (\lnot c \lor \lnot (a \land \lnot b)) \\ &\equiv ((a \land \lnot b) \lor c) \land (\lnot c \lor \lnot (a \land \lnot b)) \\ &\equiv ((a \land \lnot b) \lor c) \land \lnot (c \land a \land \lnot b) \\ &\equiv ((a \lor c) \land (\lnot b \lor c)) \land \lnot (c \land a \land \lnot b) \\ &\equiv (\lnot (\lnot a \land \lnot c) \land \lnot (\lnot \lnot b \land \lnot c)) \land \lnot (c \land a \land \lnot b) \\ &\equiv (\lnot (\lnot a \land \lnot c) \land \lnot (b \land \lnot c)) \land \lnot (c \land a \land \lnot b) \\ \end{align}