Partial Functions in a Total Setting

Simon Finn, Michael P. Fourman, John Longley

Research output: Contribution to journalArticlepeer-review


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 axiomatized 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. Our work is motivated largely by the pragmatic issues arising from mechanical theorem proving – we discuss some of the practical benefits and limitations of our scheme for mechanical verification of software and hardware systems.
Original languageEnglish
Pages (from-to)85-104
Number of pages20
JournalJournal of Automated Reasoning
Issue number1
Publication statusPublished - 1997


  • partial recursive functions
  • mechanical theorem proving

Fingerprint Dive into the research topics of 'Partial Functions in a Total Setting'. Together they form a unique fingerprint.

Cite this