Top-Down-Synthesis-for-Library-Matthew-Bowers.pdf

I came across this paper recently and thought it might be interesting to some users here.

In particular I was thinking that it could be interesting to try and refactor a Coq codebase with the approach laid out in this paper. You could go through the Gallina terms and apply these methods and if the approach was successful you might end up with new theorems that generalize existing ones or enabler simpler, shorter proofs.

A previous paper from the same research group also looks really fascinating. https://arxiv.org/abs/2006.08381

Refactoring the code base in a principled way to expose the most important abstractions underlying the library could make theorem proving much easier.

I think there are a lot of papers highly relevant to automated theorem proving i've been missing because they are published under the subject heading "program synthesis". The second paper, DreamCoder, seems like it's potentially very relevant to automated theorem proving by helping a prover keep a reasonably concise list of key theorems it needs to solve the goals.

Last updated: Oct 04 2023 at 19:01 UTC