#
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.