Kartik Sabharwal (Oct 12 2024 at 02:13): Kartik Sabharwal (Oct 12 2024 at 02:13):Hi Isabelle community,
I'm taking a class on theorem proving in Isabelle.
For the final project, I'd like to experiment with automatic proof search.
Is there any documentation on this?
At the moment I think my best bet would be to look at the Eisbach manual as well as the source code for projects like 'A Proof Strategy Language and Proof Script Generation for Isabelle/HOL' as a starting point, but it'd appeciate any advice/suggestions you can provide.
Thanks.
Mathias Fleury (Oct 12 2024 at 06:06):You need to be more precise on what you want to achieve here. Automatic proof search goes from sledgehammer (offloading to external tools), through try_harder from PSL (combining tactics and internal tools a bit blindly), to writing tactics in Eisbach or ML (so human engineering).
Kartik Sabharwal (Oct 12 2024 at 17:15):What I'd like to try is to take a proof goal (for example inverts_mat m1 m2) and search for theorems in the Matrix module whose conclusion unifies with the goal (this would be inverts_mat_def) and add its premises as subgoals (for inverts_mat_def, the premise would be m1 * m2 = 1_m (dim_row m1)).
Then I would repeat the process asking which theorems in the Matrix module unify with this premise (mat_eq_iff, transpose_mat_eq, and mat_hom_inj), ranking these choices somehow -- maybe even naively, by prompting the user -- and building a proof skeleton.
Is this sufficiently precise?
Kartik Sabharwal (Oct 12 2024 at 17:26):What motivates me to try this is that even though I really appreciate Sledgehammer, I find it a bit tedious to break up proofs to the 'correct' level of granularity for the existing automation to succeed. If I could just tell Isabelle 'please use unification with the theorems in this particular module, build some proof skeletons, then apply sledgehammer to the subgoals on my skeleton of choice' maybe I could save some time.
Mathias Fleury (Oct 12 2024 at 17:31):Yeah that sounds like you want ML
Mathias Fleury (Oct 12 2024 at 17:32):but that sounds a rather simple approach, not sure if this works in practise
Kartik Sabharwal (Oct 12 2024 at 17:41):I absolutely agree that this is a simple approach.
I will be happy if I can understand the automation interface well enough to implement it.
Then I can see how to improve the approach using literature on constructing proofs by backward search.
Kartik Sabharwal (Oct 12 2024 at 17:45):Should I look at the 'Isabelle Cookbook', then?
edit: Isabelle/ML -> Isabelle
Last updated: Dec 21 2024 at 12:33 UTC