using [[simp_trace]] let's you see what simplification rules were used and using [[unify_trace_failure]] let's you see what unification issues were encountered. I wonder if resolution proofs can be equally traced. This would make Isabelle proofs effectively surveyable.
Asked
Active
Viewed 139 times
1
user1868607
- 2,558
- 1
- 17
- 38
-
i found one can do this traces [[simp_trace,linarith_trace,metis_trace,smt_trace]] , ML_exception_trace and more by scanning the isabelle/isar manual for _trace – user1868607 Aug 29 '20 at 00:27
-
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-March/msg00065.html – user1868607 Sep 02 '20 at 16:29
1 Answers
1
I don't think one can trace auto, blast,... step by step or get proof scripts from them. (this mailing list thread should be interesting for you). What you can do is get a list of the used facts, for more details see davidgs answer in this thread.
MercedesJones
- 164
- 6
-
indeed, there does not seem to be support for this (according to the user mailing list of today) – user1868607 Aug 31 '20 at 21:49