Publications of the Project F1302

September 27, 2008

September 27, 2008

## Bibliography

- 1
- H. Anai, K. Horimoto, and T. Kutsia, 2007.
- 2
- H. Anai, K. Horimoto, and T. Kutsia,
editors.

*Algebraic Biology*, volume 4545 of*Lecture Notes in Computer Science*. Springer, 2007. - 3
- A. Armando and T. Jebelean, editors.

*Calculemus 99: International Workshop on Combining Proving and Computation*. Electronic Notes in Theoretical Computer Science,`http://www.elsevier.nl/locate/entcs`, July 1999.

Trento, Italy - by CADE 99. - 4
- A. Armando and T. Jebelean, editors.

*Calculemus: Integrating Computation and Deduction*, volume 32 of*Special Issue of Journal of Symbolic Computation*, 2001.

ISSN 0747-7171. - 5
- A. Asperti, B. Buchberger, and J. H.
Davenport, editors.

*MKM 2003: Mathematical Knowledge Management*. Springer, February 2003.

Bertinoro, Italy. - 6
- B. Beckert, M. Giese, R. Hähnle,
V. Klebanov, P. Rümmer, S. Schlager,
and P. H. Schmitt.

The key system 1.0 (deduction component).

In F. Pfenning, editor,*Proceedings, International Conference on Automated Deduction, Bremen, Germany*, volume 4603 of*LNCS*, pages 1-6. Springer, 2007. - 7
- C. Benzmueller and W. Windsteiger.

Computer-supported mathematical theory development.

Technical Report 04-14, RISC Report Series, University of Linz, Austria, July 2004.

ISBN 3-902276-04-5. - 8
- C. Benzmüller and W. Windsteiger,
editors.

*Computer-Supported Mathematical Theory Development*, University College Cork, Ireland, July 2004.

In the frame of IJCAR'04. - 9
- B. Buchberger.

Computer Support for Inventing Gröbner Bases Theory.

IMACS Conference, Prague, Czech Republic, 1998. - 10
- B. Buchberger.

Intensive Course on Gröbner Bases (30 hours).

Universitad de Oriente, Santiago, Cuba, 1998. - 11
- B. Buchberger.

Symbolic Computation: Ein überblick.

Universität Hamburg, Institut für Informatik, 1998. - 12
- B. Buchberger.

Theorema: Automatisches Beweisen für Lehre und Forschung.

Universität Leipzig, Mathematisches Institut, 1998. - 13
- B. Buchberger.

Theorema: Computer-Supported Mathematical Proving.

Annual Meeting of the Mathematics Department of the University of Wales, UK, 1998. - 14
- B. Buchberger.

Theorema: Computer-Unterstuetztes mathematisches Beweisen, 1998-4-24.

Universität Karlsruhe, Institut für Informatik, 1998. - 15
- B. Buchberger.

The Theorema Project.

Universidad de Oriente, Santiogo, Cuba, 1998. - 16
- B. Buchberger.

The Theorema Project: An Introduction.

Research Institute IRST, Trento, 1998-2-19, 1998. - 17
- B. Buchberger.

Theorema: The Current Status.

In B. Buchberger and T. Jebelean, editors,*Proceedings of the Second International Theorema Workshop*, pages 5-37, 1998.

RISC report 98-10. - 18
- B. Buchberger.

Theorema: Theorem Proving for the Masses Using Mathematica (invited keynote).

Worldwide Mathematica Conference, Chicago, USA, 1998. - 19
- B. Buchberger.

Can Computer Replace Mathematicians?

Symposium ``Symbolic Computation'', TU Wien, April 1999. - 20
- B. Buchberger.

Computer-Mathematik in der Schule.

Schulung für AHS-Lehrer, RISC, Hagenberg, Austria, December 1999. - 21
- B. Buchberger.

Gröbner Basen: Die ersten Jahren.

Colloquium ``100. Geburtstag von Wolfgang Gröbner'', Universität Innsbruck, May 1999. - 22
- B. Buchberger.

Gröbner bases: Theory and applications.

University of Timisoara, Romania, April 1999. - 23
- B. Buchberger.

*Theorema*: A System for Supporting Mathematical Proving.

North Carolina State University, Department of Mathematics, USA, October 1999. - 24
- B. Buchberger.

*Theorema*: A System for Supporting Mathematical Proving.

University of Illinois at Urbana-Champaign, Department of Mathematics, USA, October 1999. - 25
- B. Buchberger.

The*Theorema*project: The current state.

Mathematica Developer's Conference, Wolfram Research International, Urbana-Champaign, USA, October 1999. - 26
- B. Buchberger.

Mathematics: The technology of reasoning.

Invited Keynote at the 4th Asian Technology Conference in Mathematics, Guangzhou, China, December 1999. - 27
- B. Buchberger.

Mathematik: Altes Eisen oder Schlüsseltechnologie?

Fortbildungsseminar für ``European Women in Management'', RISC, Hagenberg, Austria, October 1999. - 28
- B. Buchberger.

Mathematik am Computer: Die nächste Überforderung?

Lehrerfortbildungsseminar bei der ÖMG-Tagung, Graz, Austria, September 1999. - 29
- B. Buchberger.

Möglichkeiten und Grenzen mathematischer Modellierung.

Sommerakademie der Pro Scientia ueber ``Modell und Wirklichkeit'', Tainach, Kärnten, Austria, September 1999. - 30
- B. Buchberger.

*Theorema*: A new kind of mathematical system.

University of Timisoara, Romania, April 1999. - 31
- B. Buchberger.

*Theorema*: A new kind of mathematical system.

University of Cluj-Napoca, April 1999. - 32
- B. Buchberger.

*Theorema*: A new kind of mathematical system.

University of Debrecen, Hungary, May 1999. - 33
- B. Buchberger.

*Theorema*: A new kind of mathematical system.

Invited Keynote at the COCOA Conference, Torino, Italy, June 1999. - 34
- B. Buchberger.

*Theorema*: A progress report.

GMD Bonn, Institut für Algorithmen, Bonn, Germany, June 1999. - 35
- B. Buchberger.

*Theorema*: A proving system based on*Mathematica*.

International Symposium on Symbolic and Numeric Scientific Computing, RISC, Hagenberg, Austria, August 1999. - 36
- B. Buchberger.

*Theorema*: A proving system based on*Mathematica*.

International Mathematica Symposium 1999, RISC, Hagenberg, Austria, August 1999. - 37
- B. Buchberger.

*Theorema*a system for supporting mathematical proving.

Canergie Mellon University, Department of Mathematics, Pittsburgh, USA, October 1999. - 38
- B. Buchberger.

*Theorema*: A system for supporting mathematical proving.

Workshop of the Japanese Consortium on Formal Methods, Nagoya, Japan, December 1999. - 39
- B. Buchberger.

Theory exploration versus theorem proving.

In A. Armando and T. Jebelean, editors,*Electronic Notes in Theoretical Computer Science*, volume 23. Elsevier, 1999.

CALCULEMUS Workshop, University of Trento, Trento, Italy. - 40
- B. Buchberger.

Towards algorithm verification in*Theorema*.

Workshop on Validated Software, Schloss Dagsthul, Germany, November 1999. - 41
- B. Buchberger.

Views on the future of computer science.

Invited Keynote at the Workshop of the Japanese Consortium on Formal Methods, Nagoya, Japan, December 1999. - 42
- B. Buchberger.

Automated Theorem Proving: Theory or Practice?

*Mitteilungen der Deutschen Mathematiker-Vereinigung*, 2, 2000. - 43
- B. Buchberger.

Computer Algebra: The End of Mathematics?

Freie Universität Berlin, Germany, May 2000. - 44
- B. Buchberger.

Gröbner Bases and Automated Theorem Proving.

Intensive Course at the University of Texas at Beaumont, March 2000. - 45
- B. Buchberger.

*Theorema*: Beyond Computer Algebra.

University of Texas at Beaumont, February 2000. - 46
- B. Buchberger.

Mathematica and computer science: A personal view.

In T. Jebelean and V. Negru, editors,*Proceedings of the Second International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, (SYNASC'00), Timisoara, Romania*, October 2000. - 47
- B. Buchberger.

Mathematics and computer science - a personal view.

*An. Mat. Univ. Timisoara*, 24(1):3-18, 2000.

ISSN 1224-970X. - 48
- B. Buchberger.

Mathematik am Computer: Die nächste Überforderung? (Mathematics on the Computer: The Next Overtaxation?).

*Didaktikreihe der österreichischen mathematischen Gesellschaft*, 131:37-56, March 2000. - 49
- B. Buchberger.

Theorem proving: Theory or practice.

Jahrestagung der DMV, Dresden, September 18-22, 2000. - 50
- B. Buchberger.

Theorema: Automatisches beweisen für die praxis.

Universität Salzburg, Institut für Mathematik, June 15, 2000. - 51
- B. Buchberger.

The Theorema project: Logic and algebra.

Workshop on Computer Algebra and Representation Theory, Universität Bielefeld, Fakultät für Mathematik, September 25-27, 2000. - 52
- B. Buchberger.

Theorema Proving For and With Gröbner Bases.

In K. Galkowski and E. Rogers, editors,*Proceedings of the Second International Workshop on Multidimensional (nD) Systems, June 27-30, Czocha Castle, Poland*, pages 15-22, 2000. - 53
- B. Buchberger.

Theorema Proving For and With Gröbner Bases.

Second International Workshop on Multidimensional (nD) Systems, Czocha Castle, Poland, June 27-30, 2000. - 54
- B. Buchberger.

Theory exploration with Theorema.

In T. Jebelean and V. Negru, editors,*Proceedings of the Second International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'00), Timisoara, Romania*, October 2000. - 55
- B. Buchberger.

The vertical layers in mathematics.

Workshop on Computer Algebra and Representation Theory, Universität Bielefeld, Fakultät für Mathematik, September 25-27, 2000. - 56
- B. Buchberger.

Gröbner Bases: A Short Introduction for Systems Theorists.

In R. Moreno-Diaz, B. Buchberger, and J. L. Freire, editors,*EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science)*, number 2201 in Lecture Notes in Computer Science, pages 1-19, Las Palmas de Gran Canaria, February 19-23 2001. Springer.

ISSN 0302-9743, ISBN 3-540-42959-X. - 57
- B. Buchberger.

Gröbner bases and systems theory.

*Journal of Multidimensional Systems and Signal Processing*, 12(3-4):223-251, 2001. - 58
- B. Buchberger.

Gröbner bases and Theorema.

Workshop Universal Algebra, Universität Linz, June 2001. - 59
- B. Buchberger.

Gröbner rings and modules.

3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), University of the West, Timisoara, Romania, October 2001. - 60
- B. Buchberger.

Logicographic symbols: A new feature in Theorema.

In*Symbolic Computation - New Horizons (Proceedings of the 4th International Mathematica Symposium)*, pages 23-30, Tokyo Denki University, Chiba Campus, Japan, June 25 - 27 2001. Tokyo Denki University Press.

ISBN 4-501-73020-X C3041. - 61
- B. Buchberger.

The PCS prover in Theorema.

In Moreno-Diaz et al. [371], pages 469-478.

ISSN 0302-9743, ISBN 3-540-42959-X. - 62
- B. Buchberger.

Schichten in der automatisierung der mathematik.

Workshop ``Symbolic Computation'', Technische Universität Wien, Institut für Simulation, January 2001. - 63
- B. Buchberger.

Theorema: A short introduction.

*Mathematica Journal*, 8(2):247-252, 2001.

ISSN 1047-5974. - 64
- B. Buchberger.

Theorema: Automated theorem proving for the practice.

Applied Informatics Conference, University of Eger, Ungarn, January 2001. - 65
- B. Buchberger.

Theorema: Extending Mathematica by automated proving.

In D. Bosanac and D. Ungar, editors,*PrimMath 2001 (The Programming System Mathematica in Science, Technology, and Education)*, pages 10-11. University of Zagreb, September 27-28 2001.

ISBN 953-6076-71-3. - 66
- B. Buchberger.

Theorema: Proving, solving and computing.

International Symposium ``Proving, Solving, Computing'' on the Occasion of the 60th Birthday of Professor S. Igarashi, Tsukuba University, June 2001. - 67
- B. Buchberger.

Automated Proofs of Automated Geometry Provers.

Invited talk at Forth International Workshop on Automated Deduction in Geometry, RISC, Schloss Hagenberg, Austria, September 5-7 2002. - 68
- B. Buchberger.

Computer-Algebra: Abstieg oder Aufstieg? (Computer Algebra: Descent or Ascent ?).

Invited colloquium talk at IWR (Institut für Wissenschaftliches Rechnen), Heidelberg, Germany, May 23 2002. - 69
- B. Buchberger.

Computer Mathematik: Abstieg oder Aufstieg (Computer Mathematics: Descent or Ascent).

Invited colloquium talk at Fachhochschule Ohm, Mathematical Department, Nürnberg, Germany, December 12 2002. - 70
- B. Buchberger.

Computer verstehen und benutzen (Understanding and Using Computers).

Invited colloquium talk at Workshop of the Austrian Christian Teachers Association, at RISC, Schloss Hagenberg, Austria, March 13 2002. - 71
- B. Buchberger.

Focus Windows: A New Technique for Proof Presentation.

Invited talk at 2nd Workshop on Proving, Solving, Computing, Tokyo, organized by the SCORE Group, University of Tsukuba, Japan, February 17-18 2002. - 72
- B. Buchberger.

Formal exploration management for Hilbert space theory.

Talk at the SFB Statusseminar, Strobl, Austria, April 2002. - 73
- B. Buchberger.

Formal Theory Exploration:The Lazy Thinking Paradigm.

Contributed talk at Calculemus Meeting, Pisa, Italy, September 16 2002. - 74
- B. Buchberger.

Forschung: Das Standortkriterium. Erfahrungen, Reflexionen, Visionen. (Research: A Decisive Criterion for Selecting Industrial Sites.).

Invited colloquium talk at ``Innovationsgespraeche'', Profactor Institute, Steyr, Austria, March 19 2002. - 75
- B. Buchberger.

Gröbner Bases: Applications.

In A. V. Mikhalev and G. F. Pilz, editors,*The Concise Handbook of Algebra*, pages 265-268. Kluwer Academic Publishers, Dordrecht, Netherlands., 2002. - 76
- B. Buchberger.

Gröbner Bases: The Commutative Case.

In A. V. Mikhalev and G. F. Pilz, editors,*The Concise Handbook of Algebra*, pages 262-265. Copyright: Kluwer Academic Publishers, Dordrecht, Netherlands, 2002. - 77
- B. Buchberger.

Invention by Lazy Thinking.

In R. Wagner, editor,*``A Min Tjoa @ Work''- In honor of the 50th birthday of Univ.Prof.Dr. A Min Tjoa*, pages 11-31. Austrian Computer Society, December 2002. - 78
- B. Buchberger.

Logic, Mathematics, Computer Science: The Accumulated Thinking Technology of Mankind.

Contributed talk at Conference on Logic, Mathematics and Computer Science (LMCS 2002), Symposium in Honor of Bruno Buchberger's 60th Birthday, RISC, Hagenberg, Austria, October 20-22 2002. - 79
- B. Buchberger.

Symbolic Computation.

In G. Pomberger and P. Rechenberg, editors,*Handbuch der Informatik*, 1st edition, pages 955-974. Carl Hanser Verlag Munich, 2002.

(3rd edition, pp. 963-981). - 80
- B. Buchberger.

Teaching Without Teachers?

Invited talk at VISIT-ME (Vienna International Symposium on Information Technology in Math Education), University of Vienna,`http://www.acdca.ac.at/visit-me-2002/`, July 10-13 2002. - 81
- B. Buchberger.

Theorema: A Formal Frame for Mathematics.

Invited talk at EACA - 2002, Octavo Encuentro de Algebra Computational y Applicaciones, Penaranda de Duero, Universidad de Vallodolid, pp. 11-32, September 9-11 2002. - 82
- B. Buchberger.

Theorema and Mathematical Knowledge Management.

Invited talk at IMA 2002 Summer Program: Special Functions in the Digital Age, University of Minnesota, Minneapolis, USA, July 22 - August 2 2002. - 83
- B. Buchberger.

Algorithm invention and verification by lazy thinking.

October 2003. - 84
- B. Buchberger.

Algorithm Invention and Verification by Lazy Thinking.

*Analele Universitatii din Timisoara, Seria Matematica - Informatica*, XLI:41-70, 2003.

special issue on Computer Science - Proceedings of SYNASC'03. - 85
- B. Buchberger.

Algorithm Invention and Verification by Lazy Thinking.

Invited colloquium talk at Department of Computer Science, Lamar University, Texas, USA, November 19 2003. - 86
- B. Buchberger.

Algorithm Synthesis by Failing Correctness Proofs.

Invited colloquium talk at Mathematisches Institut, Universität München, December 5 2003. - 87
- B. Buchberger.

Automated computing, solving, proving: A key to the information age.

Talk in Computer Science Department, University of Tsukuba, Japan, February 2003. - 88
- B. Buchberger.

Automated Proving, Solving, Computing: A Key to the Information Age.

Invited talk at Presentation Day of the Computer Science Department of the University of Tsukuba, Japan, February 24 2003. - 89
- B. Buchberger.

Computational mathematics, computational logic, and symbolic computation.

Talk in Technical University of Vienna, Computer Science Department, August 2003. - 90
- B. Buchberger.

Humanistische Bildung versus Learning on Demand (Humanistic Education versus Learning on Demand).

Invited talk at Conference eSchola 2003, Pädagogische Akademie, Linz, Austria, May 9 2003. - 91
- B. Buchberger.

Mathematik an Fachhochschulen: Fachliche und didaktische Überlegungen.

Tagung der Mathematiklehrer an Fachhochschulen, Bozen, Italy, September 2003. - 92
- B. Buchberger.

Mathematik und Informatik: Eine Liebeserklärung.

Talk in Tagung der österreichischen mathematischen Gesellschaft, Bozen, Italy, September 2003. - 93
- B. Buchberger.

Systematic Theory Exploration: The Lazy Thinking Paradigm.

Invited colloquium talk at Mathematics Department, University of Kyushu, Fukuoka, Japan, March 7 2003. - 94
- B. Buchberger.

Systematic Theory Exploration: The Lazy Thinking Paradigm.

Invited talk at Workshop on Computer Algebra, Research Institute of Mathematical Science, Kyoto, Japan, March 5 2003. - 95
- B. Buchberger.

The White-Box and Black-Box Usage of Mathematical Software Systems.

Invited talk at Symposium Mathematics and New Technologies: What do Learn, How to Teach?, Universidad Complutense de Madrid, Fondacion Ramon Areces, December 10-11 2003. - 96
- B. Buchberger.

Verified algorithm development by lazy thinking.

Talk in Kyushu University, Mathematical Department, Fukuoka, Japan, March 2003. - 97
- B. Buchberger.

Verified algorithm development by lazy thinking.

Talk in Research Institute for Mathematical Sciences, Mathematical Department, University of Kyoto, Japan, February 2003. - 98
- B. Buchberger.

Verified Algorithm Development by Lazy Thinking.

Talk in IMS 2003 (International Mathematica Symposium 2003, Imperial College, London, UK, July 2003. - 99
- B. Buchberger.

Verified Algorithm Development by Lazy Thinking.

Invited talk at International Mathematica Symposium 2003, Imperial College, London, July 7-11 2003. - 100
- B. Buchberger.

Algorithm supported mathematical theory exploration.

(Springer Lecture Notes in Artificial Intelligence, Vol. 3249, ISSN 0302-9743, ISBN 3-540-23212-5). Contributed talk at AISC 2004 (7th International Conference on Artificial Intelligence and Symbolic Computation), RISC, Johannes Kepler University, Austria, September 22-24 2004. - 101
- B. Buchberger.

Algorithm supported mathematical theory exploration: A personal view and stragegy.

In B. Buchberger and J. Campbell, editors,*Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation)*, volume 3249 of*Springer Lecture Notes in Artificial Intelligence*, pages 236-250. Copyright: Springer, Berlin-Heidelberg, 22-24 September 2004. - 102
- B. Buchberger.

Algorithmic algorithm synthesis: Case study Gröbner Bases.

Invited colloquium talk at Kuyshu University, Mathematical Department, Fukuoka, Japan, August 25 2004. - 103
- B. Buchberger.

Algorithmic algorithm synthesis: Case study Gröbner Bases.

Contributed talk at International Algebra Conference, Moscow State University, May 26 - June 2 2004. - 104
- B. Buchberger.

Algorithmic algorithm synthesis: Case study Gröbner Bases.

Invited colloquium talk at KAIST (University, Daejon), October 29 2004. - 105
- B. Buchberger.

Algorithmic invention of algorithms: Case study Gröbner Bases.

Invited talk at Symposium Polynomial Systems Solving, University Paris VI, November 24-26 2004. - 106
- B. Buchberger.

Computer algebra: A key to the future of mathematics, science, and engineering.

Invited colloquium talk at KIAS (Korean Institute of Advanced Studies, Seoul), October 28 2004. - 107
- B. Buchberger.

Computer-supported mathematical theory exploration: A shift of paradigm in mathematical software.

Invited talk at Mathematica Gulf Conference 2004, Sultan Qaboos University, Department of Mathematics and Statistics, organized by M. Rakha and M. Ben Rouma, January 26-28 2004. - 108
- B. Buchberger.

Computer-supported mathematical theory exploration: Schemes, failing proof analysis, and metaprogramming.

Technical report, RISC Report Series, University of Linz, Austria, Juni 2004. - 109
- B. Buchberger.

Didactic principles for using computer algebra in class.

Lecture for High-school Teachers. Invited colloquium talk at Waseda Gakuin High School, October 16 2004. - 110
- B. Buchberger.

Elimination and self-elimination.

Invited colloquium talk at University of Bochum, Mathematical Institute, December 15 2004. - 111
- B. Buchberger.

A formal knowledge base for Gröbner Bases theory.

Invited talk at Annual Conference of the Japanese Society for Symbolic and Algebraic Computation (JSSAC), Atsugi, Japan, September 1-4 2004. - 112
- B. Buchberger.

Gröbner Bases and automated theorem proving.

Invited colloquium talk at Toho University, Mathematical Institute, Tokyo - Tsudanuma, October 9 2004. - 113
- B. Buchberger.

Gröbner Bases: Theory and applications.

Invited colloquium talk at Sultan Qaboos Universiy, Department of Mathematics and Statistics, January 25 2004. - 114
- B. Buchberger.

Groebner Basis: An Overview.

Invited colloquium talk at Workshop on Computer Algebra, RIMS (Research Institute of Mathematical Sciences), Kyoto University, Japan, August 2-4 2004. - 115
- B. Buchberger.

How I Managed to Automate Myself.

Invited talk at Conference ``The Future of Scientific Computing'', The City College of New York. (Organizer: G. Baumslag), April 30 2004. - 116
- B. Buchberger.

How to give talks and write papers.

Lecture for Graduate Students. Invited colloquium talk at Kyoto University, Graduate School for Computer Science, October 13 2004. - 117
- B. Buchberger.

How to work with the literature.

Lecture for Graduate Students. Invited colloquium talk at Kyoto University, Graduate School for Computer Science, October 4 2004. - 118
- B. Buchberger.

The importance of formal methods in mathematics.

Invited colloquium talk at Workshop on Computer Algebra, RIMS (Research Institute of Mathematical Sciences), Kyoto University, Japan, August 2-4 2004. - 119
- B. Buchberger.

Let's solve!

Teaching Experiment on Computer Algebra with High School Students. Invited colloquium talk at Waseda Gakuin High School, October 16 2004. - 120
- B. Buchberger.

A note on automated generation of an algorithm verification method.

Technical Report 2004-03, Johannes Kepler University Linz, Spezialforschungsbereich F013, March 2004. - 121
- B. Buchberger.

Proving by first and intermediate principles.

Invited talk at Workshop on Types for ``Mathematics / Libraries of Formal Mathematics'', University of Nijmegen, The Netherlands, November 1-2 2004. - 122
- B. Buchberger.

The Algorithmic Invention of a Groebner Basis Algorithm.

Invited talk at Computer Algebra Workshop at Joint Institute for Nuclear Research (Dedicated to the Memory of G. Mescsheriakov), Dubna (Moscow), Russia, organized by V. Gerdt, May 25-26 2004. - 123
- B. Buchberger.

Theorema: An overview.

Invited colloquium talk at Kyoto University, Graduate School of Computer Science, July 22-23 2004. - 124
- B. Buchberger.

The Theorema project: An overview.

Invited talk at Workshop ``Verification and Rewriting'', Institute AIST, Amagasaki, October 21 2004. - 125
- B. Buchberger.

Towards the automated synthesis of a Gröbner Bases algorithm.

*RACSAM - Revista de la Real Academia de Ciencias (Review of the Spanish Royal Academy of Science), Serie A: Mathematicas*, 98(1):65-75, 2004. - 126
- B. Buchberger.

Was sie nie ueber it wissen wollten (what you never wanted to know about it).

Invited talk at ITCOM 2004 Conference, Schloss Hagenberg, Austria, (Organizer: Bruno Bischinger), April 20 2004. - 127
- B. Buchberger.

A Historic Introduction to Gröbner Bases.

Invited talk at Summer School on Gröbner Bases and Applications, July 9-22 2005. - 128
- B. Buchberger.

Algorithm Synthesis by Lazy Thinking: Case Study Gröbner Bases.

Invited colloquium talk at DFKI, Saarbrücken, Germany, November 14-15 2005. - 129
- B. Buchberger.

