Stream: Miscellaneous

Topic: Proof Planning

view this post on Zulip 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.

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

view this post on Zulip Bas Spitters (Mar 14 2023 at 06:49):

view this post on Zulip Bas Spitters (Mar 14 2023 at 06:51):

A bit more discussion

Last updated: Jun 05 2023 at 10:01 UTC