Publications of the Project F1302

UnpublishedUnInvited

September 27, 2008

UnpublishedUnInvited

September 27, 2008

## Bibliography

- 1
- B. Buchberger.

Computer-Mathematik in der Schule.

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

The*Theorema*project: The current state.

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

Mathematik: Altes Eisen oder Schlüsseltechnologie?

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

Mathematik am Computer: Die nächste Überforderung?

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

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

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

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

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

*Theorema*: A system for supporting mathematical proving.

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

Formal exploration management for Hilbert space theory.

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

Formal Theory Exploration:The Lazy Thinking Paradigm.

Contributed talk at Calculemus Meeting, Pisa, Italy, September 16 2002. - 10
- 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. - 11
- 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. - 12
- B. Buchberger.

Algorithmic algorithm synthesis: Case study Gröbner Bases.

Contributed talk at International Algebra Conference, Moscow State University, May 26 - June 2 2004. - 13
- 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. - 14
- B. Buchberger and D. Vasaru.

The Theorema PCS prover.

Jahrestagung der DMV, Dresden, September 18-22, 2000. - 15
- 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. - 16
- A. Craciun.

THEOREMA: An Overview.

Contributed talk at Scottish Theorem Provers Workshop, Glasgow, UK, December 19 2003. - 17
- 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. - 18
- 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. - 19
- 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. - 20
- 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. - 21
- 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. - 22
- M. Erascu and T. Jebelean.

Verification of imperative programs using forward reasoning.

Contributed talk at SFB Statusseminar, Strobl, Austria, Apr., 11-14 2007. - 23
- M. Giese.

Practical reflection for formal mathematics in Theorema.

Contributed talk at Workshop on Formal Gröbner Bases Theory, Linz, Austria, March 2006. - 24
- T. Jebelean.

Natural style predicate logic proving in Theorema.

ICAI'01: 5th International Conference on Applied Informatics Eger, Hungary, January 2001. - 25
- 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. - 26
- T. Jebelean.

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

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

Exploring mathematics with Theorema.

