Email Gateway (Aug 29 2020 at 17:22): Email Gateway (Aug 29 2020 at 17:22):From: Rodrigo Raya <rodrigo.raya@epfl.ch>
|I have scanned the Isabelle/Isar manual for tracers. However, I
couldn't find a method to trace resolution proofs. My goal is to see
when proving a theorem what steps go through the resolution rule if any.
Having that for unification could also help (currently, I only know of
unify_trace_failure).|
| Does this exist? |
|---|
|Thank you,|
| Rodrigo |
|---|
Email Gateway (Aug 31 2020 at 09:07):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m not quite sure what you are asking, but the resolution rule is normally regarded as an atomic step in the proof kernel. Also unification.
Larry
Email Gateway (Aug 31 2020 at 12:22):From: Makarius <makarius@sketis.net>
Just the standard meta-questions: What is your application? What do you try to
achieve? What do you actually need?
At the bottom of all proof tools based on higher-order resolution is the
primitive rule Thm.bicompose(_aux) (in $ISABELLE_HOME/src/Pure/thm.ML).
But that is rather complex and low-level: it is used a lot in many different
contexts, also with search over lazy sequences. Thus it is difficult to
extract useful information.
Makarius
Last updated: Jul 15 2022 at 23:21 UTC