Algorithm Synthesis in Theorema: Case Study Gröbner Bases.

Invited colloquium talk at University of Edinburgh, School of Informatics, June 23 2005. - 130
- B. Buchberger.

Algorithmic algorithm invention in the Theorema project.

Invited talk at Conference on Algorithms and Information Theory, Vaasa, Finland, May 16-18 2005. - 131
- B. Buchberger.

Algorithmic algorithm invention in the Theorema project.

Invited talk at AIT (Algorithmic Information Theory), Vaasa, Finland, May, 17 2005. - 132
- B. Buchberger.

Algorithmic Algorithm Synthesis: Case Study Gröbner Bases.

Invited talk at East Coast Computer Algebra Day, Ohio, Ashland, USA, March 12 2005. - 133
- B. Buchberger.

Algorithmische Beweisverfahren: Das Ende der Mathematik?

Invited colloquium talk at Kepler Symposium, Universität Linz, April 20 2005. - 134
- B. Buchberger.

Das Projekt ``Austrian IT-Park in Timisoara'' (Westrumänien).

Invited talk at CATT, Linz, March, 3 2005. - 135
- B. Buchberger.

Ein dank an meine schule, June 2005. - 136
- B. Buchberger.

Formal mathematical theory exploration in Theorema (4 lectures).

Invited talk at Summer School on Theoretical Computer Science, Marktoberdorf, August 3-13 2005. - 137
- B. Buchberger.

From Gröbner Bases to Automated Theorem Proving and Back.

3 lectures. Invited talk at Summer School on Gröbner Bases and Applications, Zanjan, Iran, July 9-22 2005. - 138
- B. Buchberger.

Gröbner-Basen: Eine Einführung für LA-Kandidaten.

Invited colloquium talk at RISC, June, 2 2005. - 139
- B. Buchberger.

Gröbner Bases: An Introduction.

Invited colloquium talk at Softwarepark Hagenberg, Feb, 02 2005. - 140
- B. Buchberger.

Introduction to Gröbner Bases.

Invited talk at Introduction to Gröbner Bases, Vaasa, Finland, May 16-18 2005. - 141
- B. Buchberger.

Lazy thinking: A new method for algorithm synthesis.

Invited colloquium talk at Workshop ``Algebraic and Numeric Algorithms and Computer-Assisted Proofs''. Research Center Schloss Dagstuhl, Germany, September 26-30 2005. - 142
- B. Buchberger.

Mathematik: Die Kunst des effektiven Handelns.

Invited colloquium talk at MathSpace, Wien, May 12 2005. - 143
- B. Buchberger.

Symbolic computation: Current trends.

Invited talk at International Workshop on Advanced Computing and Analysis Techniques in Physics Research, Berlin, Germany, May 22-27 2005. - 144
- B. Buchberger.

Theorema: A system for formal mathematics.

Invited colloquium talk at North Carolina State University, Dept of Computer Science, March 15 2005. - 145
- B. Buchberger.

A view on the future of symbolic computation.

Invited talk at ISSAC 2005 (International Symposium on Symbolic and Algebraic Computation), Bejing, July 25-27 2005. - 146
- B. Buchberger.

Automated mathematical theory exploration: How far can we go?

Invited colloquium talk at DERI, Innsbruck, December 2006. - 147
- B. Buchberger.

Automated Mathematical Theory Exploration: How Far Can We Go?

Invited colloquium talk at DERI, Innsbruck, December 14-15 2006. - 148
- B. Buchberger.

Automated Synthesis of a Gröbner Bases Algorithm.

Talk at Workshop ``Formal Gröbner Bases Theory'', March 6 2006. - 149
- B. Buchberger.

Automated Synthesis of a Gröbner Bases Algorithm.

Invited talk at Workshop ``Formal Gröbner Bases Theory'', March 6 2006. - 150
- B. Buchberger.

Die zukunft der algorithmischen mathematik: Kann mathematische forschung automatisiert werden?

Invited colloquium talk at OCG, OVE, Graz, November 2006. - 151
- B. Buchberger.

Die Zukunft der algorithmischen Mathematik: Kann mathematische Forschung automatisiert werden?

Invited colloquium talk at OCG, OVE, Graz, November 21 2006. - 152
- B. Buchberger.

Formal mathematics: A key to the future.

Invited talk at ``Engineering and Life Sciences'', Avignon, France, June 2006. - 153
- B. Buchberger.

Gröbner Bases: Tutorial for Newcomers.

Invited colloquium talk at RISC, Hagenberg, Austria, April 30 2006. - 154
- B. Buchberger.

Mathematical theory exploration.

Invited talk at IJCAR, Seattle, USA, August 2006. - 155
- B. Buchberger.

Mathematical theory exploration: Case study Gröbner Bases.

Invited talk at (SYNASC'06), Timisoara, Romania, September 2006. - 156
- B. Buchberger.

Mathematical Theory Exploration: Case Study Gröbner Bases.

Invited talk at International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06), Timisoara, Romania, September 26-29 2006. - 157
- B. Buchberger.

Symbolic computation: Current trends.

Talk at Max Planck Institute for Physics, München, January 31 2006. - 158
- B. Buchberger.

Symbolic computation: Self-application of algorithmic mathematics.

Invited talk at MAP 06 (Mathematics, Algorithms, Proofs), Mathematical Research Center, Castro-Urdiales, Spain, Jan 9-13, 2006, January 10 2006. - 159
- B. Buchberger.

Symbolic computation: Some thoughts about the future.

Invited talk at LL2006 (Loops and Legs in Quantum Physics), Eisenach, Germany, April 2006. - 160
- B. Buchberger.

The Objectives of Formal Mathematics and the Workshop on Formal Gröbner Bases Theory.

Invited talk at Workshop ``Formal Gröbner Bases Theory'', March 6 2006. - 161
- B. Buchberger, K. Aigner, C. Dupre,
T. Jebelean, F. Kriftner, M. Marin,
K. Nakagawa, O. Podisor, E. Tomuta,
Y. Usenko, D. Vasaru, and W. Windsteiger.

Theorema: An Integrated System for Computation and Deduction in Natural Style.

In*Proceedings of CADE 98 (International Conference on Computer Aided Deduction), Lindau, Germany, July 5-10*, 1998.

Workshop on integration of proving and computing. - 162
- B. Buchberger and J. Campbell, editors.

*Artificial Intelligence and Symbolic Computation*, volume 3249 of*Lecture Notes in Artificial Intelligence*. Springer Berlin-Heidelberg, September 2004. - 163
- B. Buchberger and O. Caprotti, editors.

*MKM 2001 (1st International Workshop on Mathematical Knowledge Management)*, Research Institute for Symbolic Computation, Johannes Kepler University, Hagenberg, September 24-26 2001.

ISBN 3-902276-00-2. - 164
- B. Buchberger and A. Craciun.

Algorithm synthesis by lazy thinking: Examples and implementation in Theorema.

In F. Kamareddine, editor,*Electronic Notes in Theoretical Computer Science*, volume 93, pages 24-59, 18 February 2004.

Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, Nov. 25, 2003. - 165
- B. Buchberger and A. Craciun.

Algorithm synthesis by lazy thinking: Using problem schemes.

In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,*Proceedings of 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04)*, pages 90-106, Timisoara, Romania, 26-30 September 2004. Mirton Publisher. - 166
- B. Buchberger, A. Craciun,
T. Jebelean, L. Kovacs, T. Kutsia,
K. Nakagawa, F. Piroi, N. Popov,
J. Robu, M. Rosenkranz, and
W. Windsteiger.

Theorema: Towards computer-aided mathematical theory exploration.

*Journal of Applied Logic*, 4(4):470-504, 2006. - 167
- B. Buchberger, C. Dupré,
T. Jebelean, K. Kriftner, K. Nakagawa,
D. Vasaru, and W. Windsteiger.

*Theorema*: A short demo.

In*Proceedings of the International Mathematica Symposium '99*, RISC, Austria, August 1999. - 168
- B. Buchberger, C. Dupré,
T. Jebelean, K. Kriftner, K. Nakagawa,
D. Vasaru, and W. Windsteiger.

The Theorema Project: A Progress Report.

8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, St. Andrews, Scotland, August 6-7, 2000. - 169
- B. Buchberger, C. Dupré,
T. Jebelean, K. Kriftner, K. Nakagawa,
D. Vasaru, and W. Windsteiger.

The Theorema project: A progress report.

In M. Kerber and M. Kohlhase, editors,*Proceedings of the 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, St. Andrews, Scotland*, pages 100-115, August 2000. - 170
- B. Buchberger, G. Gonnet, and
M. Hazewinkel, editors.

*Special Issue on Mathematical Knowledge Management, Annals of Mathematics and Artificial Intelligence*, volume 38. Kluwer Academic Publisher, 2003. - 171
- B. Buchberger and T. Ida.

Computational origami: Interaction of solving, proving and computing.

In*Proceedings of World Conference on 21st Century Mathematics*, Lahore, Pakistan, 18-20 March 2004. - 172
- B. Buchberger and T. Jebelean, editors.

*The 2nd International Theorema Workshop*. Proceedings published as RISC-Report 98-10, June 29-30 1998.

Hagenberg, Austria. - 173
- B. Buchberger and T. Jebelean.

The Theorema System, invited tutorial.

MFCS'98 (International Conference on Mathematical Foundations of Computer Science), Brno, Czech Republic, 1998. - 174
- B. Buchberger and T. Jebelean.

Using Theorema for Mathematical Education.

IMACS Conference on Applied Computer Algebra, Prague, Czech Republic, 1998. - 175
- B. Buchberger and T. Jebelean.

Distance teaching of mathematics using*Theorema*.

In H. Gutmann, editor,*Proceedings of the Third Technion Symposium on Software for Communication, Hagenberg, Austria*, April 1999. - 176
- B. Buchberger and T. Jebelean.

Teaching of mathematics using*Theorema*.

*International Journal of Computer Algebra in Mathematical Education*, 6(1):25-50, 1999. - 177
- B. Buchberger, T. Jebelean, and
K. Nakagawa.

Using the Predicate Logic Prover of Theorema for Formal Training in Mathematics.

In B. Buchberger and T. Jebelean, editors,*Proceedings of the 2nd International Theorema Workshop, Hagenberg, Austria*, pages 76-87, 1998. - 178
- B. Buchberger, T. Jebelean, and
D. Vasaru.

Theorema: A System for Formal Scientific Training in Natural Language Presentation.

In*Proceedings of ED-MEDIA 98 (International Conference on Educational Multimedia), Freiburg, Germany*, pages 174-179, June 20-23 1998. - 179
- B. Buchberger and K. Nakagawa.

Logicographic symbols: A new concept in logic syntax.

In*Proceedings of the INTAS Conference on Rewriting Techniques and Efficient Theorem Proving*, 2000. - 180
- B. Buchberger and K. Nakagawa.

Mathematical knowledge editor: A research plan.

Technical report, Johannes Kepler University Linz, 2004.

Spezialforschungsbereich SF013 ``Scientific Computing'', FWF (Austrian National Science Foundation). - 181
- B. Buchberger and the Theorema Group.

*Theorema*, version 1.0.

Published on CD-ROM, CALCULEMUS '99, Trento, Italy, July 1999.

Developed at RISC, Hagenberg, Austria. - 182
- B. Buchberger and D. Vasaru.

The Theorema PCS prover.

Jahrestagung der DMV, Dresden, September 18-22, 2000. - 183
- B. Buchberger, D. Vasaru, and
T. Jebelean.

The Theorema system: Current status and the proving-solving-computing cycle.

In*Proceedings of RTETP (Rewriting Techniques and Efficient Theorem Proving)*, Kiev, June 2000. - 184
- B. Buchberger and W. Windsteiger.

The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols.

In*Proceedings of Calculemus 98, Eindhoven, Netherlands*, 1998. - 185
- B. Buchberger and W. Windsteiger.

The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols in the Theorema System.

In B. Buchberger and T. Jebelean, editors,*Proceedings of the Second International Theorema Workshop*, pages 88-98, 1998.

RISC report 98-10. - 186
- E. M. Clarke, A. S. Gavlovski,
K. Sutner, and W. Windsteiger.

Analytica V: Towards the Mordell-Weil Theorem.

In A. Bigatti and S. Ranise, editors,*Proceedings of Calculemus'06*, Genova, Italy, 2006. - 187
- A. Craciun.

The sequence provers in Theorema.

Joint AISC'02 - Calculemus '02 conference, Marseille, France, July 1-5, 2002; Appears in: Seki-Report Series Nr. SR-02-04, Calculemus 2002, Work in Progress Papers, Universität des Saarlandes, July 2002. - 188
- A. Craciun.

THEOREMA: An Overview.

Contributed talk at Scottish Theorem Provers Workshop, Glasgow, UK, December 19 2003. - 189
- A. Craciun.

An Implementation of Groebner Synthesis in Theorema.

Contributed talk at Special Semester on Groebner Bases and Related Methods, Workshop C, Linz, Austria, March 6-10 2006. - 190
- A. Craciun.

Lazy Thinking Synthesis of a Groebner Bases Algorithm.

Poster presentation at Calculemus'06, 13th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Genova, Italy, July 7-9 2006. - 191
- A. Craciun.

*Lazy Thinking Algorithm Synthesis in Groebner Bases Theory*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 192
- A. Craciun and B. Buchberger.

Proving the correctness of the merge-sort algorithm with Theorema.

In*Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02)*, pages 97-111, Timisoara, Romania, October 2002.

ISBN 973-585-785-5. - 193
- A. Craciun and B. Buchberger.

Functional program verification with Theorema.

Contributed talk at Computer Aided Verification of Information Systems: A Practical Industry-Oriented Approach (CAVIS'03), February 2003. - 194
- A. Craciun and B. Buchberger.

The lazy thinking paradigm: Top-down theory exploration using Theorema.

Poster presentation at the Calculemus Midterm Review Meeting, University of Saarlandes, Saarbruecken, Germany, March 2003. - 195
- A. Craciun and B. Buchberger.

Mathematical knowledge management for reasoning about programs: Tuples and sorting.

Contributed talk at SFB Status Seminar, Strobl, Austria, April 24-26 2003. - 196
- A. Craciun and B. Buchberger.

Theory exploration by lazy thinking: A case study.

Contributed talk at Omega-Theorema Workshop, Hagenberg, Austria, May 25-27 2003. - 197
- A. Craciun and B. Buchberger.

Algorithm synthesis case studies: Sorting of tuples by lazy thinking.

Technical Report 04-16, RISC Report Series, University of Linz, Austria, October 2004. - 198
- A. Craciun and B. Buchberger.

Preprocessed lazy thinking: Synthesis of sorting algorithms.

Technical Report 04-17, RISC Report Series, University of Linz, Austria, October 2004. - 199
- A. Craciun and M. Hodorog.

Decompositions of Natural Numbers: From A Case Study in Mathematical Theory Exploration.

In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,*Proceedings of the 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'07)*, pages 1-8, Timisoara, Romania, 26-29 September 2007.

to appear as IEEE volume. - 200
- A. Craciun and M. Hodorog.

The Quotient-Remainder Theorem for Natural Numbers: Discovery by Lazy Thinking.

Contributed talk at First Central and Eastern European Conference on Computer Algebra and Dynamic Geometry Systems in Mathematics Education (CADGME), Pecs, Hungary, June 21 2007. - 201
- B. Dundua.

*Rule-Based Programming with Context and Sequence Variables*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 202
- M. Erascu.

Algorithm Analysis Using Logical and Algebraic Techniques.

Master's thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 203
- M. Erascu and T. Jebelean.

Verification of imperative programs using forward reasoning.

Contributed talk at SFB Statusseminar, Strobl, Austria, Apr., 11-14 2007. - 204
- M. Erascu and T. Jebelean.

Verification of Imperative Programs using Symbolic Execution and Forward Reasoning in the Theorema System.

Technical Report 07-12, RISC Linz, July 1 2007.

Presented at First Austria-Japan Workshop on Symbolic Computation and Software Verification, Linz, Austria, July 1st 2007. - 205
- Y. W. Feng.

A Java infrastructure for pattern based programming.

Master's thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 206
- M. Giese.

A logic with subtypes to talk about java objects.

Invited colloquium talk at UCD Systems Research Group, Dublin, Ireland, August 2006. - 207
- M. Giese.

A logic with subtypes to talk about java objects.

Invited talk at ESF Exploratory Workshop: Challenges in Java Program Verification, Nijmegen, The Netherlands, October 2006. - 208
- M. Giese.

Panelist at Panel Discussion, Intl. Workshop on Implementation of Logics, Phnom Penh, Cambodia.

November 2006. - 209
- M. Giese.

Practical reflection for formal mathematics in Theorema,.

Invited colloquium talk at SCORE Workshop on Proving and Solving, Aizu-Wakamatsu, Japan, 15.03.06 - 17.03.06, March 2006. - 210
- M. Giese.

Practical reflection for formal mathematics in Theorema.

Contributed talk at Workshop on Formal Gröbner Bases Theory, Linz, Austria, March 2006. - 211
- M. Giese.

Saturation up to redundancy for tableau and sequent calculi.

In M. Hermann and A. Voronkov, editors,*Logic for Programming, Artificial Intelligence, and Reasoning, 13th Intl. Conf., LPAR 2006, Phnom Penh, Cambodia*, volume 4246 of*LNCS*, pages 182-196, 2006. - 212
- M. Giese.

Superposition-based equality handling for analytic tableaux.

*Journal of Automated Reasoning*, 38(1-3):127-153, December 2006.

Appeared online 2 December 2006, in print April 2007. - 213
- M. Giese.

Aspects of first-order reasoning in the KeY system.

Invited talk at First Order Theorem Proving (FTP), Liverpool, UK, September 2007. - 214
- M. Giese.

First-order logic.

volume 4334 of*LNCS*, chapter 2, pages 21-68. Springer-Verlag, 2007. - 215
- M. Giese.

Saturation up to redundancy for tableau and sequent calculi.

Logic & Computation Workshop, Alta, Norway, January 2007. - 216
- M. Giese.

Some facts about the implementation of the KeY system.

Logic & Computation Workshop, Alta, Norway, January 2007. - 217
- M. Giese and B. Buchberger.

Towards practical reflection for formal mathematics.

Technical Report 07-05, RISC Report Series, University of Linz, Austria, 2007. - 218
- M. Giese and B. Buchberger.

Towards practical reflection for formal mathematics.

In*Proceedings of Austria-Japan Workshop on Symbolic Computation and Software Verification*, volume 2007 of*RISC Report Series*, pages 30-34, July 2007. - 219
- M. Giese and T. Jebelean, editors.

*Proceedings Workshop on Invariant Generation, WING 2007*, number 07-07 in RISC Report Series, June 2007. - 220
- M. Hodorog.

*Systematic Exploration of Mathematical Theories*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 221
- M. Hodorog and A. Craciun.

Scheme-Based Systematic Exploration of Natural Numbers.

In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,*Proceedings of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'06), Timisoara, Romania*, pages 23-34, 26-29 September 2006. - 222
- M. Hodorog and A. Craciun.

A Case Study in Systematic Theory Exploration: Natural Numbers.

Technical report, RISC Report Series, University of Linz, Austria, October 2007.

RISC,University of Linz, Austria. - 223
- T. Ida and B. Buchberger.

Proving and Solving in Computational Origami.

*Analele Universitatii din Timisoara, Seria Matematica - Informatica*, XLI:247-263, 2003.

special issue on Computer Science - Proceedings of SYNASC'03. - 224
- T. Ida and M. Marin.

Functional Logic Origami Programming with Open CFLP.

In P. Mitic, P. Ramsden, and J. Carne, editors,*Challenging the Boundaries of Symbolic Computation. Proceedings of 5th International Mathematica Symposium (IMS 2003)*, Imperial College, London, 2003. Imperial College Press. - 225
- T. Ida, M. Marin, and H. Takahashi.

Constraint Functional Logic Programming for Origami Construction.

In*Proceedings of the First Asian Symposium on Programming Languages and Applications*, Beijing, China, 2003. - 226
- T. Ida, D. Tepeneu, B. Buchberger, and
J. Robu.

Proving and constraint solving in computational origami.

In B. Buchberger and J. Campbell, editors,*Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation)*, volume 3249 of*Springer Lecture Notes in Artificial Intelligence*, pages 132-142. Copyright: Springer-Berlin, 22-24 September 2004. - 227
- T. Jebelean.

Natural Proofs in Elementary Analysis by S-Decomposition.

Invited talk at ISSAC'01: International Symposium on Symbolic and Algebraic Computation, London, Ontario, Canada, July 2001. - 228
- T. Jebelean.

Natural style predicate logic proving in Theorema.

ICAI'01: 5th International Conference on Applied Informatics Eger, Hungary, January 2001. - 229
- T. Jebelean.

*Non-conventional Algorithms for Multiple Precision Arithmetic*.

Habilitation thesis, RISC, University of Linz, December 2001. - 230
- T. Jebelean.

Nonconventional Algorithms for Multiprecision Arithmetic.

In V. Negru et al., editors,*Proceeding of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02)*, pages 3-7, Timisoara, Romania, October 2002. Mirton. - 231
- T. Jebelean.

Theorema: A system for the working mathematician.

In*Proceedings of ISSAC'02*, 2002.

The abstract of the talk and the software demo are published electronically on the CD-ROM accompanying the proceedings (ACM Press, ISBN 1-58113-582-3). - 232
- T. Jebelean.

Theorema: A system for the working mathematician.

Invited talk at International Symposium ``35 years of Automath'', Edinburgh, Scotland, August 2002. - 233
- T. Jebelean.

Theorema: A system for the working mathematician. software demonstration.

ISSAC'02 (International Symposium for Symbolic and Algebraic Computation, Lille, France, July 2002). The abstract of the talk and the software demo are published electronically on the CD-ROM accompanying the proceedings (ACM Press, ISBN 1-58113-582-3)., July 2002. - 234
- T. Jebelean.

Using hyper-inferences for natural style proving in predicate logic.

SFB Statusseminar Strobl, Austria, April 2002. - 235
- T. Jebelean.

Exploring mathematics with Theorema.

Contributed talk at International Symposium on Symbolic and Algebraic Computation (ISSAC'03), Philadelphia, USA, August 2003. - 236
- T. Jebelean.

Imperative program verification with Theorema.

Contributed talk at Computer Aided Verification of Information Systems: A Practical Industry-Oriented Approach (CAVIS'03), e-Austria Institute, Timisoara, Romania, February 2003. - 237
- T. Jebelean.

Forward verification of recursive programs.

In Proceedings of CAVIS 04. Contributed talk at Computer Aided Verification of Information Systems, Timisoara, Romania, February 2004. - 238
- T. Jebelean.

Using computer algebra for automated reasoning in the Theorema system.

Invited talk at Seventh Asian Symposium on Computer Mathematics (ASCM 2005), Seoul, Korea, December 15 2005. - 239
- T. Jebelean and B. Buchberger.

Theorema: A system for the working mathematician.

Contributed talk at SNSC'01, Hagenberg, Austria, September 2001. - 240
- T. Jebelean and B. Buchberger.

Theorema: Computation and Deduction in Natural Style.

In J. Grabmeier, E. Kaltofen, and V. Weispfennig, editors,*Computer Algebra Handbook*, pages 453-454. Springer - Verlag Berlin, 2003. - 241
- T. Jebelean and B. Konev.

Using meta-variables for natural deduction in Theorema.

In M. Kerber and M. Kohlhase, editors,*Proceedings of the CALCULEMUS 2000 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning*, pages 160-175, St. Andrews, Scotland, August 6-7 2000. - 242
- T. Jebelean, L. Kovacs, and N. Popov.

Verification of imperative programs in Theorema.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2003. - 243
- T. Jebelean, L. Kovacs, and N. Popov.

Verification of imperative programs in Theorema.

In D. Dranidis and K. Tigka, editors,*Proceedings of the 1st South-East European Workshop in Formal Methods (SEEFM'03)*, Thessaloniki, Greece, November 20 2003. - 244
- T. Jebelean, L. Kovacs, and N. Popov.

Experimental program verification in the Theorema system.

In T. Margaria and B. Steffen, editors,*Proceedings ISOLA 2004*, pages 92-99, Paphos, Cyprus, November 2004. - 245
- T. Jebelean, L. Kovacs, and N. Popov.

Experimental program verification in the Theorema system.

*STTT*, 2006.

in press. - 246
- T. Jebelean, B. Kutzler, and
P. Schofield, editors.

*Applications of Computer Algebra in Education*, volume 6. Special issue of the International Journal of Computer Algebra in Mathematics Education, 1999. - 247
- T. Jebelean and V. Negru, editors.

*Proceedings of the Second International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'00)*, Timisoara, Romania, October 2000. University of Timisoara. - 248
- T. Jebelean and V. Negru, editors.

*Proceedings of the International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01)*, Timisoara, Romania, September 2001. Mirton. - 249
- T. Jebelean and V. Negru, editors.

*Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02)*, Timisoara, Romania, October 2002. Mirton.

ISBN 973-585-785-5. - 250
- T. Jebelean and V. Negru, editors.

*Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03)*, Timisoara, Romania, October 2003. Mirton. - 251
- T. Jebelean and V. Negru, editors.

*Proceedings of International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04)*, Timisoara, Romania, September 2004. Mirton. - 252
- T. Jebelean and V. Negru, editors.

*Proceedings of the International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05)*, Timisoara, Romania, 2005. Mirton. - 253
- T. Jebelean and V. Negru, editors.

