First Order Logic with Domain Conditions

9 years 6 months ago
First Order Logic with Domain Conditions
This paper addresses the crucial issue in the design of a proof development system of how to deal with partial functions and the related question of how to treat undefined terms. Often the problem is avoided by artificially making all functions total. However, that does not correspond to the practice of everyday mathematics. In type theory partial functions are modeled by giving functions extra arguments which are proof objects. In that case it will not be possible to apply functions outside their domain. However, having proofs as first class objects has the disadvantage that it will be unfamiliar to most mathematicians. Also many proof tools (like the theorem prover Otter) will not be usable for such a logic. Finally expressions get difficult to read because of these proof objects. The PVS system solves the problem of partial functions differently. PVS generates type-correctness conditions (TCCs) for statements in its language. These are proof obligations that have to be satisfie...
Freek Wiedijk, Jan Zwanenburg
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Authors Freek Wiedijk, Jan Zwanenburg
Comments (0)