Email Gateway (Aug 23 2022 at 09:02): Email Gateway (Aug 23 2022 at 09:02):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Hello,
In my formalisation I'm using various very simple algebraic calculations
as I do everything step by step
( adding up factors, expanding/ getting rid of - outside parentheses,
showing equality of algebraic expressions etc etc.. )that I
would expect would be solved by linarith or simp or auto.
Very often, when I call Sledgehammer or try0 I keep getting
"Proof found"
and then repeatedly the message :
"
linarith_split_limit_exceeded (current value is 9)"
I can see this issue has been discussed before but I'm not sure how I
could get rid of this problem.
Is there some setting/ macro/plugin I could change perhaps?
Many thanks in advance,
Angeliki
Email Gateway (Aug 23 2022 at 09:02):From: Lawrence Paulson <lp15@cam.ac.uk>
Hi Angeliki, you have a number of options for modifying this limit:
At the top level of a theory file:
declare [[linarith_split_limit = 15]]
At the top level of a proof:
note [[linarith_split_limit = 15]]
Before an individual proof step:
using [[linarith_split_limit = 15]]
What I don’t know was how high you can take this limit before things fall apart.
Larry
Email Gateway (Aug 23 2022 at 09:02):From: Manuel Eberl <eberlm@in.tum.de>
I just wanted to add that just you see that message doesn't mean this is
actually the reason why your theorem wasn't proven. In my experience,
increasing that limit when you get that message very rarely leads to a
successful proof.
Manuel
Email Gateway (Aug 23 2022 at 09:02):From: Peter Lammich <lammich@in.tum.de>
Hi,
I sometimes run into this problem too, and I would wish I could disable
the splitter altogether, instead of increasing its limit.
Unfortunately, this seems not to be possible (?).
Last updated: Apr 26 2024 at 20:16 UTC