Structured calculational proof
- 1 September 1997
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 9 (5-6) , 469-483
- https://doi.org/10.1007/bf01211456
Abstract
We propose a new format for writing proofs, called structured calculational proof . The format resembles the calculational style already familiar to many computer scientists, but extends it to allow the hierarchical decomposition of larger proofs into smaller ones. Structured calculation is actually an alternative presentation of natural deduction, a style of reasoning which uses hierarchical decomposition to great effect, but which is traditionally expressed in a notation that is inconvenient for writing calculational proofs. The hierarchical nature of structured calculational proofs can be used for browsing proofs in electronic publications.Keywords
This publication has 11 references indexed in Scilit:
- Refinement CalculusPublished by Springer Nature ,1998
- Transformational Hierarchical ReasoningThe Computer Journal, 1996
- Formalizing a Hierarchical Structure of Practical Mathematical ReasoningJournal of Logic and Computation, 1993
- Induce-statements and induce-expressions: Constructs for inductive programmingPublished by Springer Nature ,1993
- A Practical Theory of ProgrammingPublished by Springer Nature ,1993
- Teaching calculation and discriminationCommunications of the ACM, 1991
- Predicate Calculus and Program SemanticsPublished by Springer Nature ,1990
- On the Shape of Mathematical ArgumentsPublished by Springer Nature ,1990
- A deficiency of natural deductionInformation Processing Letters, 1987
- Untersuchungen ber das logische Schlie en. IMathematische Zeitschrift, 1935