Contributed talk at International Symposium on Symbolic and Algebraic Computation (ISSAC'03), Philadelphia, USA, August 2003. - 28
- 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. - 29
- 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. - 30
- T. Jebelean and B. Buchberger.

Theorema: A system for the working mathematician.

Contributed talk at SNSC'01, Hagenberg, Austria, September 2001. - 31
- T. Jebelean, L. Kovacs, and N. Popov.

Verification of imperative programs in Theorema.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2003. - 32
- 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. - 33
- 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. - 34
- L. Kovacs.

Combining algebraic and logic techniques for program verification.

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

Automated Loop Invariant Generation by Algebraic Techniques Over the Rationals.

Contributed talk at Alpine Verification Meeting, Aussois, France, April 2007. - 36
- 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. - 37
- 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. - 38
- 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. - 39
- 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. - 40
- 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. - 41
- 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. - 42
- 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. - 43
- 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. - 44
- L. Kovacs and T. Jebelean.

Finding Polynomial Invariants for Imperative Loops.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2006. - 45
- 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. - 46
- L. Kovacs and T. Jebelean.

Algebraic Methods for Invariant Generation.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2007. - 47
- L. Kovacs and N. Popov.

Procedural program verification in Theorema.

Contributed talk at Omega-Theorema Workshop, Hagenberg, Austria, May 25-27 2003. - 48
- 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. - 49
- 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. - 50
- G. Kusper.

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

Conference of PhD Students in Computer Science, Szeged, Hungary, July 2002. - 51
- 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. - 52
- 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. - 53
- T. Kutsia.

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

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

Unification with sequence variables and flexible arity symbols.

Talk at the SFB Statusseminar, Strobl, Austria, April 2002. - 55
- 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. - 56
- 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. - 57
- 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. - 58
- 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. - 59
- T. Kutsia and M. Marin.

Matching with regular constraints.

Contributed talk at Theorema-Omega'05 Workshop, Saarbrucken, Germany, November 14 2005. - 60
- 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. - 61
- 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. - 62
- 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. - 63
- K. Nakagawa.

Logicographic symbol.

Contributed talk at SFB Statusseminar Strobl, Austria, April 2002. - 64
- 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. - 65
- 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. - 66
- K. Nakagawa and B. Buchberger.

Theorema and logicographic symbols.

Seminar in Kyusyu-University, Fukuoka, Japan, 2003. - 67
- F. Piroi.

Focus Windows.

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

Aspects of proof presentation in Theorema.

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

Theorema for the user.

Contributed talk at SFB Statusseminar, Strobl, Austria, April 2003. - 70
- F. Piroi and B. Buchberger.

Label management in Theorema.

Contributed talk at 4th International Conference on Mathematical Knowledge Management, July 2005. - 71
- F. Piroi and T. Jebelean.

Interactive proving in Theorema.

Contributed talk at the Ninth Workshop on Automated Reasoning (AISB'02), London, UK, April 2002. - 72
- 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. - 73
- 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. - 74
- 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. - 75
- N. Popov.

Verification of functional programs in Theorema.

Contributed talk at Fifth Symposium on Trends in Functional Programming (TFP 04), Munich, Germany, November 2004. - 76
- 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. - 77
- N. Popov.

Functional program verification in Theorema.

Contributed talk at Theorema-Ultra-Omega'05 Workshop, Saarbruecken, Germany, November 14 2005. - 78
- 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. - 79
- N. Popov and T. Jebelean.

Algebraic methods in the verification of recursive programs.

Contributed talk at SFB Statusseminar, Strobl, Austria, April, 20 2006. - 80
- 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. - 81
- N. Popov and T. Jebelean.

Supporting functional program verification in Theorema.

Contributed talk at Calculemus, Genova, Italy, July 7 2006. - 82
- 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. - 83
- 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. - 84
- 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. - 85
- N. Popov and T. Jebelean.

Logical aspects of algorithm verification.

Contributed talk at SFB Statusseminar, Strobl, Austria, April, 14 2007. - 86
- 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. - 87
- J. Robu.

Mechanical proof of geometry theorems involving inequalities.

Presented at 4th Joint Conference on Pure and Applied Mathematics, June 2001. - 88
- 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. - 89
- 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. - 90
- C. Rosenkranz and F. Piroi.

Organizational tools in Theorema.

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

Equation solving over operator domains.

Talk at the Theorema-Omega Workshop, May 2003. - 92
- 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. - 93
- 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. - 94
- Theorema Group.

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

Conference of the Association for Symbolic Logic, Chicago, June 2000. - 95
- R. Vajda.

Finding Witness Terms in ETRCF by Quantifier Elimination Techniques.

Contributed talk at Theorema-Ultra-Omega'05 Workshop, Saarbruecken, Germany, November 14 2005. - 96
- 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. - 97
- R. Vajda.

Using Real Quantifier Elimination for Obtaining Witness Terms.

Contributed talk at SFB StatusSeminar, Strobl, Austria, April 20 2006. - 98
- 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. - 99
- 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. - 100
- W. Windsteiger.

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

School on Logic and Computation, Edinburgh, England, April 1999. - 101
- 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. - 102
- W. Windsteiger.

An Automated Prover for Set Theory in Theorema.

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

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

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

The Theorema System.

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

Algorithmic methods 1.

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

An Automated Prover for Set Theory in Theorema.

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

Exploring an Algorithm for Polynomial Interpolation in the Theorema System.

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

Formalizing Mathematics / Computer-supported Mathematics.

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

Predicate logic as a working language.

Lecture notes. Available at`http://www.risc.uni-linz.ac.at/people/wwindste/Teaching/LogikAlsArbeitssprache/`, 2003. - 110
- 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. - 111
- W. Windsteiger.

Symbolic solution techniques for the elastoplasticity problem.

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

Analytica V: Towards the Mordell-Weil Theorem.

Contributed talk at Calculemus'06, Genova, Italy, July 9 2006. - 113
- 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. - 114
- 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. - 115
- 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.

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