{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:51Z","timestamp":1725664371271},"publisher-location":"Berlin, Heidelberg","reference-count":54,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540585558"},{"type":"electronic","value":"9783540490319"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58555-9_108","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:36:17Z","timestamp":1330274177000},"page":"421-440","source":"Crossref","is-referenced-by-count":2,"title":["An experimental support system for formal mathematical reasoning"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Anlauff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"J\u00e4hnichen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Simons","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"unstructured":"S. Abramsky, D. Gabbay, and T. S. E. Maibaum, editors. Handbook of Logic in Computer Science, volume 2. Oxford University Press, 1992.","key":"26_CR1"},{"doi-asserted-by":"crossref","unstructured":"J. R. Abrial. The B-Tool (Abstract). In R. Bloomfield, L. Marshall, and C. Jones, editors, VDM'88 \u2014 The Way Ahead. Springer-Verlag, 1988.","key":"26_CR2","DOI":"10.1007\/3-540-50214-9_8"},{"doi-asserted-by":"crossref","unstructured":"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\u201328. Springer-Verlag, 1993.","key":"26_CR3","DOI":"10.1007\/BFb0037095"},{"unstructured":"M. Anlauff. Devil: Deva's Interactive Laboratory. Tutorial and User Manual. Technical Report 93\u201342, TU Berlin, 1993.","key":"26_CR4"},{"key":"26_CR5","first-page":"219","volume":"38","author":"R. C. Backhouse","year":"1989","unstructured":"R. C. Backhouse. Making formality work for us. Bulletin of the EATCS, (38):219\u2013249, June 1989.","journal-title":"Bulletin of the EATCS"},{"unstructured":"R. C. Backhouse, R. Verhoeven, and O. Weber. MathSPad user manual. Technical report, Technical University of Eindhoven, Department of Computer Science, 1994.","key":"26_CR6"},{"unstructured":"M. Biersack, R. Raschke, and M. Simons. The DevaWEB system: Introduction, tutorial, user manual, and implementation. Technical Report 93\u201339, TU Berlin, 1993.","key":"26_CR7"},{"doi-asserted-by":"crossref","unstructured":"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\u2013606.","key":"26_CR8","DOI":"10.1016\/S0049-237X(08)70203-9"},{"doi-asserted-by":"crossref","unstructured":"E. Clarke and X. Zhao. Analytica \u2014 An experiment in combining theorem proving and symbolic computation. Technical Report CMU-CS-92-147, Carnegie Mellon University, 1992.","key":"26_CR9","DOI":"10.21236\/ADA258656"},{"unstructured":"R. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.","key":"26_CR10"},{"key":"26_CR11","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"26_CR12","first-page":"203","volume":"52","author":"T. Coquand","year":"1994","unstructured":"T. Coquand, B. Nordstr\u00f6m, J. M. Smith, and B. von Sydow. Type theory and programming. Bulletin of the EATCS, (52):203\u2013228, 1994.","journal-title":"Bulletin of the EATCS"},{"doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra and C. Scholten. Predicate Calculus and Predicate Transformers. Springer-Verlag, 1990.","key":"26_CR13","DOI":"10.1007\/978-1-4612-3228-5"},{"unstructured":"G. Dowek et al. The Coq proof assitant user's guide. Technical report, INRIA Rocquencourt, 1991.","key":"26_CR14"},{"key":"26_CR15","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"W. M. Farmer, J. D. Guttmann, and F. J. Thayer. IMPS: An interactive mathematical proof system. Journal of Automated Reasoning, 11:213\u2013248, 1993.","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"A. J. M. van Gasteren. On the Shape of Mathematical Arguments, volume 441 of LNCS. Springer-Verlag, 1990.","key":"26_CR16","DOI":"10.1007\/BFb0020908"},{"unstructured":"M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, 1993.","key":"26_CR17"},{"doi-asserted-by":"crossref","unstructured":"D. Gries and F. B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.","key":"26_CR18","DOI":"10.1007\/978-1-4757-3837-7"},{"unstructured":"P. de Groote. D\u00e9finition et Properi\u00e9t\u00e9s d'un M\u00e9tacalcul de Repr\u00e9sentation de Th\u00e9ories. PhD thesis, University of Louvain, 1990.","key":"26_CR19"},{"issue":"1","key":"26_CR20","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40 (1):143\u2013184, 1993.","journal-title":"Journal of the ACM"},{"unstructured":"J. Harrison and L. Th\u00e9ry. Extending the HOL theorem prover with a computer algebra system to reason about the reals. University of Cambridge Computer Laboratory.","key":"26_CR21"},{"unstructured":"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\u2013490.","key":"26_CR22"},{"key":"26_CR23","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"unstructured":"G. Huet. Residual theory in \u03bb-calculus: A formal development. Technical Report 2009, INRIA, 1993.","key":"26_CR24"},{"doi-asserted-by":"crossref","unstructured":"G. Huet and G. Plotkin, editors. Logical Frameworks. Cambridge University Press, 1991.","key":"26_CR25","DOI":"10.1017\/CBO9780511569807"},{"unstructured":"G. Huet and G. Plotkin, editors. Logical Environments. Cambridge University Press, 1993.","key":"26_CR26"},{"doi-asserted-by":"crossref","unstructured":"C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. Mural: A Formal Development Support System. Springer, 1991.","key":"26_CR27","DOI":"10.1007\/978-1-4471-3180-9"},{"doi-asserted-by":"crossref","unstructured":"J. W. Klop. Term rewriting systems. In Abramsky et al. [1], pages 1\u2013116.","key":"26_CR28","DOI":"10.1093\/oso\/9780198537618.003.0001"},{"issue":"2","key":"26_CR29","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1093\/comjnl\/27.2.97","volume":"27","author":"D. Knuth","year":"1984","unstructured":"D. Knuth. Literate programming. The Computer Journal, 27(2):97\u2013111, May 1984.","journal-title":"The Computer Journal"},{"unstructured":"D. Knuth. Literate Programming. Center for the Study of Language and Information, 1992.","key":"26_CR30"},{"unstructured":"L. Lamport. How to write a proof. Technical Report 94, DEC Systems Research Center, 1993.","key":"26_CR31"},{"unstructured":"Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990.","key":"26_CR32"},{"unstructured":"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.","key":"26_CR33"},{"doi-asserted-by":"crossref","unstructured":"B. M\u00f6ller, H. A. Partsch, and S. A. Schumann, editors. Formal Program Development, volume 755 of LNCS. Springer-Verlag, 1993.","key":"26_CR34","DOI":"10.1007\/3-540-57499-9"},{"doi-asserted-by":"crossref","unstructured":"C. Morgan. The refinement calculus, and literate developments. In M\u00f6ller et al. [34], pages 161\u2013182.","key":"26_CR35","DOI":"10.1007\/3-540-57499-9_20"},{"unstructured":"R. P. Nederpelt. Strong Normalization in a typed lambda calculus with lambda structured types. PhD thesis, Technical University of Eindhoven, 1973.","key":"26_CR36"},{"issue":"1","key":"26_CR37","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00881863","volume":"10","author":"P. A. J. Noel","year":"1993","unstructured":"P. A. J. Noel. Experimenting with Isabelle in ZF set theory. Journal of Automated Reasoning, 10(1):15\u201358, 1993.","journal-title":"Journal of Automated Reasoning"},{"unstructured":"John K. Ousterhout. Tcl and the Tk Toolkit. Addison Wesley, 1994.","key":"26_CR38"},{"doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In D. Kapur, editor, Automated Deduction \u2014 CADE-11, volume 607 of LNCS, pages 567\u2013581. Springer-Verlag, 1992.","key":"26_CR39","DOI":"10.1007\/3-540-55602-8_217"},{"doi-asserted-by":"crossref","unstructured":"L. C. Paulson. Designing a theorem prover. In Abramsky et al. [1], pages 415\u2013475.","key":"26_CR40","DOI":"10.1093\/oso\/9780198537618.003.0004"},{"unstructured":"The QED manifesto. Can be obtained from info.mcs.anl.gov in the directory\/pub\/qed.","key":"26_CR41"},{"unstructured":"T. Santen. Formalization of the SPECTRUM methodology in Deva: Signature and logical calculus. Technical Report 93-04, TU Berlin, 1993.","key":"26_CR42"},{"unstructured":"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\u201336. GMD, Forschungsstelle an der Universit\u00e4t Karlsruhe, August 1989.","key":"26_CR43"},{"unstructured":"J. P. Seldin and J. R. Hindley. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.","key":"26_CR44"},{"key":"26_CR45","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. H. Siekmann","year":"1989","unstructured":"J. H. Siekmann. Unification theory. Journal of Symbolic Computation, 7:207\u2013274, 1989.","journal-title":"Journal of Symbolic Computation"},{"unstructured":"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.","key":"26_CR46"},{"doi-asserted-by":"crossref","unstructured":"M. Sintzoff. Understanding and expressing software construction. In P. Pepper, editor, Program Transformations and Programming Environments, pages 169\u2013180. Springer-Verlag, 1980.","key":"26_CR47","DOI":"10.1007\/978-3-642-46490-4_16"},{"doi-asserted-by":"crossref","unstructured":"M. Sintzoff. Endomorphic typing. In M\u00f6ller et al. [34], pages 305\u2013323.","key":"26_CR48","DOI":"10.1007\/3-540-57499-9_24"},{"unstructured":"J. L. A. van de Snepscheut. Proxac: an editor for program transformation. Technical Report Caltech-CS-TR-93-33, California Institute of Technology, 1993.","key":"26_CR49"},{"doi-asserted-by":"crossref","unstructured":"L. Th\u00e9ry, 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.","key":"26_CR50","DOI":"10.1145\/142868.143760"},{"doi-asserted-by":"crossref","unstructured":"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\u2013427. Springer, 1991.","key":"26_CR51","DOI":"10.1007\/3-540-54834-3_25"},{"key":"26_CR52","doi-asserted-by":"crossref","first-page":"391","DOI":"10.1007\/BF01212485","volume":"5","author":"M. Weber","year":"1993","unstructured":"M. Weber. Definition and basic properties of the Deva meta-calculus. Formal Aspects of Computing, 5:391\u2013431, 1993.","journal-title":"Formal Aspects of Computing"},{"doi-asserted-by":"crossref","unstructured":"M. Weber. Literate mathematical development of a revision management system. In T. Denvir, editor, Formal Methods Europe 1994. Springer-Verlag, 1994.","key":"26_CR53","DOI":"10.1007\/3-540-58555-9_109"},{"doi-asserted-by":"crossref","unstructured":"M. Weber, M. Simons, and Ch. Lafontaine. The Generic Development Language Deva: Presentation and Case Studies, volume 738 of LNCS. Springer-Verlag, 1993.","key":"26_CR54","DOI":"10.1007\/3-540-57335-6"}],"container-title":["Lecture Notes in Computer Science","FME '94: Industrial Benefit of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58555-9_108.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T16:15:40Z","timestamp":1713629740000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58555-9_108"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540585558","9783540490319"],"references-count":54,"URL":"https:\/\/doi.org\/10.1007\/3-540-58555-9_108","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}