Towards a Mechanisation of a Logic that Copes with Partial Terms (2012)

Author(s): Jones CB, Lovert MJ, Steggles LJ

    Abstract: 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.

      • Date: February 2012
      • Series Title: School of Computing Science Technical Report Series
      • Pages: 24
      • Institution: School of Computing Science, University of Newcastle upon Tyne
      • Publication type: Report
      • Bibliographic status: Published

        Keywords: PARTIAL FUNCTIONS LPF RESOLUTION UNIFICATION REFUTATION PROCEDURE

        Staff

        Professor Cliff Jones
        Professor
        • Telephone: +44 191 222 8183

        Dr Jason Steggles
        Senior Lecturer