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

https://github.com/coq-community/manifesto/issues/57

A bit more discussion

https://coq.discourse.group/t/inductive-proof-automation/226

Last updated: Jul 23 2024 at 17:01 UTC