Subject: Refiner

Keywords: ::dekreitz
          ::tactic
          ::proof

Title: Kreitzing and dekreitzing

--------------------------------------------------

Kreitzing is the process of combining tactic expressions in 
a proof tree to with tacticals to reduce proof tree to a single
step. The subgoals of the new step must be equivalent to the
frontier of the orginal proof tree.

Dekreitzing is the process of destructing a tactic expression from
a proof step to produce a proof tree whose frontier is equivalent
to the frontier of the original step.

This process is named after Christoph Kreitz who originally thought to
kreitz proofs to make them more readable.⋅
--------------------------------------------------

Authors: 

Contributors: RICH:t

⋅

Home