Maximilian Spitz (Apr 22 2023 at 07:10): Maximilian Spitz (Apr 22 2023 at 07:10):Hi, I am curious if proof-methods like auto proceed deterministically, e. g. when loading the same theory in different instances if it will find the same axiomatic proof (modulo different versions of Isabelle etc.) / and related to that I would like to know if there is a way to display or inspect the proof auto produces in the background.
Also, I found a paper called "Isabelle for Philosophers", which is a small introduction to propositional-/FOL with many interesting exercises on axiomatic proofs, which I enjoyed a lot and which induced this question in the first place. Also, I would be very happy about any recommendations for interesting resources like that.
Thank you!
Wolfgang Jeltsch (Apr 22 2023 at 15:05):“Isabelle for Philosophers” sounds interesting. I might give that a read.
I just had a look at the first page and realized that the author started with a quote and got the name of its author, one of the most famous philosophers, wrong: he wrote “Liebniz” instead of “Leibniz”. :rolling_eyes:
Christian Pardillo Laursen (Apr 25 2023 at 13:06):To display the proofs auto produces I use the apply_trace tool: https://github.com/seL4/l4v/blob/master/lib/Eisbach_Tools/Apply_Trace_Cmd.thy . Proof methods like auto do proceed deterministically; it would be catastrophic if formalised proofs couldn't be reproduced because you randomly got the wrong execution path.
Last updated: Apr 27 2024 at 20:14 UTC