Email Gateway (Aug 18 2022 at 16:31): Email Gateway (Aug 18 2022 at 16:31):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Mr. 张,
I usually use "by simp" "by auto" "by arith" in my proof. But I do not know what exactly they mean or what they contains. Can anyone tell me which documents I can read in order to know these? I am now reading Isabelle/HOL a proof assistant for higher order logic and at the same time learn to use Isar.
Some very partial information about the proof methods can be found here:
http://www.cs.miami.edu/~tptp/CASC/J5/SystemDescriptions.html#Isabelle-HOL---2009-2
I hope other readers of the mailing list can complete the information -- e.g., arith is not mentioned.
Regards,
亚斯麦
Email Gateway (Aug 18 2022 at 16:31):From: Sascha Boehme <boehmes@in.tum.de>
Jasmin Blanchette wrote:
The method "arith" is a combination of decision procedures for
arithmetic. In its standard setup, it first tries Fourier-Motzkin
elimination (for naturals, integers, or reals; see [1] for an
overview), and if that fails, it tries a quantifier elimination
procedure for Presburger arithmetic (e.g., see [2]). More decision
procedures may also be added.
Regards,
Sascha
[1] http://en.wikipedia.org/wiki/Fourier-Motzkin_elimination
[2] http://en.wikipedia.org/wiki/Presburger_arithmetic
Last updated: Apr 20 2024 at 08:16 UTC