E3: A logic for reasoning equationally in the presence of partiality

Partiality abounds in specifications and programs. We present a three-value d typed logic for reasoning equationally about programming in the presence of partial functions. The logic in essence is a combination of the equation al logic E and typed LPF. Of course, there are already many logics in which some classical theorems acquire the status of neither-true-nor-false What is distinctive hers is that we preserve the equational reasoning style of E , as well as most of its main theorems. The principal losses among the theo rems are the law of the excluded middle, the anti-symmetry of implication, a small complication in the trading law for existential quantification, and the requirement to show definedness when using instantiation. The main los s among proof methods is proof by mutual implication; we present some new p roof strategies that make up for this loss. Some proofs are longer than in E, but the heuristics commonly used in the proof methodology of E remain va lid. We present a Hilbert-style axiomatisation of the logic in which modus ponens and generalisation are the only inference rules. The axiomatisation is easily modified to yield a classical axiomatisation of E itself. We sugg est that the logic may be readily extended to a many-valued logic, and that this will have its uses. (C) 1999 Elsevier Science B.V. All rights reserve d.