derived from Coq
's usage of it meaning a program which operates on a declarative
system in a procedural manner. That is, it operates on the declarative system in the mode of directing the proof
of it, possibly re-using existing proof procedures or overriding default ones.
This can be compared and contrasted with Maude's rewrite logic strategies.
This page is linked from: Coq Yarrow