*Proceedings of the International Workshop on Symbolic and Numeric Algorithms for Scientific Computing SYNASC'06*, Timisoara, Romania, September 2006. Mirton. - 254
- T. Jebelean and V. Negru, editors.

*Proceedings of the International Workshop on Symbolic and Numeric Algorithms for Scientific Computing SYNASC'07*, Timisoara, Romania, September 2007. Mirton. - 255
- T. Jebelean and L. Szakacs.

Functional-based synthesis of systolic online multipliers.

In D. Zaharie, D. Petcu, V. Negru, and T. Jebelean, editors,*International Symposium on Symbolic and Numeric Scientific Computing (SYNASC'05), Timisoara, Romania*, pages 267-275. IEEE Computer Society, 2005. - 256
- M. Kauers, M. Kerber, R. Miner, and
W. Windsteiger.

Calculemus/mkm 2007 - work in progress.

Technical Report 07-06, RISC Report Series, University of Linz, Austria, 2007. - 257
- M. Kauers, M. Kerber, R. Miner, and
W. Windsteiger, editors.

*Towards Mechanized Mathematical Assistants, Proceedings of Calculemus'07 and MKM'07 conferences, Hagenberg, Austria*, volume 4573 of*Lecture Notes in Computer Science*, Heidelberg, 2007. Springer. - 258
- M. Kirchner.

Program verification within*Theorema*.

Master's thesis, FHS-Hagenberg, 1999. - 259
- N. Kobayashi, M. Marin, and T. Ida.

A web oriented system for equational solving.

In G. Vidal, editor,*Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming, WFLP'03*, 2003. - 260
- B. Konev.

Metavariable method for natural deduction within*Theorema*.

Technical report, RISC - Report 99-34, 1999. - 261
- B. Konev and T. Jebelean.

Combining level-saturation strategies and meta-variables for predicate logic proving in Theorema.

In*IMACS ACA 2000, St. Petersburg, Russia*, June 2000. - 262
- B. Konev and T. Jebelean.

Solution Lifting Method for Handling Meta-variables in Theorema.

In V. Negru and T. Jebelean, editors,*3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), Timisoara, Romania*, October 2001. - 263
- F. Kossak.

An interface for interactive proving with the mathematical software system*Theorema*.

Master's thesis, FHS-Hagenberg, 1999. - 264
- F. Kossak and K. Nakagawa.

User System Interaction Within*Theorema*.

In A. Armando and T. Jebelean, editors,*Electronic Notes in Theoretical Computer Science*, volume 23. Elsevier, 1999.

Calculemus 99 Workshop, Trento, Italy. - 265
- A. Kovacs and L. Kovacs.

The lagrange interpolation formula in determining the fluid's velocity potential through profile grids.

In F. Fazekas et al., editors,*Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-147/148*, Balatonalmadi, Hungary, 26-29 May 2005. Technical University of Budapest, PAMM-Centre. - 266
- A. Kovacs, G. Tigan, L. Kovacs, and
C. Milici.

*Computer Assisted Mathematics (in romanian: ``Matematic Superioare Asistae de Calculator'')*.

Politechnica Publisher, Timisoara, 1st edition, 2006. - 267
- L. Kovacs.

Program verification using Hoare logic.

Computer Aided Verification of Information Systems: A Practical Industry-Oriented Approach (CAVIS'03), e-Austria Institute, Timisoara, February 2003. - 268
- L. Kovacs, November 18-19 2005.

British Computer Society (BSC) - Formal Aspects of Computing Science (FACS) award. (Joint work with T. Jebelean and N. Popov). - 269
- L. Kovacs.

Imperative program verification in Theorema.

Contributed talk at Theorema-Ultra-Omega'05 Workshop, Department of Computer Science, University of Saarbruecken, Germany, November 14-15 2005. - 270
- L. Kovacs.

Using combinatorial and algebraic techniques for automatic generation of loop invariants.

Technical Report 05-16, RISC Report Series, University of Linz, Austria, 2005. - 271
- L. Kovacs.

Combining algebraic and logic techniques for program verification.

Contributed talk at SFB Cooperation Meeting, Johannes Kepler University Linz, December 18 2006. - 272
- L. Kovacs.

Aligator: a Package for Reasoning about Loops.

In*Proc. of 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)*, Yerevan, Armenia, October 2007.

Short paper. to appear. - 273
- L. Kovacs.

Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema.

In M. Giese and T. Jebelean, editors,*Proc. of WING'07, RISC, Austria*, pages 56-69, 2007.

RISC Report Series No. 07-07. - 274
- L. Kovacs.

*Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema*.

PhD thesis, RISC, Johannes Kepler University Linz, Austria, October 2007.

RISC Technical Report No. 07-16. - 275
- L. Kovacs.

Automated Loop Invariant Generation by Algebraic Techniques Over the Rationals.

Contributed talk at Alpine Verification Meeting, Aussois, France, April 2007. - 276
- L. Kovacs.

Automated Loop Invariant Generation by Algebraic Techniques Over the Reals.

Invited colloquium talk at Formal Methods Group, School of Computer Science, Manchester University, UK, March 2007. - 277
- L. Kovacs.

Polynomial invariant generation by algebraic techniques for program verification in Theorema.

Invited colloquium talk at Institut de Recherche en Informatique de Toulouse (IRIT), Paul Sabatier University, Toulouse, France, 26 March 2007. - 278
- L. Kovacs.

Polynomial Invariant Generation by Algebraic Techniques for Program Verification in Theorema.

Invited colloquium talk at Models and Theory of Computation, Ecole Polytechnique Federale de Lausanne (EPFL), Switzerland, February 2007. - 279
- L. Kovacs.

Reasoning Algebraically About P-solvable Loops.

Contributed talk at SCORE Summer Workshop on Symbolic Computation and Software Verification, Fuji Susono, Japan, August 31 - September 3 2007. - 280
- L. Kovacs.

Reasoning Algebraically About P-solvable Loops.

Contributed talk at Dagstuhl Seminar 07401 on ``Deduction and Decision Procedures'', Schloss Dagstuhl, Germany, September 30 - October 5 2007. - 281
- L. Kovacs.

Using Symbolic Summation and Polynomial Algebra for Automated Generation of Polynomial Invariants in Theorema.

Invited colloquium talk at VERIMAG, Grenoble, France, February 2007. - 282
- L. Kovacs and T. Jebelean.

Generation of Invariants in Theorema.

In N. Boja, editor,*Proceedings of the 10th International Symphosium of Mathematics and its Application*, pages 407-415, 6-9 November 2003.

Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics. - 283
- L. Kovacs and T. Jebelean.

Practical Aspects of Imperative Program Verification in Theorema.

*Analele Universitatii din Timisoara, Seria Matematica - Informatica*, XLI:135-154, 2003.

special issue on Computer Science - Proceedings of SYNASC'03. - 284
- L. Kovacs and T. Jebelean.

Practical aspects of imperative program verification using Theorema.

In T. Jebelean and V. Negru, editors,*Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03)*, Timisoara, Romania, 2003. - 285
- L. Kovacs and T. Jebelean.

Automated generation of loop invariants by recurrence solving in Theorema.

In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,*Proceedings of the 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04)*, pages 451-464, Timisoara, Romania, 26-30 September 2004. Mirton Publisher. - 286
- L. Kovacs and T. Jebelean.

Automated generation of loop invariants by recurrence solving in Theorema.

*Analele Universitatii din Timisoara, Seria Matematica - Informatica*, XLII:151-166, 2004.

special issue on Computer Science - Proceedings of SYNASC'04. - 287
- L. Kovacs and T. Jebelean.

Generation of loop invariants in Theorema by combinatorial and algebraic methods.

In F. Fazekas et al., editors,*Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-144*, volume vol. CVI, pages 125-134, Balatonalmadi, Hungary, 20-23 May 2004. Technical University of Budapest, PAMM-Centre. - 288
- L. Kovacs and T. Jebelean.

Loop verification and imperative program execution in Theorema.

Contributed talk at Computer Aided Verification of Information Systems (CAVIS'04),Timisoara, Romania, 27 February 2004. - 289
- L. Kovacs and T. Jebelean.

An algorithm for automated generation of invariants for loops with conditionals.

In T. Jebelean and V. Negru, editors,*7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), Timisoara, Romania*, pages 16-19, September 25-28 2005. - 290
- L. Kovacs and T. Jebelean.

An algorithm for automated generation of invariants for loops with conditionals.

Contributed talk at 7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'05), September 25-29 2005. - 291
- L. Kovacs and T. Jebelean.

Generating Invariance Properties by Recurrence Solving and Groebner Basis Computation in the Theorema System.

Contributed talk at Dagstuhl Seminar 05311: Verifying Optimizing Compilers, July 2005. - 292
- L. Kovacs and T. Jebelean.

Polynomial invariant generation by algebraic and combinatorial methods.

Contributed talk at SFB Cooperation Meeting, Johannes Kepler University Linz, December 19 2005. - 293
- L. Kovacs and T. Jebelean.

Using combinatorial and algebraic techniques for automatic generation of loop invariants.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 1 2005. - 294
- L. Kovacs and T. Jebelean.

Automated generation of polynomial invariants for imperative program verification in Theorema.

Contributed talk at INTAS Project Meeting, Institute eAustria, Timisoara, Romania, December 10-11 2006. - 295
- L. Kovacs and T. Jebelean.

Combining Computer Algebra and Computational Logic for Imperative Program Verification in Theorema.

Poster presentation at Calculemus'06, Genova, Italy, July 6-9 2006. - 296
- L. Kovacs and T. Jebelean.

Finding Polynomial Invariants for Imperative Loops.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2006. - 297
- L. Kovacs and T. Jebelean.

Finding polynomial invariants for imperative loops in the Theorema system.

Technical Report 03-06, RISC Report Series, University of Linz, Austria, 2006. - 298
- L. Kovacs and T. Jebelean.

Finding polynomial invariants for imperative loops in the Theorema system.

In S. Autexier and H. Mantel, editors,*Proceedings of Verify'06 Workshop, IJCAR'06, The 2006 Federated Logic Conference, Seattle, USA*, pages 52-67, August 15-16 2006. - 299
- L. Kovacs and T. Jebelean.

Using symbolic summation and polynomial algebra for imperative program verification in the Theorema system.

