Abstract
Requirements for tools which support the creation and the intelligible presentation of formal deductions are investigated. They are contrasted with requirements which emphasize the interactive construction of correct proofs. As an example, the design and the implementation of a set of support tools for Deva is described. Deva is a typed functional language and has been used in a number of case-studies on formal program development. The use of this toolset is illustrated by impressions of a working session.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors. Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.
J. R. Abrial. The B-Tool (Abstract). In R. Bloomfield, L. Marshall, and C. Jones, editors, VDM'88 — The Way Ahead. Springer-Verlag, 1988.
T. Altenkirch. A formalization of the strong normalization proof for sytem F in LEGO. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of LNCS, pages 13–28. Springer-Verlag, 1993.
M. Anlauff. Devil: Deva's Interactive Laboratory. Tutorial and User Manual. Technical Report 93–42, TU Berlin, 1993.
R. C. Backhouse. Making formality work for us. Bulletin of the EATCS, (38):219–249, June 1989.
R. C. Backhouse, R. Verhoeven, and O. Weber. MathSPad user manual. Technical report, Technical University of Eindhoven, Department of Computer Science, 1994.
M. Biersack, R. Raschke, and M. Simons. The DevaWEB system: Introduction, tutorial, user manual, and implementation. Technical Report 93–39, TU Berlin, 1993.
N. G. de Bruijn. A survey of the project AUTOMATH. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism [44], pages 579–606.
E. Clarke and X. Zhao. Analytica — An experiment in combining theorem proving and symbolic computation. Technical Report CMU-CS-92-147, Carnegie Mellon University, 1992.
R. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.
T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.
T. Coquand, B. Nordström, J. M. Smith, and B. von Sydow. Type theory and programming. Bulletin of the EATCS, (52):203–228, 1994.
E. W. Dijkstra and C. Scholten. Predicate Calculus and Predicate Transformers. Springer-Verlag, 1990.
G. Dowek et al. The Coq proof assitant user's guide. Technical report, INRIA Rocquencourt, 1991.
W. M. Farmer, J. D. Guttmann, and F. J. Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11:213–248, 1993.
A. J. M. van Gasteren. On the Shape of Mathematical Arguments, volume 441 of LNCS. Springer-Verlag, 1990.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.
D. Gries and F. B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
P. de Groote. Définition et Properiétés d'un Métacalcul de Représentation de Théories. PhD thesis, University of Louvain, 1990.
R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40 (1):143–184, 1993.
J. Harrison and L. Théry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. University of Cambridge Computer Laboratory.
W. A. Howard. The formulae-as-types notion of construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism [44], pages 479–490.
G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1:27–57, 1975.
G. Huet. Residual theory in λ-calculus: A formal development. Technical Report 2009, INRIA, 1993.
G. Huet and G. Plotkin, editors. Logical Frameworks. Cambridge University Press, 1991.
G. Huet and G. Plotkin, editors. Logical Environments. Cambridge University Press, 1993.
C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. Mural: A Formal Development Support System. Springer, 1991.
J. W. Klop. Term rewriting systems. In Abramsky et al. [1], pages 1–116.
D. Knuth. Literate programming. The Computer Journal, 27(2):97–111, May 1984.
D. Knuth. Literate Programming. Center for the Study of Language and Information, 1992.
L. Lamport. How to write a proof. Technical Report 94, DEC Systems Research Center, 1993.
Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.
Z. Luo and R. Pollack. The LEGO proof development system: A user's manual. Technical Report ECS-LFCS-92-211, University of Edinburgh, LFCS, 1992.
B. Möller, H. A. Partsch, and S. A. Schumann, editors. Formal Program Development, volume 755 of LNCS. Springer-Verlag, 1993.
C. Morgan. The refinement calculus, and literate developments. In Möller et al. [34], pages 161–182.
R. P. Nederpelt. Strong Normalization in a typed lambda calculus with lambda structured types. PhD thesis, Technical University of Eindhoven, 1973.
P. A. J. Noel. Experimenting with Isabelle in ZF set theory. Journal of Automated Reasoning, 10(1):15–58, 1993.
John K. Ousterhout. Tcl and the Tk Toolkit. Addison Wesley, 1994.
S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, Automated Deduction — CADE-11, volume 607 of LNCS, pages 567–581. Springer-Verlag, 1992.
L. C. Paulson. Designing a theorem prover. In Abramsky et al. [1], pages 415–475.
The QED manifesto. Can be obtained from info.mcs.anl.gov in the directory/pub/qed.
T. Santen. Formalization of the SPECTRUM methodology in Deva: Signature and logical calculus. Technical Report 93-04, TU Berlin, 1993.
F. W. Schroer. Gentle. In J. Grosch, F. W. Schroer, and W. M. Waite, editors, Three Compiler Specifications, number 166 in GMD-Studien, pages 31–36. GMD, Forschungsstelle an der Universität Karlsruhe, August 1989.
J. P. Seldin and J. R. Hindley. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.
J. H. Siekmann. Unification theory. Journal of Symbolic Computation, 7:207–274, 1989.
M. Simons, M. Biersack, and R. Raschke. Literate and structured presentation of formal proofs. In E.-R. Olderog, editor, IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94). North Holland, 1994.
M. Sintzoff. Understanding and expressing software construction. In P. Pepper, editor, Program Transformations and Programming Environments, pages 169–180. Springer-Verlag, 1980.
M. Sintzoff. Endomorphic ty**. In Möller et al. [34], pages 305–323.
J. L. A. van de Snepscheut. Proxac: an editor for program transformation. Technical Report Caltech-CS-TR-93-33, California Institute of Technology, 1993.
L. Théry, Y. Bertot, and G. Kahn. Real theorem provers deserve real user-interfaces. ACM Software Engineering Notes, 17(5), 1992. Fifth ACM SIGSOFT Symposium on Software Development Environments.
M. Weber. Deriving transitivity of VDM reification in the Deva meta-calculus. In S. Prehn and W. J. Toetenel, editors, VDM'91 Formal Software Development Methods, volume 551 of LNCS, pages 406–427. Springer, 1991.
M. Weber. Definition and basic properties of the Deva meta-calculus. Formal Aspects of Computing, 5:391–431, 1993.
M. Weber. Literate mathematical development of a revision management system. In T. Denvir, editor, Formal Methods Europe 1994. Springer-Verlag, 1994.
M. Weber, M. Simons, and Ch. Lafontaine. The Generic Development Language Deva: Presentation and Case Studies, volume 738 of LNCS. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Anlauff, M., Jähnichen, S., Simons, M. (1994). An experimental support system for formal mathematical reasoning. In: Naftalin, M., Denvir, T., Bertran, M. (eds) FME '94: Industrial Benefit of Formal Methods. FME 1994. Lecture Notes in Computer Science, vol 873. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58555-9_108
Download citation
DOI: https://doi.org/10.1007/3-540-58555-9_108
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58555-8
Online ISBN: 978-3-540-49031-9
eBook Packages: Springer Book Archive