Now f is continuous (exercise!)

Authors

  • Robin Denis Arthan Lemma 1 Ltd. & Department of Computer Science, Oxford University

DOI:

https://doi.org/10.6092/issn.1972-5787/4566

Keywords:

interactive theorem proving, decision procedure, formalised mathematics

Abstract

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

Downloads

Published

2016-01-29

How to Cite

Arthan, R. D. (2016). Now f is continuous (exercise!). Journal of Formalized Reasoning, 9(1), 33–52. https://doi.org/10.6092/issn.1972-5787/4566