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.
Unable to display preview. Download preview PDF.
- 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
- E. W. Dijkstra. Our Proof Format. 26 January 1987. EWD999.Google Scholar
- J. V. Guttag, J. J. Horning, and J. M. Wing. Larch in Five Easy Pieces. Technical Report 5, DEC, SRC, 1985.Google Scholar
- 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
- 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
- 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
- P. A. Lindsay. A formal system with inclusion polymorphism. IPSE Document 060/pa1014/2. 3, December 1987. Manchester University.Google Scholar