Patrick Nicodemus (Mar 14 2023 at 06:28): Patrick Nicodemus (Mar 14 2023 at 06:28):Proof planning is an idea for automated theorem proving that involves working at a higher level of abstraction than tactics. The user defines "methods", where a method has preconditions explaining when it can be called, and guaranteed postconditions. The method then can call a mix of other tactics and methods to accomplish its goal of linking from preconditions to postconditions. Then drawing on existing techniques from planning theory in CS, you search for a chain of methods which proves the theorem.
Methods can be only partially filled in or require search to fill in, so that you can have a high level proof sketch which is repeatedly refined down to a more detailed one until finally you have a complete proof.
This article discusses the idea. https://www.sciencedirect.com/science/article/pii/S0004370299000764?via%3Dihub
This topic seems to have gotten little to no research attention over the past 20 years. Does anybody know why this is? Is it a dead end?
Has anybody ever tried implementing a proof-planning tool for Coq, where the user can write methods? Would this be desirable? (I personally think so.)
Bas Spitters (Mar 14 2023 at 06:49):https://github.com/coq-community/manifesto/issues/57
Bas Spitters (Mar 14 2023 at 06:51):A bit more discussion
https://coq.discourse.group/t/inductive-proof-automation/226
Last updated: Dec 07 2023 at 17:01 UTC