Bruno Buchberger

main contributions
refereed publications
unrefereed
books - journals
invited talks
contributed talks
 

 

Unrefereed Technical Reports, Manuscripts, etc.

Copyright: If you download papers, please, respect the copyright of the publishers indicated at the various papers. If no publisher is explicitly mentioned, the copyright is with Bruno Buchberger.

If you download a paper, I would appreciate if you send an e-mail to buchberger@risc.uni-linz.ac.at  with the title of the paper. If you use material from the papers, please, cite them appropriately.

The files with extension .nb are Mathematica notebooks. For reading them you nee Mathematica installed, see Wolfram . For executing the formulae in the input cells in some of the papers, in addition to Mathematica, you need our Theorema system, see Theorema.

2004-08-26-A: Mathematical Knowledge Editor: A Research Plan.
B. Buchberger, K. Nakagawa
SFB Report, 2004, Johannes Kepler University Linz, Spezialforschungsbereich SF013 "Scientific Computing", FWF (Austrain National Science Foundation), 17 pages.



[nb]
2004-06-04-A: Computer-Supported Mathematical Theory Exploration: Schemes, Failing Proof Analysis, and Metaprogramming
B. Buchberger
RISC Technical Report, 4 June, 2004



2004-03-00-A: A Note on Automated Generation of an Algorithm Verification Method
B. Buchberger
SFB Report No. 2004-03, Johannes Kepler University Linz, Spezialforschungsbereich F013, March, 2004, 6 pages.



[pdf]
2003-11-00-A: Groebner Rings in Theorema: A Case Study in Functors and Categories
B. Buchberger
SFB Report No. 2003-49, Johannes Kepler University Linz, Spezialforschungsbereich F013, November, 2003, 68 pages.



[nb]
2003-10-06-C: F 1322: Computer Algebra for Pure and Applied Functional Analysis
B. Buchberger
In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, Johannes Kepler University Linz, Austria, October, 2003, pp.335-364.



2003-10-06-B: F 1302: THEOREMA: Proving, Solving, and Computing in the Theory of Hilbert Spaces
B. Buchberger et al
In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, Johannes Kepler University Linz, Austria, October, 2003, pp. 58-73.



2003-10-06-A: F 1302: Proving, Solving, and Computing in General Domains
B. Buchberger et al
In: 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, October, 2003, pp. 148-170.



2003-10-00-E: Algorithm Retrieval: Concept Clarification and Case Study in Theorema
B. Buchberger
SFB Report No. 2003-44, Johannes Kepler University Linz, Spezialforschungsbereich F013, October, 2003, 14 pages.



[nb]
2003-10-00-D: A Symbolic Algorithm for Solving Two-Point BVPs on the Operator Level
M. Rosenkranz,B. Buchberger, H. W. Engl
SFB Report No.2003-41, Johannes Kepler University Linz, Spezialforschungsbereich F013, October, 2003, 29 pages.



[pdf]
2003-10-00-C: Algorithm Invention and Verification by Lazy Thinking
B. Buchberger
SFB Report No. 2003-29, Johannes Kepler University Linz, Spezialforschungsbereich F013, October, 2003, 21 pages.



[nb]
2003-10-00-B: Origami Theorem Proving
B. Buchberger, T. Ida
SFB Report No. 2003-23, Johannes Kepler University Linz, Spezialforschungsbereich F013, October, 2003, 13 pages.



[pdf]
2003-10-00-A: Focus Windows: A New Approach to Presenting Mathematical Proofs (In Automated Proving Systems)
B. Buchberger
SFB Report No. 2003-22, Johannes Kepler University Linz, Spezialforschungsbereich F013, October, 2003, 20 pages.



[pdf][ps]
2003-08-25-A: Computational Mathematics, Computational Logic and Symbolic Computation.
B. Buchberger
In: M.Baaz, J. A. Makowsky (eds.), Computer Science Logic – Proceedings of 17th International Workshop CSL 2003, 12th Annual Conference of the EACSL, 8th Kurt Gödel Colloqium, KGC 2003, Vienna, Austria, 25-30 August, 2003, Lecture Notes in Computer Science Vol. 2803, pp. 98-99.
ISSN 0302-9743
Copyright: Springer - Verlag Berlin.

[nb]
2003-05-01-B: Preface on Mathematical Knowledge Management.
B. Buchberger, G. Gonnet, M. Hazewinkel.
Special Issue of Annals of Mathematics and Artificial Intelligence, Vol. 38, No. 1-3, May 2003, pp. 1-2.
ISSN 1012-2443
Copyright: Kluwer Academic Publishers, Dordrecht, Netherlands.

