Abstract
We introduce a semantics for classical logic with partial functions. We believe that the semantics is natural. When a formula contains a subterm in which a function is applied outside of its domain, our semantics ensures that the formula has no truth-value, so that it cannot be used for reasoning. The semantics relies on order of formulas. In this way, it is able to ensure that functions and predicates are properly declared before they are used. We define a sequent calculus for the semantics, and prove that this calculus is sound and complete for the semantics.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Berezin, S., Barrett, C., Shikanian, I., Chechik, M., Gurfinkel, A., Dill, D.: A practical approach to partial functions in CVC Lite. In: Selected Papers from the Workshop on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 04), July 2005. Electronic Notes in Theoretical Computer Science, vol. 125, pp. 13–23. Elsevier, Amsterdam (2005)
Darvas, Á., Mehta, F., Rudich, A.: Efficient well-definedness checking. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 100–115. Springer, Heidelberg (2008)
de Nivelle, H.: Theorem prover Geo 2007F. Can be obtained from the author’s homepage (September 2007)
de Nivelle, H., Meng, J.: Geometric resolution: A proof procedure based on finite model search. In: Harrison, J., Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 303–317. Springer, Heidelberg (2006)
Farmer, W.M.: Mechanizing the traditional approach to partial functions. In: Farmer, W., Kerber, M., Kohlhase, M. (eds.) Proceedings of the Workshop on the Mechanization of Partial Functions (associated to CADE 13), pp. 27–32 (1996)
Farmer, W.M., Guttman, J.D.: A set theory with support for partial functions. Studia Logica 66, 59–78 (2000)
Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Logic Journal of the IGPL 13(4), 415–433 (2005)
Kerber, M., Kohlhase, M.: A mechanization of strong Kleene logic for partial functions. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 371–385. Springer, Heidelberg (1994)
Mehta, F.: A practical approach to partiality - a proof based approach. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 238–257. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Nivelle, H. (2010). Classical Logic with Partial Functions. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-14203-1_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14202-4
Online ISBN: 978-3-642-14203-1
eBook Packages: Computer ScienceComputer Science (R0)