Advertisement

Consequences

  • Cliff B. Jones
Part of the Texts and Monographs in Computer Science book series (MCS)

Abstract

A proof is a chain of reasoning in which each step is mediated by a consequence relation. A variety of consequence notions exist. This paper explores the extent to which congruences between consequence notions can be used to yield congruent proofs in different theories.

Keywords

Inference Rule Natural Deduction Natural Deduction Proof Proof Style Systematic Software Development 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    J. C. Bicarregui and B. Ritchie. Providing support for the formal development of software. In Proceedings of the 1st International Conference on System Development Environments and Factories, 1989. Berlin.Google Scholar
  2. [2]
    E. W. Dijkstra. Our Proof Format. 26 January 1987. EWD999.Google Scholar
  3. [3]
    A. J. M. van Gasteren. On the Shape of Mathematical Arguments. Ph.D. thesis, Eindhoven University of Technology, 1988.MATHGoogle Scholar
  4. [4]
    J. V. Guttag, J. J. Horning, and J. M. Wing. Larch in Five Easy Pieces. Technical Report 5, DEC, SRC, 1985.Google Scholar
  5. [5]
    C. B. Jones and P. A. Lindsay. A support system for formal reasoning: requirements and status. In R. Bloomfield, L. Marshall, and R. Jones, editors, VDM’88: VDM—The Way Ahead, pages 139–152, Springer- Verlag, 1988. Lecture Notes in Computer Science, Vol. 328.Google Scholar
  6. [6]
    C. B. Jones and R. Moore. Muffin: a user interface design experiment for a theorem proving assistant. In R. Bloomfield, L. Marshall, and R. Jones, editors, VDM’88: VDM—The Way Ahead, pages 337–375, Springer-Verlag, 1988. Lecture Notes in Computer Science, Vol. 328.Google Scholar
  7. [7]
    Cliff B. Jones. Systematic Software Development using VDM. Prentice Hall International, second edition, 1990.MATHGoogle Scholar
  8. [8]
    P. A. Lindsay . Formal reasoning in an IPSE. In K. H. Bennet, editor, Software Engineering Environments: Research and Practice, pages 235–253, Ellis Harwood Ltd, 1989.Google Scholar
  9. [9]
    P. A. Lindsay. A formal system with inclusion polymorphism. IPSE Document 060/pa1014/2. 3, December 1987. Manchester University.Google Scholar
  10. [10]
    D. Prawitz. Natural Deduction. Almquist and Wiksell, 1965.MATHGoogle Scholar

Copyright information

© Springer-Verlag New York, Inc. 1990

Authors and Affiliations

  • Cliff B. Jones
    • 1
  1. 1.Department of Computer ScienceThe UniversityManchesterEngland

Personalised recommendations