Contributed talk at 12th International Conference on Applications of Computer Algebra (ACA'06), Varna, Bulgaria, June 26-29 2006. - 300
- L. Kovacs and T. Jebelean.

Algebraic Methods for Invariant Generation.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2007. - 301
- L. Kovacs, T. Jebelean, and D. Kapur.

Using symbolic summation and polynomial algebra for imperative program verification in Theorema.

Technical report, RISC-Linz, 2006.

submitted to MatCom Journal. - 302
- L. Kovacs, T. Jebelean, and A. Kovacs.

Practical aspects of algebraic invariant generation for loops with conditionals.

volume CVIII/2251, pages 116-125. Technical University of Budapest, PAMM-Centre, 2005.

ISSN 0133-3526. Proc. of Pannonian Applied Mathematical Meetings, PC-147/148, Balatonalmadi, Hungary, 26-29 May 2005. - 303
- L. Kovacs and N. Popov.

Procedural program verification in Theorema.

Contributed talk at Omega-Theorema Workshop, Hagenberg, Austria, May 25-27 2003. - 304
- L. Kovacs, N. Popov, and T. Jebelean.

A verification environment for imperative and functional programs in the Theorema system.

Contributed talk at 2nd South-East European Workshop on Formal Methods (SEEFM05), Ohrid, Macedonia, 18-19 November 2005. - 305
- L. Kovacs, N. Popov, and T. Jebelean.

Verification environment in Theorema.

*Annals of Mathematics, Computing and Teleinformatics (AMCT)*, 1(2):27-34, 2005. - 306
- L. Kovacs, N. Popov, and T. Jebelean.

Combining logic and algebraic techniques for program verification in Theorema.

In T. Margaria and B. Steffen, editors,*Proceedings ISOLA 2006*, Paphos, Cyprus, November 2006. - 307
- F. Kriftner.

Theorema: The Language.

In B. Buchberger and T. Jebelean, editors,*Proceedings of the Second International Theorema Workshop, Hagenberg, Austria*, pages 39-54, 1998.

available as RISC report 98-10. - 308
- Kusper, Schreiner, and Lovas.

Integrating temporal specifications as runtime assertions into parallel debugging tools.

Technical report, RISC, 2002.

Technical Report 02-07, RISC-Linz. - 309
- G. Kusper.

Solving the resolution-free sat problem in polynomial time by sub-model propagation.

Technical Report 01-06, RISC-Linz, February 2001. - 310
- G. Kusper.

Solving the Resolution-Free SAT Problem in Polynomial Time by Sub-Model Propagation.

5th International Conference on Applied Informatics Eger, Hungary, January 2001. - 311
- G. Kusper.

Integrating Temporal Assertions into a Parallel Debugger.

In B. Monien and R. Feldmann, editors,*Proceedings of the 8th International Euro-Par Conference*, pages 113-120, Paderborn, Germany, 2002. Springer-Verlag. - 312
- G. Kusper.

Investigation of Binary Representations of SAT, especially 2-Literal Representation.

Conference of PhD Students in Computer Science, Szeged, Hungary, July 2002. - 313
- G. Kusper.

Solving the resolution-free sat problem by hyper-unit propagation in linear time.

Fifth International Symposium on the Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, USA, May 2002. - 314
- G. Kusper.

Solving the sat problem by hyper-unit propagation.

RISC Linz Report Series 02-02, Research Institute for Symbolic Computation, J. Kepler University Linz, 2002. - 315
- G. Kusper.

Solving the resolution-free sat problem by hyper-unit propagation in linear time.

*Annals of Mathematics and Artificial Intelligence*, 43(1-4):129-136, 2005. - 316
- T. Kutsia.

Unification in the empty and flat theories with sequence variables and flexible arity symbols.

Contributed talk at the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus'01), Siena, Italy, June 2001. - 317
- T. Kutsia.

Gröbner bases approach towards formula simplification in operator theory.

Talk at the SFB Statusseminar, Strobl, Austria, April 2002. - 318
- T. Kutsia.

Pattern unification with sequence variables and flexible arity symbols.

*Electronic Notes in Theoretical Computer Science*, 66(5), 2002. - 319
- T. Kutsia.

*Solving and Proving in Equational Theories with Sequence Variables and Flexible Arity Symbols*.

PhD thesis, RISC, Johannes Kepler University, Linz, Austria, 2002. - 320
- T. Kutsia.

Theorem proving with sequence variables and flexible arity symbols.

In M. Baaz and A. Voronkov, editors,*Logic in Programming, Artificial Intelligence and Reasoning. Proceedings of the 9th International Conference LPAR'02*, volume 2514 of*Lecture Notes in Artificial Intelligence*, pages 278-291, Tbilisi, Georgia, October 14-18 2002. Springer Verlag.

ISBN 3-540-00010-0. - 321
- T. Kutsia.

Unification in a free theory with sequence variables and flexible arity symbols and its extensions.

Technical report, Johannes Kepler University, Linz, 2002.

SFB Report 02-6. - 322
- T. Kutsia.

Unification with sequence variables and flexible arity symbols.

Talk at the SFB Statusseminar, Strobl, Austria, April 2002. - 323
- T. Kutsia.

Unification with sequence variables and flexible arity symbols and its extension with pattern-terms.

In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors,*Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AICS'2002 - Calculemus'2002 conference*, volume 2385 of*Lecture Notes in Artificial Intelligence*, pages 290-304, Marseille, France, July 2002. Springer Verlag.

ISBN 3-540-43865-3. - 324
- T. Kutsia.

Equational prover of Theorema.

In R. Nieuwenhuis, editor,*Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03)*, volume 2706 of*LNCS*, Valencia, Spain, 2003. Springer Verlag. - 325
- T. Kutsia.

Matching in flat theories.

In J. Levy, M. Kohlhase, J. Niehren, and M. Villaret, editors,*Proceedings of the 17th International Workshop on Unification (UNIF 2003)*, Valencia, Spain, 2003. - 326
- T. Kutsia.

Unification modulo flatness.

In T. Jebelean and V. Negru, editors,*Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03)*, Timisoara, Romania, 2003. - 327
- T. Kutsia.

Solving equations involving sequence variables and sequence functions.

In B. Buchberger and J. A. Campbell, editors,*Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation, AISC'04*, volume 3249 of*Lecture Notes in Artificial Intelligence*, pages 157-170, Hagenberg, Austria, Sep 22-24 2004. Springer Verlag. - 328
- T. Kutsia.

Solving equations involving sequence variables and sequence functions.

Technical Report 04-01, RISC Report Series, University of Linz, Austria, January 2004. - 329
- T. Kutsia.

Solving equations involving sequence variables and sequence functions.

