Patrick Nicodemus (Mar 20 2023 at 02:16): Patrick Nicodemus (Mar 20 2023 at 02:16):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.
Patrick Nicodemus (Mar 20 2023 at 02:17):A previous paper from the same research group also looks really fascinating. https://arxiv.org/abs/2006.08381
Patrick Nicodemus (Mar 20 2023 at 02:19):Refactoring the code base in a principled way to expose the most important abstractions underlying the library could make theorem proving much easier.
Patrick Nicodemus (Mar 20 2023 at 02:22):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 13 2024 at 01:02 UTC