Solving Subproblem in Logic (first-order, propositional, pddl)

One sentence question

Is there any algorithm able to prove (solve) a logic problem (first-order, propositional, pddl) by finite induction?

Background

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:

on(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)?

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".

• Very good answer and very helpful. – rdllopes Jul 25 '16 at 14:23

I didn't solve yet but I found important insights and pitfalls.

Mathematical induction is the Mathematical reasoning that allows generalization the one proposition over a whole well-ordered set following:

1. the proposition should applies over a base element, and
2. if the proposition applies over any element of the set then it should implies that to next element;

Mathematical induction is an Axiom of second-order logic. Therefore, it could not be apply directly in first-order logic. A possible solution is identify well-ordered sets over the belief base.