On calculational proofs

Annals of Pure and Applied Logic 113 (1-3):207-224 (2001)
  Copy   BIBTEX

Abstract

This note is about the “calculational style” of presenting proofs introduced by Dijkstra and Scholten and adopted in some books on theoretical computer science. We define the concept of a calculation, which is a formal counterpart of the idea of a calculational proof. The definition is in terms of a new formalization DS of predicate logic. Any proof tree in the system DS can be represented as a sequence of calculations. This fact shows that any logically valid predicate formula has a calculational proof

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 76,479

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Probabilistic proofs and transferability.Kenny Easwaran - 2009 - Philosophia Mathematica 17 (3):341-362.
The Depth of Resolution Proofs.Alasdair Urquhart - 2011 - Studia Logica 99 (1-3):349-364.
Why feynman diagrams represent.Letitia Meynell - 2008 - International Studies in the Philosophy of Science 22 (1):39 – 59.
Hypothetical Logic of Proofs.Eduardo Bonelli & Gabriela Steren - 2014 - Logica Universalis 8 (1):103-140.
The three dimensions of proofs.Yves Guiraud - 2006 - Annals of Pure and Applied Logic 141 (1):266-295.
Why do mathematicians re-prove theorems?John W. Dawson Jr - 2006 - Philosophia Mathematica 14 (3):269-286.
The role of diagrams in mathematical arguments.David Sherry - 2008 - Foundations of Science 14 (1-2):59-74.

Analytics

Added to PP
2014-01-16

Downloads
10 (#891,033)

6 months
1 (#455,463)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

No references found.

Add more references