Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to



On Apr 12, 2015 12:01 AM, "Larry Paulson" <lp15 at cam.ac.uk> wrote:
>
> Iâm afraid that your question isnât very clear. You should try to get a
friend to translate for you.

I have attempted a translation inline below.

>
> 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.

I can prove And, Or, Implication by reducing to a truth table.

> >
> > But  can not  search  logic table for exist some, all, belong to,
idempotent relation  these  higher order concepts  in books, wiki  or web.

I can't find truth tables for Exists, All, set membership, other higher
order concepts in books, wikis or through internet search.

> >
> > 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?

Does Isabelle use truth tables for proofs involving these concepts or does
it use programming skill and reduction/simplification?  How does it work?

> >
> > 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?

I want to see all the intermediate steps In a proof.  How does Isabelle
generate the subgoals?

> >          is there  any books teaching  these  algorithms to generate
subgoals?

Could you recommend a textbook which covers implementation of an
interactive theorem prover?

> >
> > Regards,
> >
> > Martin Lee
>



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