Contributed talk at the 7th International Conference on Artificial Intelligence and Symbolic Computation (AISC'04), Hagenberg, Austria, September 2004. - 330
- T. Kutsia.

Context sequence matching for XML.

In M. Alpuente, S. Escobar, and M. Falaschi, editors,*Proceedings of the 1th International Workshop on Automated Specification and Verification of Web Sites (WWV'05)*, pages 103-119, Valencia, Spain, March 14-15 2005.

(Final version to appear in Elsevier ENTCS). - 331
- T. Kutsia.

Context sequence matching for XML.

Contributed talk at the 1th International Workshop on Automated Specification and Verification of Web Sites (WWV'05), Valencia, Spain, March 15 2005. - 332
- T. Kutsia, 2006.
- 333
- T. Kutsia.

Context sequence matching for XML.

*Electronic Notes in Theoretical Computer Science*, 157(2):47-65, 2006. - 334
- T. Kutsia.

Matching with regular constraints.

Invited colloquium talk at Department of Computer Science, Graduate School of Systems and Information Engineering, University of Tsukuba, Japan, March 14 2006. - 335
- T. Kutsia.

Matching with regular constraints.

Invited talk at SCORE Workshop on Proving and Solving, University of Aizu, Aizuwakamatsu, Japan, March 16 2006. - 336
- T. Kutsia, 2007.
- 337
- T. Kutsia, 2007.

Series of lectures. - 338
- T. Kutsia.

*Contributions to Equational Reasoning*.

Habilitation thesis, RISC, University of Linz, Austria, 2007.

Ongoing. - 339
- T. Kutsia.

Solving equations with sequence variables and sequence functions.

*JSC*, 43(2):352-388, 2007. - 340
- T. Kutsia and B. Buchberger.

Predicate logic with sequence variables and sequence function symbols.

In A. Asperti, G. Bancerek, and A. Trybulec, editors,*Proceedings of the 3rd International Conference on Mathematical Knowledge Management, MKM'04*, volume 3119 of*Lecture Notes in Computer Science*, pages 205-219, Bialowieza, Poland, Sep 19-21 2004. Springer Verlag. - 341
- T. Kutsia and B. Buchberger.

Predicate logic with sequence variables and sequence function symbols.

Contributed talk at the 3rd International Conference on Mathematical Knowledge Management (MKM'04), Bialowieza, Poland, September 2004. - 342
- T. Kutsia and B. Buchberger.

Predicate logic with sequence variables and sequence function symbols.

Technical Report 05-17, RISC Report Series, University of Linz, Austria, 2005. - 343
- T. Kutsia, J. Levy, and M. Villaret.

Sequence unification through currying.

In F. Baader, editor,*Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA'07)*, volume 4533 of*Lecture Notes in Computer Science*, pages 288-302, Paris, France, 2007. - 344
- T. Kutsia and M. Marin.

Unification procedure for terms with sequence variables and sequence functions (extended abstract).

In M. Kohlhase, editor,*Proceedings of the 18th International Workshop on Unification (UNIF'04)*, pages 1-13, Cork, Ireland, 5 2004. - 345
- T. Kutsia and M. Marin.

Can context sequence matching be used for querying XML?

In L. Vigneron, editor,*Proceedings of the 19th International Workshop on Unification (UNIF'05)*, pages 77-92, Nara, Japan, 2005. - 346
- T. Kutsia and M. Marin.

Can context sequence matching be used for XML querying?

Contributed talk at the 19th International Workshop on Unification (UNIF'05), Nara, Japan, April 22 2005. - 347
- T. Kutsia and M. Marin.

Matching with regular constraints.

Technical Report 05-05, RISC Report Series, University of Linz, Austria, 2005. - 348
- T. Kutsia and M. Marin.

Matching with regular constraints.

In G. Sutcliffe and A. Voronkov, editors,*Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference LPAR'05*, volume 3835 of*Lecture Notes in Artificial Intelligence*, pages 215-229, Montego Bay, Jamaica, 2005. Springer Verlag. - 349
- T. Kutsia and M. Marin.

Matching with regular constraints.

Invited talk at Austria-Japan Summer Workshop on Term Rewriting, Obergurgl, Austria, August 10 2005. - 350
- T. Kutsia and M. Marin.

Matching with regular constraints.

Contributed talk at Theorema-Omega'05 Workshop, Saarbrucken, Germany, November 14 2005. - 351
- T. Kutsia and M. Marin.

Matching with regular constraints.

Contributed talk at 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'05), Montego Bay, Jamaica, December 2 2005. - 352
- T. Kutsia and M. Marin.

A rule-based framework for solving regular context sequence constraints.

Technical report, RISC Report Series, University of Linz, Austria, 2006. - 353
- T. Kutsia and M. Marin.

Solving regular constraints for hedges and contexts.

In J. Levy, editor,*Proceedings of 20th International Workshop on Unification, UNIF'06*, pages 89-107, Seattle, USA, 2006. - 354
- T. Kutsia and M. Marin.

Austria-japan workshop on symbolic computation and software verification.

Technical Report 07-09, RISC Report Series, University of Linz, Austria, 2007. - 355
- T. Kutsia and K. Nakagawa.

System description: Interface between Theorema and external automated deduction systems.

Contributed talk at the 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus'01), Siena, Italy, June 2001. - 356
- C. Lindinger.

Using cave technology for the illustration of abstract mathematical concepts.

Master's thesis, Johannes Kepler University Linz, RISC, 2001. - 357
- L. Lukacs.

Automated Analysis of Program Code Properties for Code Search on the Web.

Master's thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 358
- M. Marin.

*Functional Logic Programming with Distributed Constraint Solving*.

PhD thesis, RISC Institute, April 2000. - 359
- M. Marin.

Functional programming with sequence variables: The sequentica package.

In J. Levy, M. Kohlhase, J. Niehren, and M. Villaret, editors,*Proceedings of the 17th International Workshop on Unification (UNIF 2003)*, 2003. - 360
- M. Marin and T. Kutsia.

On the implementation of a rule-based programming system and some of its applications.

In B. Konev and R. Schmidt, editors,*Proceedings of the Fourth International Workshop on the Implementation of Logics*, Almaty, Kazakhstan, 2003. - 361
- M. Marin and T. Kutsia.

Programming with transformation rules.

In T. Jebelean and V. Negru, editors,*Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03)*, Timisoara, Romania, 2003. - 362
- M. Marin and T. Kutsia.

A rule-based approach to the implementation of evaluation strategies.

In D. Petcu, D. Zaharie, V. Negru, and T. Jebelean, editors,*Proceedings of the 6th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04)*, pages 227-241, Timisoara, Romania, Sep 26-30 2004. Mirton Publishing Company. - 363
- M. Marin and T. Kutsia.

A rule-based approach to the implementation of evaluation strategies.

Contributed talk at the 6th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04), Timisoara, Romania, September 2004. - 364
- M. Marin and T. Kutsia.

Foundations of the rule-based system rholog.

*Journal of Applied Non-Classical Logics*, 16(1-2):151-168, 2006. - 365
- M. Marin and F. Piroi.

Deduction and presentation in log.

In F. Kamareddine, editor,*Proceedings of the Mathematical Knowledge Management Symposium*, volume 93 of*ENTCS*, pages 161-182. Heriot-Watt University, Edinburgh, Elsevier, February 2004. - 366
- M. Marin and F. Piroi.

Rule-based programming with mathematica.

In*Proceedings of the 6th International Mathematica Conference, Alberta, Canada*. Wolfram Institute, August 2004.

Also as RICAM report series 2004-16. - 367
- M. Marin and D. Tepeneu.

Programming with Sequence Variables: The Sequentica Package.

In P. Mitic, P. Ramsden, and J. Carne, editors,*Challenging the Boundaries of Symbolic Computation. Proceedings of 5th International Mathematica Symposium (IMS 2003)*, Imperial College, London, 2003. Imperial College Press. - 368
- G. Mayrhofer.

An Inductive Prover for Logical Formulae.

Master's thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 369
- G. Mayrhofer, S. Saminger, and
W. Windsteiger.

Creacomp: Computer-supported experiments and automated proving in learning and teaching mathematics.

In E. Milkova, editor,*Proceedings of ICTMT8, Hradec Kralove, Czech Republic*, July 2007. - 370
- G. Mayrhofer, S. Saminger, and
W. Windsteiger.

Creacomp: Experimental formal mathematics for the classroom.

In D. Wang, editor,*SCE'06 book*. World Scientific, 2007.

Accepted for publication. - 371
- R. Moreno-Diaz, B. Buchberger, and
J. L. Freire, editors.

*EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory- Formal Methods and Tools for Computer Science)*, number 2178 in Lecture Notes in Computer Science, Las Palmas de Gran Canaria, Feb. 19-23 2001. Springer.

ISSN 0302-9743, ISBN 3-540-42959-X. - 372
- K. Nakagawa, editor.

*Logic, Mathematics and Computer Science: Interactions (LMCS' 2002)*. RISC, Linz, October 2002.

ISBN 3-902276-02-9. - 373
- K. Nakagawa.

Logicographic symbol.

Contributed talk at SFB Statusseminar Strobl, Austria, April 2002. - 374
- K. Nakagawa.

*Supporting User-Friendliness in the Mathematical Software System Theorema*.

PhD thesis, Research Institute for Symbolic Computation, January 2002. - 375
- K. Nakagawa.

User-friendly features of mathematical software system Theorema.

Invited talk of the Computer Algebra Seminar at Kobe University, Japan, February 2002. - 376
- K. Nakagawa.

User-friendly features of mathematical software system Theorema.

Invited talk at Kyusyu University, Japan, February 2002. - 377
- K. Nakagawa.

User-friendly features of mathematical software system Theorema.

Invited talk at Fujitsu Laboratories LTD, Japan, March 2002. - 378
- K. Nakagawa.

Variable Shape Logicographic Symbols.

In K. Nakagawa, editor,*Logic, Mathematics and Computer Science: Interactions (LMCS 2002)*, pages 202-216, RISC, Schloss Hagenberg, Austria, October 2002. - 379
- K. Nakagawa.

Logicographic symbols.

*Journal of Symbolic Computation: Special Issue*, 2003. - 380
- K. Nakagawa and B. Buchberger.

Presenting proofs using logicographic symbols.

Contributed talk at Workshop on Proof Transformation and Presentation (PTP-01 in IJCAR-2001), Siena, Italy, June 2001. - 381
- K. Nakagawa and B. Buchberger.

Two tools for mathematical knowledge management in Theorema.

In Buchberger and Caprotti [163].

ISBN 3-902276-00-2. - 382
- K. Nakagawa and B. Buchberger.

Theorema and logicographic symbols.

Workshop of the Researches for Algorithms on Computer Algebra, Research Institute for Mathematical Sciences (RIMS), Kyoto, Japan, 2003. - 383
- K. Nakagawa and B. Buchberger.

Theorema and logicographic symbols.

Seminar in Kyusyu-University, Fukuoka, Japan, 2003. - 384
- H. T. Ping.

Translation of pattern based programs into Lisp.

Master's thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 385
- F. Piroi.

Focus Windows.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2002. - 386
- F. Piroi.

Focus windows: A tool for automated provers.

In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,*Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'02)*, Timisoara, Romania, October 2002.

ISBN 973-585-785-5. - 387
- F. Piroi.

Aspects of proof presentation in Theorema.

Contributed talk at Omega-Theorema Workshop, Hagenberg, Austria, May 2003. - 388
- F. Piroi.

Theorema for the user.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2003. - 389
- F. Piroi.

Tools for using automated provers in mathematical theory exploration.

Technical Report 04-12, RISC Report Series, University of Linz, Austria, August 2004.

PhD Thesis. - 390
- F. Piroi.

*Tools for Using Automated Provers in Mathematical Theory Exploration*.

PhD thesis, Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria, August 2004.

Also available as RISC Tech Report no. 04-12. - 391
- F. Piroi.

User interface features in Theorema: A summary.

In P. Libbrecht, editor,*In Proceedings of ``Mathematical User-Interfaces Workshop'' At the Third Mathematical Knowledge Management Conference, Bialowieza, Poland*, pages 1-16, 2004.

Also available as SFB Technical Report 2004-46. - 392
- F. Piroi and B. Buchberger.

Focus windows: A new technique for proof presentation.

In J. Calmet, B. Benhamou, O. Caprotti, L. Henocque, and V. Sorge, editors,*Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AICS'2002 - Calculemus'2002 Conference.*, volume 2385 of*Lecture Notes in Artificial Intelligence*, pages 290-304, Marseille, France, July 2002. Springer Verlag.

ISBN 3-540-43865-3. - 393
- F. Piroi and B. Buchberger.

Focus Windows: A New Technique for Proof Presentation.

In H. Kredel and W. Seiler, editors,*Proceedings of the 8th Rhine Workshop on Computer Algebra, Mannheim, Germany*, pages 297-313, March 21-22 2002. - 394
- F. Piroi and B. Buchberger.

An environment for building mathematical knowledge libraries.

In W. Windsteiger and C. Benzmueller, editors,*Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, Second International Joint Conference (IJCAR)*, pages 19-29, Cork, Ireland, 4-8 July 2004. - 395
- F. Piroi and B. Buchberger.

Label management in mathematical theories.

Technical Report 2004-16, Johann Radon Institute for Computational and Applied Mathematics (RICAM), November 2004. - 396
- F. Piroi and B. Buchberger.

Label management in Theorema.

In M. Kohlhase, editor,*Informal proceedings of the 4th International Conference on Mathematical Knowledge Management (MKM'05)*, July 2005.

Bremen, Germany. - 397
- F. Piroi and B. Buchberger.

Label management in Theorema.

Contributed talk at 4th International Conference on Mathematical Knowledge Management, July 2005. - 398
- F. Piroi, B. Buchberger,
C. Rosenkranz, and T. Jebelean.

Organisational Tools for MKM in Theorema.

Technical Report 07-11, RISC Report Series, University of Linz, Austria, 2007. - 399
- F. Piroi and T. Jebelean.

Advanced Proof Presentation in Theorema.

In V. Negru and T. Jebelean, editors,*3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), Timisoara, Romania*, October 2001. - 400
- F. Piroi and T. Jebelean.

Advanced Proof Presentation in Theorema.

Technical Report SFB 01-38, Research Institute for Symbolic Computation, J. Kepler University Linz, October 2001. - 401
- F. Piroi and T. Jebelean.

Interactive proving in Theorema.

Contributed talk at the Ninth Workshop on Automated Reasoning (AISB'02), London, UK, April 2002. - 402
- F. Piroi and T. Kutsia.

The Theorema environment for interactive proof development.

In G. Sutcliffe and A. Voronkov, editors,*Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference (LPAR'05)*, volume 3835 of*Lecture Notes in Artificial Intelligence*, pages 261-275, Montego Bay, Jamaica, 2005. Springer Verlag. - 403
- F. Piroi and T. Kutsia.

The Theorema environment for interactive proof development.

Contributed talk at 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'05), Montego Bay, Jamaica, December 3 2005. - 404
- N. Popov.

Operators in recursion theory.

Technical Report 03-06, RISC, 2003. - 405
- N. Popov.

Verification using weakest precondition strategy.

Contributed talk at Computer Aided Verification of Information Systems: A Practical Industry-Oriented Approach (CAVIS'03), Timisoara, Romania, February 2003. - 406
- N. Popov.

A practical approach to verification of recursive programs in Theorema.

Contributed talk at Computer Aided Verification of Information Systems (CAVIS-04), Timisoara, Romania, February 2004. - 407
- N. Popov.

Verification of functional programs in Theorema.

Contributed talk at Fifth Symposium on Trends in Functional Programming (TFP 04), Munich, Germany, November 2004. - 408
- N. Popov.

Verification of recursive programs in Theorema.

Invited colloquium talk at Department of Mathematical Logic, Faculty of Mathematics and Computer Science, Sofia University, Bulgaria, July 2004. - 409
- N. Popov.

Verification of simple recursive programs in Theorema: Completeness of the method.

Contributed talk at 6th International Workshop on Symbolic and Numeric Algorithms in Scientific Computing (SYNASC'04), Timisoara, Romania, September 2004. - 410
- N. Popov.

Functional program verification in Theorema.

Contributed talk at Theorema-Ultra-Omega'05 Workshop, Saarbruecken, Germany, November 14 2005. - 411
- N. Popov.

Verification of simple recursive programs in Theorema: Completeness of the method.

Technical Report 05-06, RISC Report Series, University of Linz, Austria, June 2005. - 412
- N. Popov.

*Functional Program Verification in Theorema*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 413
- N. Popov and T. Jebelean.

A practical approach to verification of recursive programs in Theorema.

In T. Jebelean and V. Negru, editors, - 414
- N. Popov and T. Jebelean.

A practical approach to proving termination of recursive programs in Theorema.

In M. Codish and A. Middeldorp, editors,*Proceedings of 7th International Workshop on Termination*, pages 43-46, Aachen, Germany, June 2004. - 415
- N. Popov and T. Jebelean.

Verification of simple recursive programs: Sufficient conditions.

Technical Report 04-06, RISC Report Series, University of Linz, Austria, June 2004. - 416
- N. Popov and T. Jebelean.

The role of algebraic simplification in the verification of functional programs.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 01 2005. - 417
- N. Popov and T. Jebelean.

Algebraic methods in the verification of recursive programs.

Contributed talk at SFB Statusseminar, Strobl, Austria, April, 20 2006. - 418
- N. Popov and T. Jebelean.

Functional program verification in Theorema - using completeness for debugging.

Contributed talk at INTAS (First Meeting of the INTAS Project), Timisoara, Romania, December 09 2006. - 419
- N. Popov and T. Jebelean.

Supporting functional program verification in Theorema.

Contributed talk at Calculemus, Genova, Italy, July 7 2006. - 420
- N. Popov and T. Jebelean.

Using computer algebra techniques for the specification and verification of recursive programs.

Contributed talk at ACA (Applications of Computer Algebra), Varna, Bulgaria, June 28 2006. - 421
- N. Popov and T. Jebelean.

Verification and synthesis of tail recursive programs in Theorema.

Contributed talk at NWPT (Nordic Workshop on Programming Theory), Reykjavik, Iceland, October 20 2006. - 422
- N. Popov and T. Jebelean.

Automated support for the algorithm validation.

Keynote talk. Contributed talk at New Trends in Mathematics and Informatics, 60 years Institute of Mathematics, Bulgarian Academy of Sciences, July 6 2007. - 423
- N. Popov and T. Jebelean.

Logical aspects of algorithm verification.

Contributed talk at SFB Statusseminar, Strobl, Austria, April, 14 2007. - 424
- N. Popov and T. Jebelean.

Proving termination of recursive programs by matching against simplified program versions and construction of specialized libraries in Theorema.

In D. Hofbauer and A. Serebrenik, editors,*Proceedings of 9-th International Workshop on Termination*, pages 48-52, Paris, France, June 2007. - 425
- N. Popov and T. Jebelean.

Proving termination of recursive programs or how to avoid proving termination.

Contributed talk at INTAS (Second Meeting of the INTAS Project), Moscow, Russia, August 27 2007. - 426
- N. Popov and T. Jebelean.

Using computer algebra techniques for the specification, verification and synthesis of recursive programs.

*Mathematics and Computers in Simulation*, pages 1-13, 2007.

to appear. - 427
- J. Robu.

Mechanical proof of geometry theorems involving inequalities.

Presented at 4th Joint Conference on Pure and Applied Mathematics, June 2001. - 428
- J. Robu.

Systematic Exploration of Geometric Configurations Using Mathematica.

In V. Negru and T. Jebelean, editors,*3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'01), Timisoara, Romania*, October 2001. - 429
- J. Robu.

*Geometry Theorem Proving in the Frame of the Theorema Project*.

PhD thesis, Johannes Kepler University, Linz, 2002. - 430
- J. Robu.

Geometry theorem proving in the frame of Theorema project.

Contributed talk at the 4th International Workshop on Automated Deduction in Geometry (ADG'02), Hagenberg, Austria, September 2002. - 431
- J. Robu.

Systematic exploration of geometric configurations using Mathematica.

In*Analele Universitatii Timisoara*, volume XXXIX of*Seria Matematica-Informatica*, pages 209-216, Timisoara, Romania, 2002. - 432
- J. Robu.

Automated proof of geometry theorems involving order relation in the frame of the Theorema project.

In H. F. Pop, editor,*Knowledge Engineering: Principles and Techniques*, number Special Issue in Studia Universitatis ``Babes-Bolyai'', Series Informatica, pages 307-315, 2007. - 433
- J. Robu, D. Tepeneu, T. Ida,
H. Takahashi, and B. Buchberger.

Computational origami construction of a regular heptagon with automated proof of its correctness.

In H. Hong and D. Wang, editors,*Proceedings of ADG 2004 (The Fifth International Workshop on Automated Deduction in Geometry)*, volume 3763 of*Lecture Notes in Computer Science*, pages 19-33. University of Florida, Gainesville, FL, USA, Springer Berlin / Heidelberg, 2006. - 434
- C. Rosenkranz.

*Retrieval and Structuring of Large Mathematical Knowledge Bases: A Theorema Approach*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 435
- C. Rosenkranz.

The Status Quo of MKM. Current Trends in Knowledge Buildup and Retrieval.

Technical Report 07-13, RISC Report Series, University of Linz, Austria, September 2007. - 436
- C. Rosenkranz, R. Hemmecke,
T. Jebelean, and B. Buchberger.

Mathematical knowledge management in the frame of verification and synthesis of generic algorithms for Gröbner Bases.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 1 2005. - 437
- C. Rosenkranz and F. Piroi.

Organizational tools in Theorema.

Contributed talk at Theorema-Ultra-Omega Workshop, Saarbruecken, Germany, November 14-15 2005. - 438
- M. Rosenkranz.

Equation solving over operator domains.

Talk at the Theorema-Omega Workshop, May 2003. - 439
- M. Rosenkranz.

*The Green's Algebra: A Polynomial Approach to Boundary Value Problems*.

PhD thesis, RISC, University of Linz, 2003. - 440
- M. Rosenkranz.

Symbolic solution of boundary value problems.

Poster at the ISSAC Conference, Philadelphia (USA), August 2003. - 441
- M. Rosenkranz.

Symbolic solution of simple BVPs on the operator level.

*SIGSAM Bulletin*, 37(3):84-87, 2003. - 442
- M. Rosenkranz.

Symbolic solution of simple BVPs on the operator level: A new approach.

In T. Jebelean and V. Negru, editors, - 443
- M. Rosenkranz.

The algorithmization of physics: Math between science and engineering.

In B. Buchberger and J. A. Campbell, editors,*Proceedings of AISC 2004*, volume 3249 of*Lecture Notes in Artificial Intelligence (LNAI)*, pages 1-7, Castle of Hagenberg, Austria, September 2004. Springer.

Invited talk. - 444
- M. Rosenkranz.

New symbolic method for solving linear two-point boundary value problems on the level of operators.

*Journal of Symbolic Computation*, 39(2):171-199, 2004. - 445
- M. Rosenkranz, B. Buchberger, and
H. W. Engl.

Computing the Moore-Penrose-inverse by Gröbner bases.

Conference on Computational Methods for Inverse Problems Strobl, Austria, August 2002. - 446
- M. Rosenkranz, B. Buchberger, and
H. W. Engl.

Solving linear boundary value problems via non-commutative Gröbner bases.

Fourth International SYNASC Workshop Timisoara, Romania, October 2002. - 447
- M. Rosenkranz, B. Buchberger, and
H. W. Engl.

Solving Linear Boundary Value Problems Via Non-commutative Gröbner Bases.

In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,*Proceedings of SYNASC 2002, 4th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing*, pages 300-313, Timisoara, Romania, 9-12 October 2002. Mirton Publisher. - 448
- S. Saminger, R. Vajda, and
W. Windsteiger.

Using a computer-algebra system and a theorem prover to stimulate creativity in learning mathematics.

*International Journal of Computers for Mathematical Learning*, 2005.

Submitted. - 449
- Theorema Group.

Theorema: A system for supporting mathematical proving implemented in Mathematica.

Conference of the Association for Symbolic Logic, Chicago, June 2000. - 450
- E. Tomuta.

*An Architecture for Combining Provers and its Applications in the Theorema System*.

PhD thesis, The Research Institute for Symbolic Computation, Johannes Kepler University, 1998.

RISC report 98-14. - 451
- E. Tomuta and B. Buchberger.

Combining Provers in the Theorema System.

Technical report, the Research Institute for Symbolic Computation, Johannes Kepler University, 1998.

RISC report 98-02. - 452
- E. Tomuta and B. Buchberger.

Combining Provers in the Theorema System.

In*Proceedings of the Sixth Rhine Workshop on Computer Algebra, March 31.-April 3, Sankt Augustin, Germany*, 1998. - 453
- E. Tomuta, D. Vasaru, and M. Marin.

Handling Provers Cooperation in Theorema.

In B. Buchberger and T. Jebelean, editors,*Proceedings of the Second International Theorema Workshop*, pages 55-75, 1998.

RISC report 98-10. - 454
- R. Vajda.

Finding Witness Terms in ETRCF by Quantifier Elimination Techniques.

Contributed talk at Theorema-Ultra-Omega'05 Workshop, Saarbruecken, Germany, November 14 2005. - 455
- R. Vajda.

E-training of Formal Mathematics: Report on the CreaComp Project at the University of Linz.

Contributed talk at ACA (Applications of Computer Algebra), Varna, Bulgaria, June 26 2006. - 456
- R. Vajda.

Using Real Quantifier Elimination for Obtaining Witness Terms.

Contributed talk at SFB StatusSeminar, Strobl, Austria, April 20 2006. - 457
- R. Vajda.

Report on the CreaComp Project: Linking Computer Algebra and Automated Reasoning for Providing a New Learning Environment for Elementary Analysis.

Contributed talk at First Central and Eastern European Conference on Computer Algebra and Dynamic Geometry Systems in Mathematics Education (CADGME), Pecs, Hungary, June 21 2007. - 458
- R. Vajda.

*Supporting Exploration in Elementary Analysis by Computational, Graphical and Reasoning Tools*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing. - 459
- R. Vajda and T. Jebelean.

Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis.

Contributed talk at ACA (Applications of Computer Algebra), Varna, Bulgaria, June 28 2006. - 460
- R. Vajda, T. Jebelean, and
B. Buchberger.

Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis.

*Mathematics and Computers in Simulation*, pages 1-11, 2007.

to appear. - 461
- D. Vasaru-Dupré.

*Automated Theorem Proving by Integrating Proving, Solving and Computing*.

PhD thesis, RISC Institute, May 2000.

RISC report 00-19. - 462
- W. Windsteiger.

Building up Hierarchical Mathematical Domains Using Functors in*Mathematica*.

In A. Armando and T. Jebelean, editors,*Electronic Notes in Theoretical Computer Science*, volume 23. Elsevier, 1999.

Calculemus 99 Workshop, Trento, Italy. - 463
- W. Windsteiger.

*Theorema*: Overview on using the system and details on composing hierarchical knowledge bases.

School on Logic and Computation, Edinburgh, England, April 1999. - 464
- W. Windsteiger.

On a solution of the mutilated checkerboard problem using the Theorema set theory prover.

In S. Linton and R. Sebastiani, editors,*Proceedings of the Calculemus 2001 Symposium*, 2001.

Talk given at the Calculemus 2001 workshop, June 21, 2001. - 465
- W. Windsteiger.

On a solution of the mutilated checkerboard problem using the Theorema set theory prover.

Technical Report 01-26, RISC-Linz, 2001. - 466
- W. Windsteiger.

A set theory prover in Theorema.

Talk given at the CAL'01 workshop at the EUROCAST'01, Las Palmas de Gran Canaria, 2001. - 467
- W. Windsteiger.

*A Set Theory Prover in Theorema: Implementation and Practical Applications*.

PhD thesis, RISC Institute, May 2001. - 468
- W. Windsteiger.

Theorema: Ein Rahmen für Mathematik, Algorithmik und Didaktik.

Technical Report 22, RISC, 2001.

In German. - 469
- W. Windsteiger.

An Automated Prover for Set Theory in Theorema.

In O. Caprotti and V. Sorge, editors,*Calculemus 2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning: Work in Progress Papers*, pages 56-67, Marseille, France, June 2002.

Appears in Seki-Report Series Nr. SR-02-04, Universität des Saarlandes. - 470
- W. Windsteiger.

An Automated Prover for Set Theory in Theorema.

Contributed talk at Calculemus'2002, Marseille, France, June 5 2002. - 471
- W. Windsteiger.

An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema.

In K. Nakagawa, editor,*Logic, Mathematics and Computer Science: Interactions (LMCS 2002)*, pages 266-280, RISC, Schloss Hagenberg, Austria, October 2002.

Symposium in Honor of Bruno Buchberger's 60th Birthday, Appears in RISC-report Series Nr. 02-60. - 472
- W. Windsteiger.

An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema.

Contributed talk at LMCS'02, Hagenberg, Austria, October 20 2002. - 473
- W. Windsteiger.

The Theorema System.

Contributed talk at Calculemus Autumn School, Pisa, Italy, September 27 2002. - 474
- W. Windsteiger.

Algorithmic methods 1.

Lecture notes. Available at`http://www.risc.uni-linz.ac.at/people/wwindste/Teaching/AlgMeth1/AktuellerJG/`, 2003. - 475
- W. Windsteiger.

An Automated Prover for Set Theory in Theorema.

Contributed talk at Omega-Theorema Workshop, Hagenberg, Austria, May 26 2003. - 476
- W. Windsteiger.

Exploring an algorithm for polynomial interpolation in the*Theorema*system.

Technical report, Laboratoire d'Informatique de Paris 6, 2003.

Proceedings of Calculemus'03, September 10-12, Rome, Italy. - 477
- W. Windsteiger.

Exploring an algorithm for polynomial interpolation in the*Theorema*system.

In T. Hardin and R. Rioboo, editors,*Calculemus 2003. 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning*, pages 130-136. Aracne, 2003. - 478
- W. Windsteiger.

Exploring an Algorithm for Polynomial Interpolation in the Theorema System.

Contributed talk at Calculemus'2003, Rome, Italy, September 12 2003. - 479
- W. Windsteiger.

Formalizing Mathematics / Computer-supported Mathematics.

Talk at the SFB Statusseminar, Strobl, Austria., April 2003. - 480
- W. Windsteiger.

Mathematica.

In J. Grabmeier, E. Kaltofen, and V. Weispfenning, editors,*Computer Algebra Handbook: Foundations, Applications, Systems*, pages 314-320. Springer, 2003. - 481
- W. Windsteiger.

Predicate logic as a working language.

Lecture notes. Available at`http://www.risc.uni-linz.ac.at/people/wwindste/Teaching/LogikAlsArbeitssprache/`, 2003. - 482
- W. Windsteiger, 2004.
- 483
- W. Windsteiger.

An automated theorem prover for set theory within the Theorema system.

Invited colloquium talk at Institute for Algebra, Charles University Prague, April 25 2005. - 484
- W. Windsteiger.

CreaComp: Neue Möglichkeiten im e-learning für Mathematik.

Invited colloquium talk at Research Net Upper Austria: Brennpunkt Forschung, Austria, 22. April 2005. - 485
- W. Windsteiger.

The creacomp project: Theorema for computer-supported teaching and learning of mathematics.

Contributed talk at Theorema-Ultra-Omega'05 Workshop, Saarbrucken, Germany, November 14 2005. - 486
- W. Windsteiger.

Symbolic solution techniques for the elastoplasticity problem.

Contributed talk at SFB Statusseminar, Strobl, Austria, March 31 2005. - 487
- W. Windsteiger.

Theorema: A system for mathematical theory exploration.

Invited colloquium talk at Institute for Algebra, Charles University Prague, April 26 2005. - 488
- W. Windsteiger.

Wie erfinde ich mathematische algorithmen? wie beweise ich mathematische algorithmen?

Technical Report 05-18, RISC Report Series, University of Linz, Austria, December 2005.

Presentation slides for a presentation given at Schwerpunktfach Mathematik, Europagymnasium Auhof, December 15, 2005. - 489
- W. Windsteiger.

Analytica V: Towards the Mordell-Weil Theorem.

Contributed talk at Calculemus'06, Genova, Italy, July 9 2006. - 490
- W. Windsteiger.

An automated prover for Zermelo-Fraenkel set theory in Theorema.

*JSC*, 41(3-4):435-470, 2006. - 491
- W. Windsteiger.

Computer-supported Proving in ZF Set Theory with the Theorema System.

Invited colloquium talk at Carnegie Mellon University, Math Logic seminar, March 2 2006. - 492
- W. Windsteiger.

Introduction to the Gröbner Bases method.

Talk given in the frame of the seminar ``Fast SAT Solvers and Practical Decision Procedures''. Invited colloquium talk at Carnegie Mellon University, Computer Science Deptartment, April 28 2006. - 493
- W. Windsteiger.

Introduction to Theorema: An example of a formal math system.

Contributed talk at Special Semester on Groebner Bases: Workshop on Formal Groebner Bases Theory. RICAM, Linz, March 6 2006. - 494
- W. Windsteiger.

The Theorema system.

Invited colloquium talk at Carnegie Mellon University, Computer Science seminar, February 20 2006. - 495
- W. Windsteiger.

Creacomp: Computer-supported experiments and automated proving in learning and teaching mathematics.

Contributed talk at 8th International Conference on Technology in Mathematics Teaching (ICTMT8), Hradec Kralove, Czech Republic, July 3 2007. - 496
- W. Windsteiger.

Towards computer-supported proving in maths education.

Contributed talk at First Central and Eastern European Conference on Computer Algebra- and Dynamic Geometry Systems in Mathematics Education (CADGME), Pecs, Hungary, June 21 2007. - 497
- W. Windsteiger, B. Buchberger, and
M. Rosenkranz.

Theorema.

In*The Seventeen Provers of the World*, volume 3600 of*LNAI*, pages 96-107. Springer Berlin Heidelberg New York, 2006. - 498
- A. Zapletal.

*A Compiler for Theorema*.

PhD thesis, RISC, University of Linz, Austria, 2007.

ongoing.

Please direct your comments
or eventual problem reports to webmaster.

SpezialForschungsBereich SFB F013 | Special Research Program of the FWF - Austrian Science Fund

SpezialForschungsBereich SFB F013 | Special Research Program of the FWF - Austrian Science Fund