Email Gateway (Aug 18 2022 at 09:53): Email Gateway (Aug 18 2022 at 09:53):From: kuecuek@rbg.informatik.tu-darmstadt.de
Hallo
i try to solve an equation in isabelle in which i use 6 parameter. But
isabelle can not solve this problem with auto.
is there any other method for solving problems automatically (i have tried
simp and arith too. )
the important things in the equation are :
(((y1-y2)^nat (p - 3)) - x1 ) ^3 = .....
i think the use of nat and power may be a problem against the auto.
can anybody recommend something?
thanks
Email Gateway (Aug 18 2022 at 09:54):From: Amine Chaieb <chaieb@informatik.tu-muenchen.de>
Kuecuek,
There is a new mthod (not yet included in the repository) to solve similar
problems based on Groebner bases. Yet I do'nt think that it would work for
these instances. The key questions are:
a) is nat a variable?
b) can you get rid of substraction (-) in your context
If the answer to both is yes, then the method would work for you.
Unfortunately It might take time to include it.
Otherwise try stuff like ring_eq_simps and add appropriate theorems for
power.
Aemin.
Last updated: May 03 2024 at 04:19 UTC