*To*: Mandy Martin <tesleft at hotmail.com>*Subject*: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to*From*: Larry Paulson <lp15 at cam.ac.uk>*Date*: Sat, 11 Apr 2015 17:00:50 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <BAY167-W115A944EF99DD33F513BDB6B6FB0@phx.gbl>*References*: <CAPWZQLq=pbRwXZC0N9h46L7eh=Qqyt2EO6e71v_ecfBcq75RpQ@mail.gmail.com> <, <CAPWZQLqH=SKgFohEqyWt_3uJsC2XK8EjeZ2=B_Hfg=t04C8M0w@mail.gmail.com> <, <3DC7F053-2741-4CCB-92DA-7112B3E192B0@cam.ac.uk>>> <BAY167-W115A944EF99DD33F513BDB6B6FB0@phx.gbl>

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

**Follow-Ups**:**Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to***From:*Harry Butterworth

**References**:**[isabelle] Fwd: [Isabelle] Failed to parse prop***From:*Martin Lee

**Re: [isabelle] Fwd: [Isabelle] Failed to parse prop***From:*Larry Paulson

**[isabelle] How do Isabelle use logic table to prove exist some, all, belong to***From:*Mandy Martin

- Previous by Date: [isabelle] Code generation for certificate-based external/untrusted functions
- Next by Date: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- Previous by Thread: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- Next by Thread: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list