Algorithmic proof-search is an essential enabling technology throughout informatics. Proof-search is the proof-theoretic realisation of the formulation of logic not as a theory of deduction but rather as a theory of reduction. Whilst deductive logics typically have a well-developed semantics of proofs, reductive logics are typically well-understood only operationally. Each deductive system can, typically, be read as a corresponding reductive system. We discuss some of the problems which must be addressed in order to provide such a semantics of proof-searches of comparable value to the corresponding semantics of proofs. Just as the semantics of proofs is intimately related to the model theory of the underlying logic, so too should be the semantics of proof-searches. We discuss how it is that the semantics of search is essentially constructive, in the sense of Kripke, and how to solve the problem of providing a semantics for (the construction of) proof-searches which adequately models both the operational and logical aspects of the reductive logic. In particular, we propose an algebraic approach to the semantics of control.

(cf. ENTCS 37(2000), 18pp.)