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

Issue

Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto

Section

QED 20th anniversary

License

Copyright (c) 2016 Michael Beeson

Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.

Creative Commons License

This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy