Abstract
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 satisfied ‘on the side’ to show that statements are well-formed.
We propose a TCC-like approach for the treatment of partial functions in type theory. We add domain conditions (DCs) to classical first-order logic and show the equivalence with a first order system that treats partial functions in the style of type theory.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Beeson, M.J.: Foundations of constructive mathematics. Springer, Heidelberg (1985)
Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ (1986)
Finn, S., Fourman, M., Longley, J.: Partial Functions in a Total Setting. Journal of Automated Reasoning 18, 85–104 (1997)
Geuvers, H., Wiedijk, F., Zwanenburg, J.: Equational Reasoning via Partial Reflection. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 162–178. Springer, Heidelberg (2000)
Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL. Cambridge University Press, Cambridge (1993)
Guttman, J.D., Thayer, F.J.: IMPS: An Interactive Mathematical Proof System. Journal of Automated Reasoning 11, 213–248 (1993)
Harrison, J.: Re: Undefined terms. Message <"swan.cl.cam.:266770:950519095422"@cl.cam.ac.uk> as sent to the QED mailing list (1995), http://www.ftp.cl.cam.ac.uk/ftp/hvg/qed-project-archive/03xx/0380
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)
Kuper, J.: Partiality in Logic and Computation – Aspects of Undefinedness. PhD thesis, University of Twente, Dept INF, Enschede, The Netherlands (1994)
Muzalewski, M.: An Outline of PC Mizar. Fondation Philippe le Hodey, Brussels (1993), http://www.cs.kun.nl/~freek/mizar/mizarmanual.ps.gz
Nederpelt, R.P., Geuvers, J.H., de Vrijer, R.C.: Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol. 133. Elsevier Science, Amsterdam (1994)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Scott, D.S.: Identity and existence in intuitionistic logic. In: Fourman, M.P., Mulvey, C.J., Scott, D.S. (eds.) Applications of Sheaves, Berlin. Lecture Notes in Mathematics, vol. 753, pp. 660–696. Springer, Heidelberg (1979)
Shankar, N., Owre, S.: Principles and Pragmatics of Subtyping in PVS. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 37–52. Springer, Heidelberg (2000)
The Coq Development Team. The Coq Proof Assistant Reference Manual (2002), ftp://ftp.inria.fr/INRIA/coq/current/doc/Reference-Manual-all.ps.gz
Troelstra, A., van Dalen, D.: Constructivism in Mathematics, an Introduction, Vols. 1-2. Studies in Logic and The Foundations of Mathematics, vol. 121 and 123. North-Holland, Amsterdam (1988)
Wos, L.: The Automation of Reasoning: An Experimenter’s Notebook with Otter Tutorial. Academic Press, New York (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wiedijk, F., Zwanenburg, J. (2003). First Order Logic with Domain Conditions. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_15
Download citation
DOI: https://doi.org/10.1007/10930755_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40664-8
Online ISBN: 978-3-540-45130-3
eBook Packages: Springer Book Archive