Mixing Computations and Proofs

Authors

  • Michael Beeson San Jose State University

DOI:

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

Keywords:

computation, formal proof, logic

Abstract

We examine the relationship between proof and computation in mathematics, especially in formalized mathematics. We compare the various approaches to proofs with a significant computational component, including (i) verifying  the algorithms, (ii) verifying the results of the unverified algorithms, and (iii) trusting an external computation.  

Downloads

Published

2016-01-29

How to Cite

Beeson, M. (2016). Mixing Computations and Proofs. Journal of Formalized Reasoning, 9(1), 71–99. https://doi.org/10.6092/issn.1972-5787/4552