Towards a Mechanisation of a Logic that Copes with Partial Terms

  1. Lookup NU author(s)
  2. Professor Cliff Jones
  3. Matthew Lovert
  4. Dr Jason Steggles
Author(s)Jones CB, Lovert MJ, Steggles LJ
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Legacy DateFebruary 2012
Report Number1314
Full text is available for this publication:
It has been pointed out by a number of authors that partial terms (i.e. terms that can fail to denote a value) arise frequently in the specification and development of programs. Furthermore, earlier papers describe and argue for the use of a non-classical logic (the "Logic of Partial Functions") to facilitate sound and convenient reasoning about such terms. This paper addresses some of the issues that arise in trying to provide (semi-)decision procedures -such as resolution- for such a logic. Particular care is needed with the use of "proof by refutation". The paper is grounded on a semantic model.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication