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

Larry Paulson


> 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?
> 
> Regards,
> 
> Martin Lee




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.