Re: [isabelle] How do Isabelle use logic table to prove exist some, all, belong to
On Apr 12, 2015 12:01 AM, "Larry Paulson" <lp15 at cam.ac.uk> wrote:
> Iâm afraid that your question isnât very clear. You should try to get a
friend to translate for you.
I have attempted a translation inline below.
> Meanwhile I suggest that you read some documentation, starting with the
first item at http://isabelle.in.tum.de/documentation.html <
> And study the examples. For logic, see src/HOL/ex/Classical.thy
> Larry Paulson
> > On 9 Apr 2015, at 21:31, Mandy Martin <tesleft at hotmail.com> wrote:
> > Hi Larry,
> > i use logic table that can prove And , Or, Implication quickly by
from more one to less one.
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.
> > 1. how do Isabelle do with these concept to prove with logic
table? or solved by programming skill together with more one to less
one? how do it do?
Does Isabelle use truth tables for proofs involving these concepts or does
it use programming skill and reduction/simplification? How does it work?
> > 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?
> > Regards,
> > Martin Lee
This archive was generated by a fusion of
Pipermail (Mailman edition) and