Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Structure of Proofs


view this post on Zulip Email Gateway (Mar 07 2021 at 11:01):

From: "Jens-D. Doll" <jens.doll@live.de>
Hello everyone,

is there a common sense about how a proof has to be structured? Does
there exist a formal grammar or a mathematical structure for it? Can
coherence* be formalized?

Happy reasoning,
Jens

*from philosophy of science

view this post on Zulip Email Gateway (Mar 07 2021 at 18:27):

From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Jens,

you may want to have a look in Chapter 6 of the Isabelle manual

https://isabelle.in.tum.de/doc/isar-ref.pdf

where there are some details about common proof structures, e.g. proof
by induction,
proof by cases, proof by contradiction etc.-- in Isar there exist some
standard
ways for structuring these.

I'm not sure if this answers your question though.

Best wishes,
Angeliki

view this post on Zulip Email Gateway (Mar 08 2021 at 17:17):

From: "Jens-D. Doll" <jens.doll@live.de>
Hello Angeliki,

the basic types of proofs is not enough. I imagine a formal expression
over these types, which tells me if a certain sequence or hierarchy is
allowed. For instance a sequence of two proofs by contradiction is not
allowed?!

Jens


Last updated: Dec 08 2021 at 09:20 UTC