*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to*From*: Harry Butterworth <heb1001 at gmail.com>*Date*: Sun, 12 Apr 2015 00:46:29 +0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, tesleft at hotmail.com*In-reply-to*: <52F398EA-D07E-4B60-A23A-1FE0E96E2266@cam.ac.uk>*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> <52F398EA-D07E-4B60-A23A-1FE0E96E2266@cam.ac.uk>

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 >

**Follow-Ups**:

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

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

- Previous by Date: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- Next by Date: [isabelle] Isabelle2015-RC0 available for testing
- Previous by Thread: Re: [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