Revising Basic Theorem Proving Algorithms to Cope withrnthe Logic of Partial Functions

摘要

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