One sentence question
Is there any algorithm able to prove (solve) a logic problem (first-order, propositional, pddl) by finite induction?
I am researching Hierarchical planning solvers and I found the following problem. Let a problem climb a stairway. An agent is able to move up or down. For example, suppose the following "move up" action:
moveup(position): pre-condition: on(position) post-condition: ~on(position) ^ on(next(position)
Now, let a stairway be defined as:
stairway: next(first_step) = second_step next(second_step) = third_step ... next(nminusoneth_step) = nth_step
and, a start point from agent is on the first step:
Now, I want to create a plan to bring the agent from the first step to last one. Of course, I can solve that in many different ways (brute force for example), but I know how to climb an one-step stairway (just move up) so, I am able to infer that all I need to climb an n-step stairway is just moving up (it is not necessary to decide each action individually). Is there already any algorithm for that (recognize a subproblem structure and infer actions by induction)?