Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How do Isabelle use logic table to prove exis...

view this post on Zulip Email Gateway (Aug 22 2022 at 09:39):

From: Mandy Martin <tesleft@hotmail.com>
Hi Larry,
i use logic table that can prove And , Or, Implication quickly by from more one to less one.
But can not search logic table for exist some, all, belong to, idempotent relation these higher order concepts in books, wiki or web.

  1. how do Isabelle do with these concept to prove with logic table? or solved by programming skill together with more one to less one? how do it do?
  2. I want to research the subgoals between A and B when prove A -> B after quick decide that it is true with table method, what is the name of algorithms used in Isabelle to generate subgoals? is there any books teaching these algorithms to generate subgoals?
    Regards,
    Martin Lee

Last updated: Nov 21 2024 at 12:39 UTC