[isabelle] How do Isabelle use logic table to prove exist some, all, belong to
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and