[preface.doc]
2002-12-00-C: Invention by Lazy Thinking.
B. Buchberger
In: R. Wagner (ed.), “A Min Tjoa @ Work”- In honor of the 50th birthday of Univ.Prof.Dr. A Min Tjoa, Austrian Computer Society, December 2002, pp. 11-31.
ISBN 3-85403-164-5


2002-12-00-B: Focus Windows: A New Technique for Proof Presentation
F.Piroi, B. Buchberger
SFB Report No. 02-32, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 2002, 5 pages.



[pdf]
2002-12-00-A: Proving the Correctness of the Merge-Sort Algorithm with Theorema
[AC], B. Buchberger
SFB Report No. 02-31, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 2002, 15 pages.



2002-02-25-A: Focus Windows: A New Technique for Proof Presentation
Florina Piroi, B. Buchberger
Proceedings of the 8th Rhine Workshop on Computer Algebra, Mannheim, Germany, March 21-22, (H. Kredel, W. Seiler eds.), 41 pages.


Keywords: automated theorem proving, Theorema, example, implementation, elementary set theory, equivalences
[abstract][pdf]
2002-02-00-A: F 1302: Solving and Proving in General Domains
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, [AC], N. Popov, G. Kusper, M. Rosenkranz
Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Annual Report 2002, Johannes Kepler University Linz, Austria, February, 2002, pp. 4-5.



2001-12-00-C: Two Tools for Mathematical Knowledge Management in Theorema
K. Nakagawa,B. Buchberger
SFB Report No. 01-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 2001, 10 pages.



2001-12-00-B: Presenting Proofs Using Logicographic Symbols
K. Nakagawa,B. Buchberger
SFB Report No. 01-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 2001, 11 pages.



2001-09-26-A: The Role of Logicographic Symbols for Mathematical Knowledge Management.
B. Buchberger, K. Nakagawa
Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM) (B. Buchberger, O. Caprotti eds), RISC-Linz, A-4232 Schloss Hagenberg, September 24-26, 2001.
www.risc.uni-linz.ac.at/institute/conferences/MKM2001/



2001-09-24-A: Mathematical Knowledge Management in THEOREMA.
B. Buchberger
In: B. Buchberger, O. Caprotti (eds.), First International Workshop on Mathematical Knowledge Management (MKM 2001), RISC-Linz, A-4232 Schloss Hagenberg, September 24-26, 2001, 17 pages.



2000-10-06-B: F1302: Proving, Solving, and Computing in the Theory of Hilbert Spaces (Research Proposal)
B. Buchberger et al
Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, Johannes Kepler University Linz, Austria, 6 October, 2000, pp. 54-85.



2000-10-00-C: F 1303: Proving and Solving Over the Reals (Progress Report)
B. Buchberger, J. Schicho
Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, Johannes Kepler University Linz, Austria, October, 2000, pp.126-142.



2000-10-00-B: F 1302: THEOREMA: Proving, Solving, and Computing in General Domains (Progress Report)
B. Buchberger et al
Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, Johannes Kepler University Linz, Austria, October, 2000, pp.101-125.



2000-10-00-A: F 1301: Coordination and Service Project (Progress Report)
B. Buchberger et al
Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, Johannes Kepler University Linz, Austria, October, 2000, pp.88-100.



2000-03-00-B: Annual Report of the SFB F013: 1.11.99-31.12.99
B. Buchberger, U.Langer (eds.)
SFB Report No. 00-06, Johannes Kepler University Linz, Spezialforschungsbereich F013, March, 2000, 45 pages.



2000-01-30-A: Focus Windows: A New Technique for Presenting Mathematical Proofs (in Automated Theorem Proving Systems)
B. Buchberger
Theorema Technical Report, 2000-01-30, Research Institute for Symbolic Computation, Johannes Kepler University, A4040 Linz, Austria, 19 pages.


Keywords: relevant knowledge, didactics of proving, example: correctness of merge sort
[abstract][ps][pdf]
2000-00-00-A: Symbolisches Rechnen: Eliminieren sich die Mathematiker selbst? (Symbolic Computation: Are the Mathematicians Eliminating Their Own Jobs.)
B. Buchberger
Exhibition Catalogue "Mathematische Machinen: Von der Rechenmaschine zum Computer" (F. Pichler ed.), Strom-Museum, Ybbs, Austria, 12 pages.



1999-12-00-E: Mathematik am Computer: Die nächste Überforderung? (Mathematics on the Computer: The Next Overtaxation?)
B. Buchberger
Annual Conference of the Austrian Mathematical Society, Graz, Austria, Sep. 24, 1999. (Available as SFB Report No. 99-39, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999, 16 pages. )



1999-12-00-D: Theory Exploration Versus Theorem Proving
B. Buchberger
SFB Report No. 99-38, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999, 67 pages.



1999-12-00-C: Theorema: A Short Demo
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakawaga, D. Vasaru, W. Windsteiger
SFB Report No. 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999, 61 pages.



1999-12-00-B: Distance Teaching of Mathematics Using Theorema
B. Buchberger, T. Jebelean
SFB Report No. 99-36, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999, 8 pages.



1999-12-00-A: Theorema: A Progress Report
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakawaga, D. Vasaru, W. Windsteiger
SFB Report No. 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999, 11 pages.



1999-04-01-A: Distance Teaching of Mathematics Using Theorema.
B. Buchberger, T. Jebelean
Proceedings of the 3rd Technion Symposium on Software for Communication (H. Gutmann ed.), April 1-3, 1999, Hagenberg, Austria



1999-03-00-A: Annual Report of the SFB F013: 1.4.98-31.12.98
B. Buchberger, U.Langer (eds.)
SFB Report No. 99-02, Johannes Kepler University Linz, Spezialforschungsbereich F013, March, 1999, 32 pages.



1999-00-00-B: Theory Exploration Versus Theorem Proving
B. Buchberger
Proceedings of the Calculemus '99 Workshop, Electronic Notes in Theoretical Computer Science, 23/3, Elsevier, 1999



1998-07-00-B: The Theorema Language: Implementing the Object- and Meta-Level Usage of Symbols
B. Buchberger, W.Windsteiger
SFB Report No. 98-07, Johannes Kepler University Linz, Spezialforschungsbereich F013, July, 1998, 12 pages.



1998-07-00-A: Theorema: An Integrated System for Computation and Deduction in Natural Style
B. Buchberger, K. Aigner, C. Dupre, T. Jebelean, F. Kriftner, M. Marin, K. Nakawaga, O. Podisor, E. Tomuta, Y. Usenko, D. Vasaru, W. Windsteiger
SFB Report No. 98-06, Johannes Kepler University Linz, Spezialforschungsbereich F013, July, 1998, 7 pages.



1998-06-29-E: The Theorema Language: Implemening Object- and Meta-Level Usage of Symbols
B. Buchberger, W.Windsteiger
Proceedings of the Second International Theorema Workshop, RISC, Hagenberg, Austria, 29-30 June, 1998, 11 pages,
RISC-Linz Report Series No. 98-10.



1998-06-29-D: Theorema: Using the Predicate Logic Prover for Proof Training
B. Buchberger, T. Jebelean
Proceedings of the Second International Theorema Workshop, RISC, Hagenberg, Austria, 29-30 June, 1998, 12 pages,
RISC-Linz Report Series No. 98-10.



1998-06-29-C: Theorema: The Current Status
B. Buchberger
Proceedings of the Second International Theorema Workshop, RISC, Hagenberg, Austria, 29-30 June, 1998, 33 pages,
RISC-Linz Report Series No. 98-10.



1998-06-00-B: Theorema: A System for Formal Scientific Training in Natural Language Presentation.
B. Buchberger, T. Jebelean, D.Vasaru
SFB Report No. 98-05, Johannes Kepler University Linz, Spezialforschungsbereich F013, June, 1998, 6 pages.



1998-06-00-A: Theorema: Theorem Proving for the Masses Using Mathematica.
B. Buchberger
Worldwide Mathematica Conference, Chicago, USA, June 20, 1998. (Available as SFB Report No. 98-04, Johannes Kepler University Linz, Spezialforschungsbereich F013, June, 1998, 27 pages.)



1998-04-00-B: Combinig Provers in the Theorema System.
E.Tomuta, B. Buchberger
SFB Report No. 98-01, Johannes Kepler University Linz, Spezialforschungsbereich F013, April, 1998, 14 pages.



1998-00-00-D: Knowledge Web: A Design and Feasibilty Study.
B. Buchberger, T. Ida, W. Schreiner.
Institute of Information Sciences and Electronics, University of Tsukuba. ISE-TR-98-151, 32 pages.



1997-06-09-H: Proving by Simplification
B. Buchberger, M.Marin
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 11 pages.



1997-06-09-G: A Note on Computing Times in Different Programming Styles in Mathematica
B. Buchberger
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 7 pages.



1997-06-09-F: Theorema: The Induction Prover over Lists
B. Buchberger, D.Vasaru
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 12 pages.



1997-06-09-E: Theorema: The Predicate Logic Prover
B. Buchberger, T. Jebelean
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 22 pages.



1997-06-09-D: The Theorema Prover for Equalities over the Natural Numbers
B. Buchberger
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 20 pages.



1997-06-09-C: Theorema: Natural Language and Nested Cells Representation of Proofs
B. Buchberger
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 10 pages.



1997-06-09-B: Theorema: The Language
B. Buchberger, F.Kriftner
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 12 pages.



1997-06-09-A: Theorema: An Overview on the Project and the Proceedings
B. Buchberger
First International Theorema Workshop, RISC, Hagenberg, Austria, June 9-10, 1997, 4 pages.



1996-05-12-A: Mathematiksoftware und Mathematikunterricht: Ein Vorwort (Mathematical Software and Mathematics Teaching: A Preface).
B. Buchberger
Preface in: H.Heugl, W. Klinger, J. Lechner, Matheamatikunterricht mit Computeralgebra-Systemen, Addison-Wesley, Bonn - Reading, pp. 9-13.
ISBN 3-8273-1082-2


1995-09-05-A: Symbolic Computation Software Systems: The Current State of Technology
B. Buchberger
In: Proc. of the EUROSIM 95 Conference, Sept. 5-7, 1995, Vienna, Technical University.



1993-03-00-A: Systolic Multiprecision Arithmetic
B. Buchberger, T. Jebelean
In: Proc. of Impact TEMPUS JEP and Hungarian Transputer Users Group Workshop ``Parallel Processing in Education'', Miskolc, Hungary, March 1993.



1991-07-00-A: Systolic Algorithms in Computer Algebra
B. Buchberger, T. Jebelean
In: Proc. of the NATO ASI on Parallel Processing on Distributed Memory Multiprocessors, Ankara, July 1991.



1991-02-08-A: Speeding-up Quantifier Elimination by Gröbner Bases
B. Buchberger, H.Hong
RISC-Linz Technical Report Nr. 91-06.0, February 1991, 20 pages.



1990-00-00-B: Editorial for Special Issue Computational Algebraic Complexity.
E. Kaltofen, B. Buchberger
Journal of Symbolic Computation (1990) 9, pp. 225-228.
0747-7171/90
Copyright: Academic Press Limited

[pdf]
1988-00-00-A: A Note on Proofs for the Main Theorem in Groebner Bases Theory
B. Buchberger
RISC Technical Report No. 88-34.0, Johannes Kepler University, Linz, Austria.



1985-03-00-C: Symbolic Computation (An Editorial)
B. Buchberger et al.
Journal of Symbolic Computation, Vol. 1, Number 1, 1985, pp. 1-6.
ISSN 0747-7171
Copyright: Academic Press Inc., Harcourt Brace Jovanovich Publishers, London.

[pdf]
1983-10-03-B: Groebner Bases: A Method in Symbolic Mathematics
B. Buchberger
In: Proceedings of "Les Journées de Saint-Etienne: Algorithmique, Calcul Formel, Arithmetique", 3-8 October, 1983, Université de Saint-Etienne, U.E.R de Sciences, pp. II.1-II.10
CAMP Punl.Nr. 83-24.0



1983-00-00-E: A Critical-Pair/Completion Algorithm in Reduction Rings.
B. Buchberger
RISC-Linz Technical Report 83-21, Johannes Kepler University, Linz, Austria, 1983, 62 pages.



[pdf]
1983-00-00-D: Miscellaneous Results on the Gröbner-Bases for Polynomial Ideals II
B. Buchberger
Technical Report 83-1, Department of Computer And Information Sciences, University of Delaware, 1983, 41 pages.



1981-10-00-A: Computer-unterstützter mathematisches Problemlösen: Eine Übersicht (Computer-Aided Mathematical Problem Solving: A Survey)
B. Buchberger
CAMP-LINZ (Computer-Aided Mathematical Problem Solving), Johannes Kepler University, Linz, Austria, Technical Report Camp-Publ.-Nr.: 81-9.0, Lecture Notes, October 1981, 32 pages.



1981-02-00-A: H-bases and Groebner-Bases for Polynomial Ideals
B. Buchberger
CAMP-LINZ (Computer-Aided Mathematical Problem Solving), Johannes Kepler University, Linz, Austria, Camp-Publ.-Nr.: 81-2.0, Internal Report, February, 1981, 14 pages.



1980-02-00-A: Ein Fallstudie in systematischer Algorithmenentwicklung und Algorithmenverifikation: Ein Algorithmus für ein Nimmspiel (A Case Study in Systematic Algorithm Development and Algorithm Verification: An Algorithm for the Game of Nim)
B. Buchberger
Johannes Kepler University, Technisch-Naturwissenschaftliche Fakultät, Institut für Mathematik, Report Nr.162, February, 1980, 38 pages.



1979-07-00-A: A Note on Some Variants of the Notion of Creative Set.
B. Buchberger, R. Neubauer, H. Rolletschek, G. Seeber
Johannes Kepler University, Technisch-Naturwissenschaftliche Fakultät, Insitut für Mathematik, Bericht Nr.139, July, 1979, 18 pages.



1979-06-00-A: Miscellaneous Results on the Construction of Gröbner-Bases for Polynomial Ideals.
B. Buchberger, F. Winkler
Johannes Kepler University, Technisch-Naturwissenschaftliche Fakultät, Insitut für Mathematik, Bericht Nr.137, June, 1979, 86 pages.



1977-03-21-A: Simulation-Universal Automata
B. Buchberger, W. Menzel
Proc. of the Internat. Workshop on Semantics of Programming Languages, Bad Honnef, March 21-25, 1977. Report No.41, Universität Dortmund, Abteilung Informatik, pp. 30-34.



1977-00-00-A: Simulation-Universal Automata
B. Buchberger, W. Menzel
Universität Karlsruhe, Fakultät für Informatik I, Bericht Nr. 14/77, 24 pages.



1976-09-00-A: Eine Bemerkung zu rekursiven Komponenten und 1-1-Splintern (A Remark on Recursive Components and 1-1 Splinters)
B. Buchberger
University of Linz, Institute for Mathematics, September 1976, 9 pages.



1975-11-24-A: Einige Resultate über universelle Automaten (Some Results on Universal Automata)
B. Buchberger
Mathematisches Forschungsinstitut Oberwolfach, Tagunsbericht 46|1975, Automatentheorie und Formale Sprachen, 24-28 november, 1975, pp. 6-7.



1975-11-00-A: Some Results on Universal Automata and Input/Output Codings
B. Buchberger
Hochschule Linz, Technische-Naturwissenschaftliche Fakultät, Institut für Mathematik, Bericht Nr. 34, November, 1975, 35 pages.



1973-11-00-A: Implementierung einer Metasprache zur Definition von Programmiersprachen (Implementation of a Meta-language for the Definition of Programming Languages)
B. Buchberger, F. Jenewein
Institut für Informatik und Numerische Mathematik, Universität Innsbruck, Programmbibliothek Nr.228 (ZUSE Z 23V), November 1973, 36 pages.



1973-00-00-B: On Certain Decompositions of Goedel Numberings
B. Buchberger
Institut für Informatik, Universität Innsbruck, 1973, 23 pages. (Appeared in Archiv für Mathematische Logik und Grundlagenforschung.)



1972-12-00-A: A Study on Universal Functions
B. Buchberger, B.Roider
Institut für Numersiche Mathematik und Elektronische Informationsverarbeitung Universität Innsbruck, Bericht Nr. 72-5, December 1972, 31 pages.



1972-02-00-A: A Basic Problem in the Thoery of Programming Languages
B. Buchberger
Institut für Numersiche Mathematik und Elektronische Informationsverarbeitung Universität Innsbruck, Bericht Nr. 72-1, Februar 1972, 40 pages.



[pdf]
1971-08-00-A: A Comment on Blum's Signal Function
B. Buchberger
Institut für Numerische Mathematik und Elektronische Informationsverarbeitung Universität Innsbruck, Bericht Nr. 71-3, August 1971, 7 pages.



[pdf]
1969-10-06-A: Grundbegriffe der Algorithmentheorie (Basic Notions of Algorithm Theory)
B. Buchberger
Steiermärkisches Mathematisches Symposium, Grottenhof-Hardt, 6-9 October, 1969, Technical Report, Angewandte Mathematik, Universität und Technische Hochschule Graz, 31 pages.



[pdf]
1965-00-00-A: Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal)
B. Buchberger
PhD Thesis, Mathematical Institute, University of Innsbruck, Austria, 1965. (English translation to appear in Journal of Symbolic Computation, 2004)
[pdf]