Re: [isabelle] Issue with smt and linear arithmetic

Hi Lukas,

linarith works as follows: Based on a decomposition of the original problem into a set of linear inequalities, it tries to find a refutation for them. The trace for the refutation is used to replay the steps, which should yield the Theorem False in the end. Proof replay essentially applies the simplifier with a carefully selected simpset. Whenever the final theorem differs from False, the warning you noticed is shown.

In your particular case, the obvious simplification for â(2x +2y) / 2â is not performed, because some rule or simproc is missing in linarithâs simpset. Extending the simpset appropriately would be a solution. Iâll see what I can do, such that your issue is resolved in the next release of Isabelle.


Von: Lukas Bulwahn

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