Solving Subproblem in Logic (first-order, propositional, pddl)
In general, using mathematical induction to prove theorems automatically is quite difficult. First, note that this isn't really a problem of first-order vs second-order logic, since induction can easily be expressed as a schema in FOL, and generally be reduced to a finite set of axioms. It's more useful though to keep it as a schema, and add induction as a logical rule rather than a list of axioms.

This has been studied quite a bit, but success of general purpose automatic theorem provers is somewhat limitied in the presence of induction, for the following reasons:


(Of course) the first order (quantifier free) theory with induction is undecidable. A good milestone of how undecidable a theory is is to measure how expressive the resulting theory is, and the theory with induction is essentially capable of expressing a large part of elementary mathematics quite easily. This is a pretty bad sign.
Induction is always applicable: any goal which contains some occurrence of an inductive data type (like a list or a natural number) may be proven (indeed, may need to be proven) by induction. Clearly there needs to be a clever heuristic to decide when to apply induction. The general rule is: do everything but induction, and apply induction as an absolute last resort! Even with this heuristic, you need to know when to give up, which is again undecidable, but necessary if any kind of backtracking is to be performed.
Sometimes the goal needs to be generalized. This is a distinctive phenomenon of induction, that sometimes the induction hypothesis is too weak to prove the conclusion, and as a result the whole goal needs to be strengthened, which is rather counter-intuitive (failure to prove a goal results in trying to prove a stronger one!). Finding and proving these strengthenings automatically is the subject of exciting current research in computer science (in the field of loop invariant synthesis). 


Given all these difficulties, it's clear there's no general purpose algorithm for proving theorems by induction in full generality. However the problem itself is being actively studied, and I'll just leave you with this link to a workshop specifically addressing this problem.



As a footnote, your problem doesn't seem to be solvable with much else than standard "brute force" (or resolution), since the algorithm needs to verify that the last step is reachable by explicitly going through all the steps. Unless you have further knowledge (e.g. each step corresponds to a natural number), you need to verify that each step can be taken, and that there are no "breaks".