Abstract
Rewriting logic can be used to prototype systems for automated
deduction. In this paper, we illustrate how this approach allows
experiments with deduction strategies in a flexible and conceptually
satisfying way.
This is achieved by exploiting the reflective property of rewriting
logic. By specifying a theorem prover in this way one quickly
obtains a readable, reliable and reasonably efficient system which
can be used both as a platform for tactic experiments and as a basis
for an optimized implementation. The approach is illustrated by
specifying a calculus for the connection method in rewriting logic
which clearly separates rules from tactics.