Automating Side Conditions in Formalized Partial Functions

Abstract. Assumptions about the domains of partial functions are necessary in state-of-the-art proof assistants. On the other hand when mathematicians write about partial functions they tend not to explicitly write the side conditions. We present an approach to formalizing partiality in real and complex analysis in total frameworks that allows keeping the side conditions hidden from the user as long as they can be computed and simplified automatically. This framework simplifies defining and operating on partial functions in formalized real analysis in HOL LIGHT. Our framework allows simplifying expressions under partiality conditions in a proof assistant in a manner that resembles computer algebra systems.

• Type: Conference
• Year: 2008
• Where: AISC
• Authors: Cezary Kaliszyk
• Keywords: AISC 2008, Artificial Intelligence, Partial Functions, Proof Assistant, State-of-the-art Proof Assistants