*Abstract:* We discuss a scheme for defining and reasoning
about partial recursive functions within a classical two-valued
logic in which all terms denote. We show how a total extension of
the partial function introduced by a recursive declaration may be
axiomatised within a classical logic, and illustrate by an example
the kind of reasoning that our scheme supports. By presenting a
naive set-theoretic semantics, we show that the system we propose
is logically consistent. We discuss some of the practical
advantages and limitations of our approach in the context of
mechanical theorem-proving.

**ECS-LFCS-96-341**, January 1996.

This report is available in the following formats:

- PDF file
- Gzipped PDF file
- PostScript file
- Gzipped PostScript file
- PostScript file with Type 1 fonts
- Gzipped PostScript file with Type 1 fonts
- LaTeX DVI file
- Gzipped LaTeX DVI file