Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] which directory include geometry prove logic

view this post on Zulip Email Gateway (Aug 22 2022 at 10:04):

From: Mandy Martin <tesleft@hotmail.com>
Hi sir,

  1. i find this site mention this, but do not find in afp and directory Isabelle2014\src\HOL, where is it?http://web.stanford.edu/~danlass/esslli2011stus/petrovic.pdf
  2. what is the logic principle or representation of elimination for proving geometry in numeric and variable case and in only variable case?
  3. besides elimination method, is there any other method exist in the world?
    as i think descriptive geometry prove need expert in geometry, i feel difficult and do not know how to generate geometry proof from combinations.
    Regards,
    Martin Lee

Last updated: Apr 23 2024 at 16:19 UTC