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.