Abstract
We introduce a semantics for classical logic with partial functions, in which ill-typed formulas are guaranteed to have no truth value, so that they cannot be used in any form of reasoning. The semantics makes it possible to mix reasoning about types and preconditions with reasoning about other properties. This makes it possible to deal with partial functions with preconditions of unlimited complexity. We show that, in spite of its increased complexity, the semantics is still a natural generalization of first-order logic with simple types. If one does not use the increased expressivity, the type system is not stronger than classical logic with simple types. We will define two sequent calculi for our semantics, and prove that they are sound and complete. The first calculus follows the semantics closely, and hence its completeness proof is fairly straightforward. The second calculus is further away from the semantics, but more suitable for practical use because it has better proof theoretic properties. Its completeness can be shown by proving that proofs from the first calculus can be translated.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.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). Electronic Notes in Theoretical Computer Science, vol. 125, pp. 13–23. Elsevier (2005)
Darvas, Á., Mehta, F., Rudich, A.: Efficient well-definedness checking. In: Armado, A., Baumgartner, P., Dowek, G. (eds.) International Joint Conference on Automated Reasoning (IJCAR) 2008. LNAI, vol. 5195, pp. 100–115. Springer (2008)
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. Stud. Log. 66, 59–78 (2000)
Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)
Hähnle, R.: Many-valued logic, partiality, and abstraction in formal specification languages. Log. J. IGPL 13(4), 415–433 (2005)
Kerber, M., Kohlhase, M.: A mechanization of strong Kleene logic for partial functions. In: Automated Deduction—CADE 12. LNAI, vol. 814, pp. 371–385. Springer (1994)
Mehta, F.: A practical approach to partiality—a proof based approach. In: Liu, S., Maibaum, T. (eds.) International Conference on Formal Engineering Methods, (ICFEM). LNCS, vol. 5256, pp. 238–257. Springer (2008)
de Nivelle, H.: Theorem prover Geo 2007F. Can be obtained from the author’s homepage (2007)
de Nivelle, H.: Classical logic with partial functions. In: Giesl, J., Hähnle, R. (eds.) International Joint Conference on Automated Reasoning (IJCAR) 2010. LNAI, vol. 6173, pp. 203–217. Springer (2010)
de Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: Harrison, J., Furbach, U., Shankar, N. (eds.) International Joint Conference on Automated Reasoning 2006. Lecture Notes in Artificial Intelligence, vol. 4130, pp. 303–317. Springer, Seattle, USA (2006)
Orevkov, V.: Lower bounds for increasing complexity of derivations after cut elimination. Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta Imenyi V.A. Steklova AN SSSR 88, 137–161 (1979). English translation in J. Sov. Math. 2337–2350 (1982)
Scott, D.: Existence and description in formal logic. In: Fourman, M. (ed.) Applications of Sheaves. LNM, pp. 660–696. Springer (1977)
Statman, R.: Lower bounds on Herbrand’s theorem. In: Proceedings of the American Mathematical Society, vol. 75-1, pp. 104–107. American Mathematical Society, Providence (1979)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
de Nivelle, H. Classical Logic with Partial Functions. J Autom Reasoning 47, 399–425 (2011). https://doi.org/10.1007/s10817-011-9236-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-011-9236-z