Re: [isabelle] Linear Arithmetic Split Limit Exceeded



Thanks Tjark! With n = 12 there´s no need to use (arith)+ after the
existential proofs.

Best!

On Thu, Feb 7, 2013 at 12:30 PM, Tjark Weber <webertj at in.tum.de> wrote:

> On Thu, 2013-02-07 at 14:31 +0100, Makarius wrote:
> > Someone else who understands the "lin_arith" solver needs to explain how
> > to switch it off, or how to do these proofs about "mod" in a better way.
>
> The limit exists because repeated splitting leads to an exponential
> blow-up of the goal. It can be set, e.g., via
>
>   using [[linarith_split_limit=n]]
>
> For this particular proof, n=12 gets rid of the warnings, and also of a
> few more subgoals.
>
> Best regards,
> Tjark
>
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.