Logic with Partial Functions in CVC Lite

Abstract

Partial functions occur commonly in mathematics and formal verification. Surprisingly though, the problem of reasoning about partial functions has been largely ignored in mathematical logic and automated deduction research. A few approaches propose logics of partial functions and their translations to classical logic, but there is still no consensus on which is ``the right'' logic to use. In this paper, we propose using a three-valued Kleene logic, where partial functions return the ``undefined'' value when applied outside of their domains. The particular semantics are chosen according to the \emph{principle of least surprise} to the user; if it is unclear what the value of the formula should be (from the classical point of view), its evaluation is undefined. We also enrich the logic with the if-then-else operator, which is necessary to model many large-scale formal verification problems, and devise a practically efficient extension of the existing validity checking algorithm implemented in the CVC Lite tool.