Email Gateway (Aug 22 2022 at 09:40): Email Gateway (Aug 22 2022 at 09:40):From: Larry Paulson <lp15@cam.ac.uk>
I’m afraid that your question isn’t very clear. You should try to get a friend to translate for you.
Meanwhile I suggest that you read some documentation, starting with the first item at http://isabelle.in.tum.de/documentation.html <http://isabelle.in.tum.de/documentation.html>
And study the examples. For logic, see src/HOL/ex/Classical.thy
Larry Paulson
Email Gateway (Aug 22 2022 at 09:40):From: Harry Butterworth <heb1001@gmail.com>
On Apr 12, 2015 12:01 AM, "Larry Paulson" <lp15@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 <
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@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.
- 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?
- 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?
Regards,
Martin Lee
Email Gateway (Aug 22 2022 at 09:40):From: Makarius <makarius@sketis.net>
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.
- 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
Email Gateway (Aug 22 2022 at 09:41):From: Makarius <makarius@sketis.net>
On Sun, 12 Apr 2015, Mandy Martin wrote:
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
Yes. A table can be easily infinite, you just draw "..." on the
blackboard or paper and imagine the rest in your mind.
- 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?
Subgoals emerge by applying a rule backwards. E.g. you start with a goal
"A & B" and apply the rule conjI: this produces subgoals A and B.
The Isar proof language has the virtue that it shows the structure of
sub-proofs directly in the text, in correspondence to Natural Deduction
rules that are applied (implicitly or explicitly). So you can just write
out the resoning directly, letting the system do the internal bookkeeping
of goals and rules:
notepad
begin
-- "explicit rules"
fix A B :: bool
have "A ∧ B ⟶ B ∧ A"
proof (rule impI)
assume *: "A ∧ B"
from * have a: A by (rule conjunct1)
from * have b: B by (rule conjunct2)
from b and a show "B ∧ A" by (rule conjI)
qed
next
-- "implicit rules"
fix A B :: bool
have "A ∧ B ⟶ B ∧ A"
proof
assume *: "A ∧ B"
from * have a: A ..
from * have b: B ..
from b and a show "B ∧ A" ..
qed
end
The Isabelle documentation provides more information on all that, tons of
manuals and examples ...
Makarius
Email Gateway (Aug 22 2022 at 09:41):From: Mandy Martin <tesleft@hotmail.com>
Hi Makarius,
it is difficult to imagine infinite disjunction and conjunction in truth table
Regards,
Martin Lee
Last updated: Apr 19 2024 at 01:05 UTC