*To*: Harry Butterworth <heb1001 at gmail.com>*Subject*: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to*From*: Makarius <makarius at sketis.net>*Date*: Sat, 11 Apr 2015 21:55:28 +0200 (CEST)*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, tesleft at hotmail.com*In-reply-to*: <CAMUwPhxoY2qMpvA4-X6sBDhWvcbW9h=K+mM4w=SXzy+LmeWrhw@mail.gmail.com>*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> <CAMUwPhxoY2qMpvA4-X6sBDhWvcbW9h=K+mM4w=SXzy+LmeWrhw@mail.gmail.com>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Sun, 12 Apr 2015, Harry Butterworth wrote:

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.

2. I want to research the subgoals between A and B when prove A -> Bafter 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 generatesubgoals?Could you recommend a textbook which covers implementation of aninteractive theorem prover?

Makarius

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

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

- Previous by Date: [isabelle] Isabelle2015-RC0 available for testing
- Next by Date: Re: [isabelle] Unknown Isabelle tool: env
- 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