Revising basic theorem proving algorithms to cope with the logic of partial functions

• Addresses the task of modifying proof procedures to handle the Logic of Partial Functions.
• Re-uses as much as possible of the standard literature.
• Provides proofs of the things that have to be modified.

Partial terms are those that can fail to denote a value; such terms arise frequently in the specification and development of programs. Earlier papers describe and argue for the use of the non-classical “Logic of Partial Functions” (LPF) to facilitate sound and convenient reasoning about such terms. This paper reviews the fundamental theorem proving algorithms — such as resolution — and identifies where they need revision to cope with LPF. Particular care is needed with “refutation” procedures. The modified algorithms are justified with respect to a semantic model. Indications are provided of further work which could lead to efficient support for LPF.