Sledgehammer in ZF · Beginner Questions

In "Three Years of Experience with Sledgehammer, a Practical Link
between Automatic and Interactive Theorem Provers" it is mentioned in the end that they plan to make a version of sledgehammer for Isabelle/ZF. I can't find it, but there is so much info about Isabelle, so I might have missed it. Anybody knows?

Mathias Fleury (Jan 07 2022 at 09:31):

Dan Synek (Jan 07 2022 at 10:18):

Thanks! I wonder if it is because of lack of interest or because automatic theorem proving is harder for set theory. Anyway, thanks again for your quick reply!

Mathias Fleury (Jan 07 2022 at 11:16):

maybe @Martin Desharnais knows better, but I believe it is a combination of lack of interest (very few users and Jasmin Blanchette is not one of them) and lack of publicability (publishing sledgehammer papers is very hard nowadays, because it is a very mature -- there are still open problems [e.g., dependent types], but no very interesting ones expected for Isabelle/ZF)

Martin Desharnais (Jan 07 2022 at 14:04):

@Mathias Fleury basically nailed it. On top of that, porting Sledgehammer to another logic would require a lot of non-trivial refactoring for which we are missing the contributor resources.

Dan Synek (Jan 07 2022 at 15:19):

What a good group. Thanks for the explanation. I suppose all the work on transforming higher order to first order which had to be done for HOL would be wasted on Isabelle/ZF since it is already first order. And I think I read somewhere in the TPTP documentation that set theory is known to be hard for automatic theorem provers - on the hand, if I remember correctly many of the Mizar theorems can now be proved automatically, so perhaps that has changed. Anyway, thanks again!

Lekhani Ray (Jan 11 2022 at 21:10):

Hello! I am currently working with functions and I have a problem with their termination. With my current code Isabelle seems to be unable to identify that the function is over and I am a little confused with the section.
code looks like this and it says failed to finish subgoal.
theory th1_th8_new
imports Main
begin

fun len :: "BinNum ⇒ nat"
where
"len Zero = 1"|
"len One = 1"|
"len (JoinZero x) = len x + 1"|
"len (JoinOne x) = len x + 1"

function addBinNum :: "BinNum ⇒ BinNum ⇒ BinNum"
where
"addBinNum Zero x = x"|
"addBinNum x Zero = x"|
"addBinNum One One = JoinZero One"|
"addBinNum One (JoinZero x) = JoinOne x"|
"addBinNum One (JoinOne x) = JoinZero(addBinNum One x)"|
"addBinNum(JoinZero x) One = JoinOne x"|
"addBinNum(JoinOne x) One = JoinZero(addBinNum One x)"|
"addBinNum(JoinZero x) (JoinZero y) = JoinZero(addBinNum x y)"|
"addBinNum(JoinZero x) (JoinOne y) = JoinOne(addBinNum x y)"|
"addBinNum(JoinOne x) (JoinZero y) = JoinOne(addBinNum x y)"|
"addBinNum(JoinOne x) (JoinOne y) = JoinZero(addBinNum(addBinNum x y) One)"
by pat_completeness auto

Simon Roßkopf (Jan 11 2022 at 22:58):

Your termination proof does not complete and Isabelle tells you where it gets stuck:

Failed to finish proof⌂:
goal (1 subgoal):
 1. ⋀x y. addBinNum_dom (x, y) ⟹ len (addBinNum x y) < Suc (len x + len y)

As the value of addBinNum x y depends on what x and yare, an induction proof might help. In fact this works as a termination proof:

apply (relation "measure (λ(x,y). len x + len y)")
apply auto
subgoal for x y by (induction x y rule: addBinNum.pinduct) (auto simp add: addBinNum.psimps)
done

As there is no termination proof done yet, this uses the partial versions of the induction and simplification rules.
You can also proof termination by just applying the size_change method

Stream: Beginner Questions

Topic: Sledgehammer in ZF