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.