Meta Proof Planning
I have been reflecting quite a while on my proof planning on my human
meta-level, which I have been watching now for many years with the aim to
use it for modeling object-level proof planning.
It could be considered as an AI planning process with some specialties:
It has free existential variables in the theorem.
These variables take care of technical details that cannot be
guessed easily on the high level of abstraction where the theorems
are speculated. Moreover, these variables are there to admit additional
requirements that turn out during the expansion of the plans to calculus
level (my meta-calculus, I mean).
- Then, on a very high level with semantical means I construct a proof
plan. Although it is order independent, it may be a state-space planning
as I do not take care of threats.
Nevertheless, it is not at all clear to me
how this planning process could be automated.
Then, I try to expand the proof plan to calculus level. This is usually
successful (as it changes the theorem via instantiation of meta-variables)
and because I am very experienced on this very high semantical level.
- Then, I start a semantical analysis of the instantiated theorem.
If it is what I want and the additional requirements seem necessary
indeed, I stop. Otherwise I start proof rewriting on the calculus level
(mostly peephole optimization). If this is successful, I repeat step 4.
- Re-planning. Then go on with 3.
This is file p/metaproofplan.html on Claus-Peter Wirth's web site.
Last modified 2004/06/21/21.45.