From: Rodrigo Raya <email@example.com>
|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
|Does this exist?|
From: Lawrence Paulson <firstname.lastname@example.org>
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.
From: Makarius <email@example.com>
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.
Last updated: Sep 25 2021 at 09:17 UTC