Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- To: Makarius <makarius at sketis.net>, Harry Butterworth <heb1001 at gmail.com>
- Subject: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
- From: Mandy Martin <tesleft at hotmail.com>
- Date: Sun, 12 Apr 2015 04:47:39 +0800
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Importance: Normal
- In-reply-to: <alpine.LNX.firstname.lastname@example.org>
- 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>, <alpine.LNX.email@example.com>
it is difficult to imagine infinite disjunction and conjunction in truth table
1. does it mean that there are infinite disjunction to connect the final result columns of infinite truth tables, infinite conjunction to connect final result columns of infinite truth tables
2. i got a question about subgoal when prove simple logic, because when i prove in Isabelle, the only subgoal it the lemma itself. i would like to know where do subgoals come from.without assumptions, where do subgoals come from?
if below is correct, does it mean that i can pick any one from thousands of logic equations, which means can also build or prove B from A
0 0 00 0 10 <=== deduct to === 1 <===deduct to 11 1 1
when prove 0111 to 0001 , can i say that 0011 is the subgoal ?
but 0011 can be represented by many kinds of logic equations
when consider0 00 10 <=== deduct to === 11 1
does it mean that it do not have any subgoal ?
but if i imagine 0101 between 0001 and 0111, can i say 0101 is its subgoal ?
0 0 00 1 10 <=== deduct to === 0 <==== deduct to === 11 1 1
> Date: Sat, 11 Apr 2015 21:55:28 +0200
> From: makarius at sketis.net
> To: heb1001 at gmail.com
> CC: isabelle-users at cl.cam.ac.uk; tesleft at hotmail.com
> Subject: Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
> 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.
> Exists and All are just infinitary disjunction and conjunction,
> Truth tables are fine as a start, but the real understanding of logic
> works better via pure Natural Deduction. Just expose yourself with the
> relevant introduction and elimination rules of the connectives until they
> become second nature. It also helps to write structured Isar proofs that
> correspond to the standard Natural Deduction rules.
> The Isabelle manuals provide plenty of information on all that -- in fact
> too much information.
> >>> 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?
> Just an arbitrary entry point: "isar-ref" manual section 9.4 on the
> Classical Reasoner. It is both relatively basic and advanced at the same
This archive was generated by a fusion of
Pipermail (Mailman edition) and