Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

TPHOL

2003

IEEE

2003

IEEE

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 undeﬁned terms. Often the problem is avoided by artiﬁcially 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 ﬁrst 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 diﬃcult to read because of these proof objects. The PVS system solves the problem of partial functions diﬀerently. PVS generates type-correctness conditions (TCCs) for statements in its language. These are proof obligations that have to be satisﬁe...

Related Content

Added |
05 Jul 2010 |

Updated |
05 Jul 2010 |

Type |
Conference |

Year |
2003 |

Where |
TPHOL |

Authors |
Freek Wiedijk, Jan Zwanenburg |

Comments (0)