A proof-centric approach to mathematical assistants

Wenzel, 1999, Isar—a generic interpretative approach to readable formal proof documents, vol. 1690, 167 Paulson, 1994 Dixon, 2003, IsaPlanner: A prototype proof planner in Isabelle, vol. 2741, 279 Rudnicki, 1992, An overview of the Mizar project, 311 Zammit Autexier, 2003, Assertion-level proof representation with under-specification, Electronic in Theoret. Comput. Sci., 93, 5, 10.1016/j.entcs.2003.12.026 D. Syme, Declarative theorem proving for operational semantics, Ph.D. thesis, University of Cambridge, 1999 Abel Harrison, 1996, A Mizar mode for HOL, vol. 1125, 203 Weidijk, 2001, Mizar light for HOL light, vol. 2152, 378 F. Wiedijk, Formal proof sketches, in: TYPES, 2003, pp. 378–393 Ireland, 1996, Productive use of failure in inductive proof, J. Automat. Reason., 16, 79, 10.1007/BF00244460 Ireland, 1999, Interactive proof critics, Formal Asp. Comput., 11, 302, 10.1007/s001650050052 Paulson, 2002 Paulson, 1997, Generic automatic proof tools, 23 Paulson, 1999, A generic tableau prover and its integration with Isabelle, J. Universal Comput. Sci., 5, 73 Melis, 2000, Proof planning with multiple strategies, vol. 1861, 644 A. Bundy, The use of explicit plans to guide inductive proofs, in: Conference on Automated Deduction, 1988, pp. 111–120, citeseer.nj.nec.com/bundy88use.html Bundy, 1991, A science of reasoning, Computational Logic (Essays in Honor of Alan Robinson), 6, 178 L. Dixon, A proof planning framework for Isabelle, Ph.D. thesis, School of Informatics, University of Edinburgh, January 2005 Dixon, 2004, Higher order rippling in IsaPlanner, vol. 3223, 83 Bundy, 2005 Richardson, 1998, System description: proof planning in higher-order logic with Lambda-Clam, vol. 1421, 129 Fleuriot, 2001 L.I. Meikle, J.D. Fleuriot, Formalizing Hilbert's Grundlagen in Isabelle/Isar, in: Theorem Proving in Higher Order Logics, 2003, pp. 319–334 C. Laumann, An idealistic formalization of Stokes' theorem: Pedagogical math in Isabelle/Isar, Master's thesis, School of Informatics, University of Edinburgh, 2004 M. Wenzel, Type classes and overloading in higher-order logic, in: Theorem Proving in Higher Order Logics, 1997, pp. 307–322 C. Ballarin, Locales and locale expressions in Isabelle/Isar, in: TYPES, 2003, pp. 34–50 F. Kammüller, Modular reasoning in Isabelle, Ph.D. thesis, University of Cambridge, August 1999 Hindley, 1969, The principal type-scheme of an object in combinatory logic, Trans. Amer. Math. Soc., 146, 29 Milner, 1978, A theory of type polymorphism in programming, J. Comput. Syst. Sci., 17, 348, 10.1016/0022-0000(78)90014-4 Nipkow, 1993, Order-sorted polymorphism in Isabelle, 164 Melham, 1992, The HOL logic extended with quantification over type variables, 3 Johnsen, 2004, Theorem reuse by proof term transformation, vol. 3223, 152 F. Guidi, I. Schena, A query language for a metadata framework about mathematical resources, in: MKM, 2003, pp. 105–118 S. Autexier, D. Hutter, H. Mantel, A. Schairer, Towards an evolutionary formal software-development using CASL, in: Workshop on Algebraic Development Techniques, 1999, pp. 73–88, citeseer.ist.psu.edu/article/autexier99towards.html A. Fiedler, User-adaptive proof explanation, Ph.D. thesis, Naturwissenschaftlich-Technische Fakultät I, Universität des Saarlandes, Saarbrücken, Germany, 2001 Nipkow, 2004, Random testing in Isabelle/HOL, 230 A. Ireland, The use of planning critics in mechanizing inductive proofs, in: Logic Programming and Automated Reasoning, 1992, pp. 178–189, citeseer.nj.nec.com/ireland92use.html Meng, 2004, Experiments on supporting interactive proof using resolution, 372 Burstein, 1996, Issues in the development of human-computer mixed-initiative planning, 283 Dixon, 2005, Interactive hierarchical tracing of techniques in IsaPlanner J. Gow, The dynamic creation of induction rules using proof planning, Ph.D. thesis, School of Informatics, University of Edinburgh, 2004 Huet, 1997, The zipper, J. Funct. Programming, 7, 549, 10.1017/S0956796897002864 Aspinall, 2004 Lüth, 1999, TAS and IsaWin: Tools for transformational program development and theorem proving, vol. 1577, 239 Aspinall, 2003, Proof general meets isawin J. van der Hoeven, Gnu texmacs: A free, structured, wysiwyg and technical text editor, in: D. Flipo (Ed.), Le document au XXI-ième siècle, vols. 39–40, Actes du congrès Gutenberg, Metz, 2001, pp. 39–50 van der Hoeven Audebaud, 2003, TexMacs as authoring tool for publication and diffusion of formal developments Amerkad A. Trybulec, Tarski Grothendieck set theory, J. Formal. Math. Axiom D. Syme, Declare: A prototype declarative proof system for higher order logic tech report, comp lab, univ of camb, 1997, citeseer.ist.psu.edu/syme97declare.html C. Benzmüller, L. Cheikhrouhou, D. Fehrer, A. Fiedler, X. Huang, M. Kerber, M. Kohlhase, K. Konrad, A. Meier, E. Melis, W. Schaarschmidt, J.H. Siekmann, V. Sorge, Omega: Towards a mathematical assistant, in: Conference on Automated Deduction, 1997, pp. 252–255 Siekmann, 2003, Proof development in OMEGA: The irrationality of square root of 2, vol. 28, 271 1993 Owre, 1999 Constable, 1986 B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz, L. Kovacs, C. Kocsis, F 1302: THEOREMA: Proving, Solving and Computing in General Domains, in: P. Paule, U. Langer (Eds.), Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 2001–September 2003, Johannes Kepler University Linz, Austria, 2003, pp. 148–170 Coquand Andrews, 2000, System description: Tps: A theorem proving system for type theory, vol. 1831, 164 Andrews, 1996, TPS: A theorem proving system for classical type theory, J. Autom. Reason., 16, 321, 10.1007/BF00252180