Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
Iâm afraid that your question isnât very clear. You should try to get a friend to translate for you.
Meanwhile I suggest that you read some documentation, starting with the first item at http://isabelle.in.tum.de/documentation.html <http://isabelle.in.tum.de/documentation.html>
And study the examples. For logic, see src/HOL/ex/Classical.thy
> On 9 Apr 2015, at 21:31, Mandy Martin <tesleft at hotmail.com> wrote:
> 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?
> Martin Lee
This archive was generated by a fusion of
Pipermail (Mailman edition) and