Now f is continuous (exercise!)

Journal of Formalized Reasoning

Robin Denis Arthan

关键词: interactive theorem proving;    decision procedure;    formalised mathematics;   

DOI  :  10.6092/issn.1972-5787/4566

学科分类：计算机科学（综合）

来源: Universita degli Studi di Bologna

【 摘 要 】

A recurring proof obligation in modern mathematics, ranging from textbook exercises to deep research problems, is to show that a given function is a morphism in some category: in analysis and topology, for example, we frequently need to prove that functions are continuous, while in group theory we are constantly concerned with homomorphisms. This paper describes a generic procedure that automatically discharges routine instances of this kind of proof obligation in an interactive theorem prover. The proof procedure has been implemented and found very useful in a mathematical case studies carried out using the ProofPower system

【 授权许可】

CC BY