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



Hi Makarius,
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

Regards,
Martin  Lee


> 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, 
> respectively.
> 
> 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 
> time.
> 
> 
>  	Makarius
> 
> 
 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.