RISC Publications and Technical Reports of Wolfgang Windsteiger
2022
W. Windsteiger.Learning to Reason Assisted by Automated Reasoning. In: Intelligent Computer Mathematics: 15th International Conference, K. Buzzard and T. Kutsia (ed.), Proceedings of CICM 2022, Lecture Notes in Artificial Intelligence LNAI13467, pp. 305-320.2022.Springer,ISBN 978-3-031-16681-5.[doi][pdf][bib]
2021
W. Windsteiger.Automated Theorem Proving in the Classroom. In: Proceedings Automated Deduction in Geometry (ADG 2021), Predrag Janicic (ed.), Proceedings of Automated Deduction in Geometry (ADG 2021), Electronic Proceedings in Theoretical Computer Science (EPTCS)352, pp. 54-63.2021.ISSN 2075-2180.Extended abstract.[doi][pdf][bib]
W. Windsteiger.Automated Theorem Proving in the Classroom. Technical report no. 21-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2021.Extended version of keynote talk at ADG 2021 conference. Licensed under CC BY 4.0 International.[doi][pdf][bib]
2020
David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere.Computational Logic in the First Semester of Computer Science: An Experience Report. In: Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU, Springer (ed.), Proceedings of CSEDU, pp. 374-381.2020.978-989-758-417-6.[doi][bib]
David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere.Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App. In: ITICSE 2020, ACM (ed.), Proceedings of ITICSE, pp. 61-67.2020.9781450368742.[doi][bib]
2017
A. Maletzky, W. Windsteiger.The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema. In: Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke (ed.), Lecture Notes in Computer Science10383, pp. 25-39.2017.Springer,ISBN 978-3-319-62075-6.doi 10.1007/978-3-319-62075-6_3.[url][pdf][bib]
W. Windsteiger.Theorema 2.0: A Brief Tutorial. In: Proceedings of SYNASC 2017, Tudor Jebelean and Daniela Zaharie (ed.), Proceedings of SYNASC 2017, IEEE Explore, pp. 1-3.2017.ISBN 978-1-5386-2626-9.[doi][pdf][bib]
2016
Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger.Theorema 2.0: Computer-Assisted Natural-Style Mathematics.JFR9(1), pp. 149-185.2016.ISSN 1972-5787.[doi][bib]
2014
W. Windsteiger.Theorema 2.0: A System for Mathematical Theory Exploration. In: Proceedings International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-8, 2014, Chee Yap and Hoon Hong (ed.), Proceedings of International Congress on Mathematical Software (ICMS'2014), Lecture Notes in Computer Science (LNCS)8592, pp. 49-52.2014.ISBN 978-3-662-44198-5.[url][pdf][bib]
2013
Manfred Kerber, Christoph Lange, Colin Rowat and Wolfgang Windsteiger.Developing an Auction Theory Toolbox. In: AISB 2013, Manfred Kerber, Christoph Lange, Colin Rowat (ed.), pp. 1-4.2013.no ISSN.proceedings available online.[url][pdf][bib]
Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger.A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. In: Conference on Intelligent Computer Mathematics (CICM 2013), Jacques Carette (ed.), Lecture Notes in Artificial Intelligence (LNAI)7961, pp. 200-215.2013.Springer,ISBN 978-3-642-39319-8.[pdf][bib]
2012
Ph. Kügler, W. Windsteiger.Algorithmische Methoden - Funktionen, Matrizen, Multivariate Polynome.Reihe: Mathematik kompakt.1st edition,May2012.Birkhäuser Basel Boston Berlin,ISBN 978-3-7643-8515-6.[url][bib]
W. Windsteiger.Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System. In: 24th OpenMath Workshop, 7th Workshop on Mathematical User Interfaces (MathUI), and Intelligent Computer Mathematics Work in Progress, James Davenport and Johan Jeuring and Christoph Lange and Paul Libbrecht (ed.), CEUR Workshop Proceedings921, pp. 73-81.2012.Aachen,1613-0073.[url][pdf][bib]
W. Windsteiger.Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System. In: Proceedings 10th International Workshop On User Interfaces for Theorem Provers, Bremen, Germany, July 11th 2012, Cezary Kaliszyk and Christoph Lüth (ed.), Proceedings of UITP 2012, Electronic Proceedings in Theoretical Computer Science118, pp. 72-82.2012.Open Publishing Association,ISBN 2075-2180 (ISSN).doi: 10.4204/EPTCS.118.5.[url][bib]
2011
Manfred Kerber, Colin Rowat, and Wolfgang Windsteiger.Using Theorema in the Formalization of Theoretical Economics. In: Intelligent Computer Mathematics, James H. Davenport, William M. Farmer, Florian Rabe, Josef Urban (ed.), Proceedings of CICM 2011, Lecture Notes in Artificial Intelligence (LNAI)6824, pp. 58-73.2011.Springer,ISSN 0302-9743.[doi][pdf][bib]
2009
Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger.Automated Reasoning. In: Hagenberg Research, B. Buchberger, M. Affenzeller, A. Ferscha, M. Haller, T. Jebelean, E.P. Klement, P. Paule, G. Pomberger, W. Schreiner, R. Stubenrauch, R. Wagner, G. Weiss, W. Windsteiger (ed.), pp. 63-101.2009.Springer Dordrecht Heidelberg London New York,ISBN 978-3-642-02126-8.[url][bib]
2008
W. Windsteiger.Stimulating Students' Creativity Through Computer-Supported Experiments and Automated Theorem Proving. In: Promoting Creativity for all Students in Mathematics Education, Emiliya Velikova, Agnis Andzans (ed.), pp. 351-357.2008.8 Studentska Str., 7017 Rousse, Bulgaria,University of Rousse, Bulgaria,ISBN 978-954-712-420-2.Proceedings of Discussion Group 9, the 11th International Congress on Mathematical Education (ICME 11).[pdf][bib]
Ph. Kügler, W. Windsteiger.Algorithmische Methoden - Zahlen, Vektoren, Polynome.Reihe: Mathematik kompakt.1st edition,December2008.Birkhäuser Basel Boston Berlin,ISBN: 978-3-7643-8434-0.[url][bib]
2007
G. Mayrhofer, S. Saminger, W. Windsteiger.CreaComp: Computer-Supported Experiments and Automated Proving in Learning and Teaching Mathematics. In: Proceedings of ICTMT8, Eva Milkova (ed.), pp. ?-?.2007.ISBN 978-80-7041-285-5.[pdf][bib]
G. Mayrhofer, S. Saminger, W. Windsteiger.CreaComp: Experimental Formal Mathematics for the Classroom. In: Symbolic Computation and Education, Shangzhi Li, Dongming Wang, and Jing-Zhong Zhang (ed.), pp. 94-114.2007.World Scientific Publishing Co.,Singapore, New Jersey,ISBN 978-981-277-599-3.[url][pdf][bib]
Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger.Calculemus/MKM 2007 - Work in Progress. Technical report no. 07-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2007.[ps][pdf][bib]
2006
W. Windsteiger.An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema.JSC41(3-4), pp. 435-470.2006.Elsevier,ISSN 0747-7171.[url][pdf][bib]
B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, W. Windsteiger.Theorema: Towards Computer-Aided Mathematical Theory Exploration.Journal of Applied Logic4(4), pp. 470-504.2006.ISSN 1570-8683.[doi][pdf][bib]
W. Windsteiger, B. Buchberger, M. Rosenkranz.Theorema. In: The Seventeen Provers of the World, Freek Wiedijk (ed.), Lecture Notes in Artificial Intelligence (LNAI)3600, pp. 96-107.2006.Springer Berlin Heidelberg New York,ISBN 3-540-30704-4.[url][pdf][bib]
E. M. Clarke, A. S. Gavlovski, K. Sutner, W. Windsteiger.Analytica V: Towards the Mordell-Weil Theorem. In: Proceedings of Calculemus'06, A. Bigatti, S. Ranise (ed.), Proceedings of Calculemus'06, pp. ?-?.2006.[pdf][bib]
B. Buchberger, E.P. Klement, G. Pilz, S. Saminger, W. Windsteiger.CreaComp: e-Schulung von Kreativität und Problemlösekompetenz. Technical report no. 06-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2006.[pdf][bib]
2005
W. Windsteiger.Wie erfinde ich mathematische Algorithmen? Wie beweise ich mathematische Algorithmen?. Technical report no. 05-18 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2005.Presentation slides for a presentation given at Schwerpunktfach Mathematik, Europagymnasium Auhof, December 15, 2005.[nb][pdf][bib]
2003
W. Windsteiger.Mathematica. In: Computer Algebra Handbook: Foundations, Applications, Systems, J. Grabmeier, E. Kaltofen, and V. Weispfenning (ed.), pp. 314-320.2003.Springer,ISBN 3-540-65466-6.[bib]
W. Windsteiger.Exploring an Algorithm for Polynomial Interpolation in the Theorema System. In: Proceedings of the Calculemus 2003 Symposium, T. Hardin and R. Rioboo (ed.), pp. 130-136.September2003.Aracne Editrice S.R.L.,Rome Italy,ISBN 88-7999-545-6.[pdf][bib]
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 the Theory of Hilbert Spaces. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, P. Paule, U. Langer (ed.), pp. 58-73.October2003.Johannes Kepler University Linz, Austria,-.[bib]
2002
W. Windsteiger.An Automated Prover for Set Theory in Theorema. In: Calculemus 2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning: Work in Progress Papers, O. Caprotti, V. Sorge (ed.), pp. 56-67.June2002.Marseille, France,ISSN 14274447.Appears in Seki-Report Series Nr. SR-02-04, Universitaet des Saarlandes.[ps][bib]
W. Windsteiger.An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema. In: Logic, Mathematics and Computer Science: Interactions (LMCS 2002), K. Nakagawa (ed.), pp. 266-280.October2002.RISC, Schloss Hagenberg, Austria,ISBN 3-902276-03-7.Symposium in Honor of Bruno Buchberger's 60th Birthday, Appears in RISC-report Series Nr. 02-60.[pdf][bib]
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz.F 1302: Solving and Proving in General Domains. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Annual Report 2002, U. Langer, F. Winkler (ed.), pp. 4-5.February2002.Johannes Kepler University Linz, Austria,[bib]
2001
W. Windsteiger.A Set Theory Prover in Theorema. In: Computer Aided Systems Theory, R. Moreno-Diaz and B. Buchberger and J.L. Freire (ed.), LNCS2178, pp. 525-539.2001.Springer,ISSN 0302-9743, ISBN 3-540-429.Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), extended version available as RISC report 01-07.[bib]
W. Windsteiger.On a Solution of the Mutilated Checkerboard Problem using the Theorema Set Theory Prover. In: Proceedings of the Calculemus 2001 Symposium, S. Linton and R. Sebastiani (ed.), pp. 28-47.2001.[pdf][bib]
Wolfgang Windsteiger.A Set Theory Prover in Theorema: Implementation and Practical Applications. RISC Institute. PhD Thesis.May2001.[tar.gz][bib]
Wolfgang Windsteiger.Theorema: Ein Rahmen fuer Mathematik, Algorithmik und Didaktik. Technical report no. 01-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2001.Course for mathematics teachers given in the frame of the ``Tag der Mathematik 2001'' at the University of Linz, November 23, 2001. In German.[ps][tar.gz][bib]
Wolfgang Windsteiger.A Set Theory Prover within Theorema. Technical report no. 01-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2001.Also available as SFB report 01-23.[ps][bib]
2000
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger.The Theorema Project: A Progress Report. In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), M. Kerber, M. Kohlhase (ed.), pp. 98-113.6-7 August2000.Copyright: A.K. Peters, Natick, Massachusetts,St. Andrews, Scotland,ISBN 1-56881-145-4.[ps][pdf][abstract][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Theorema System: Proving, Solving, and Computing for the Working Mathematician. Technical report no. 00-38 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Natural Style Provers of Theorema: A Survey of Strategies for Different Mathematical Domains. Technical report no. 00-39 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Facilities of Theorema for Teaching Logic and Mathematics. Technical report no. 00-41 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
1999
Windsteiger W..Building Up Hierarchical Mathematical Domains Using Functors in THEOREMA. In: Electronic Notes in Theoretical Computer Science, A. Armando and T. Jebelean (ed.), Proceedings of Calculemus'99, Trento, Italy, ENTCS23/3, pp. 401-419.1999.Elsevier,ISSN: 1571-0661.[url][pdf][bib]
Wolfgang Windsteiger.Theorema: Overview on Using the System and Details on Composing Hierarchical Knowledge Bases. Technical report no. 99-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1999.Presented at the Edinburgh School in Logic and Computation.[tar.gz][bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Progress Report. Technical report no. 99-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[ps][bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Short Demo. Technical report no. 99-45 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[tar.gz][bib]
1998
B. Buchberger, W. Windsteiger.The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols. SFB F013 Numerical and Symbolic Scientific Computing. Technical report no. 98-07, 1998.[pdf][bib]
Bruno Buchberger, Klaus Aigner, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Mircea Marin, Koji Nakagawa, Ovidiu Podisor, Elena Tomuta, Yaroslav Usenko, Daniela Vasaru, Wolfgang Windsteiger.Theorema: An Integrated System for Computation and Deduction in Natural Style. Technical report no. 98-25 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1998.Also available as SFB Report No. 98-06.[ps][bib]
B. Buchberger, W.Windsteiger.The Theorema Language: Implemening Object- and Meta-Level Usage of Symbols. In: Proceedings of the Second International Theorema Workshop, B. Buchberger, T. Jebelean (ed.), pp. -.June 29-301998.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 98-10.[bib]
1993
Windsteiger W..GRÖBNER-IO: An Input/Output Libray for GRÖBNER. University of Linz, RISC Institute. Technical report no. ??, 1993.[bib]
Wolfgang Windsteiger, Bruno Buchberger.GRÖBNER: A Library for Computing Gröbner Bases based on SACLIB. Technical report no. 93-72 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1993.[ps][bib]
Wolfgang Windsteiger.Using GRÖBNER as a "Black Box". Technical report no. 93-71 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1993.[ps][bib]
1992
Windsteiger W..Gröbner Bases: A Characterization by Syzygy Completeness and an Implementation. University of Linz, RISC Institute. Diploma Thesis.January1992.[ps][bib]
Wolfgang Windsteiger.Gröbner Bases: A Characterization by Syzygy Completeness and an Implementation. Technical report no. 92-20 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1992.Diploma Thesis.[bib]
1990
Wolfgang Windsteiger.An Implementation of Rational Functions in PCL. Technical report no. 90-56 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1990.[ps][bib]
Wolfgang Windsteiger.An Approach to Object-Oriented Programming in C. Technical report no. 90-57 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1990.[ps][bib]
