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