Gergely Buday (Aug 18 2023 at 10:05): Gergely Buday (Aug 18 2023 at 10:05):I have an algebraic theory where Vampire proved a non-trivial equation by metis and a few lemmas.
I would be interested in a calculational proof that bridges the gap but in spite of setting Sledgehammer to create an Isar proof, it says only by metis.
Is there any tool or manual method that would help me finding a step-by-step proof of the theorem?
Lukas Stevens (Aug 18 2023 at 10:14):I would describe the isar proof search by sledgehammer as an experimental tool. It only succeeds in some cases. I think there is no automated way to convert a metis proof into a more human-readable one. I would suggest that you look at the theorems that metis uses and think about how they are used in your proof. Often enough, you can turn a proof by metis into a proof by auto by instantiating the theorems that metis uses in the appropiate way and passing the theorems as intro, elim, dest, simp parameters.
Lukas Stevens (Aug 18 2023 at 10:15):Even if that does not finish the proof, the resulting proof state might give you an idea about the nature of the subgoals that you need to prove.
Wolfgang Jeltsch (Aug 18 2023 at 11:16):Often enough, you can turn a proof by metis into a proof by auto by instantiating the theorems that metis uses in the appropiate way and passing the theorems as intro, elim, dest, simp parameters.
And often you can even drop many or all of those rules, because many such rules have been already registered to be taken into account automatically, which basic provers like auto do, as opposed to metis and smt, which only seem to consider a fixed set of basic logical rules.
Mathias Fleury (Aug 18 2023 at 18:47):You are not the first to ask for such a tool and it is somewhere in the sledgehammer todo list, but nothing has happened so far
Last updated: Apr 27 2024 at 20:14 UTC