*To*: Larry Paulson <lp15 at cam.ac.uk>*Subject*: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to*From*: Mandy Martin <tesleft at hotmail.com>*Date*: Fri, 10 Apr 2015 04:31:11 +0800*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Importance*: Normal*In-reply-to*: <3DC7F053-2741-4CCB-92DA-7112B3E192B0@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>

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

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

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

- Previous by Date: Re: [isabelle] using Isabelle programmatically
- Next by Date: Re: [isabelle] Fwd: [Isabelle] Failed to parse prop
- Previous by Thread: Re: [isabelle] Fwd: [Isabelle] Failed to parse prop
- 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