Isabela Dramnesc, Tudor Jebelean.Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema. Technical report no. 20-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2020.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema. Technical report no. 20-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2020.[pdf][bib]
Besik Dundua, Temur Kutsia, Mikheil Rukhaia.Unranked Nominal Unification. Technical report no. 20-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2020.[pdf][bib]
2018
T. Jebelean.Experiments with Automatic Proofs in Elementary Analysis. Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2018.Work in progress.[zip][pdf][pdf][bib]
David M. Cerna and Temur Kutsia.Idempotent Generalization is Infinitary. RISC. Technical report, RISC Report, 2018.[pdf][bib]
A. Maletzky, F. Immler.Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version). RISC, JKU Linz. Technical report, May2018.arXiv:1805.00304 [cs.LO].[url][bib]
2017
A. Maletzky.A New Reasoning Framework for Theorema 2.0. RISC, Johannes Kepler University Linz. Technical report, May2017.Accepted as work-in-progress paper at CICM 2017 (10th Conference on Intelligent Computer Mathematics, Edinburgh, UK, July 17-21).[pdf][bib]
Tudor Jebelean, Nikolaj Popov.A Set-Based Approach to Qualitative and Quantitative Estimation of Competencies. Technical report no. 17-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2017.[pdf][bib]
2016
Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayer.An Overview of PρLog. Technical report no. 16-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2016.[pdf][bib]
Manfred Schmidt-Schauss, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal Unification of Higher Order Expressions with Recursive Let. Technical report no. 16-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2016.[pdf][bib]
A. Maletzky.Computer-Assisted Exploration of Gröbner Bases Theory in Theorema. Technical report no. 16-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2016.PhD thesis.[pdf][bib]
2015
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal Anti-Unification. RISC. Technical report no. 15-03, April2015.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean and Sorin Stratulat.Synthesis of Some Algorithms for Trees: Experiments in Theorema. Technical report no. 15-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2015.[pdf][bib]
Boris Konev, Temur Kutsia.Anti-Unification of Concepts in Description Logic EL. Technical report no. 15-20 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2015.[pdf][bib]
A. Maletzky.Exploring Reduction Ring Theory in Theorema. Technical report no. 15-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July2015.[pdf][bib]
Angelos Mantzaflaris, Hamid Rahkooy, Zafeirakis Zafeirakopoulos.Efficient Computation of Multiplicity and Directional Multiplicity of an Isolated Point. Technical report no. 15-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2015.[pdf][bib]
Manuela Wiesinger-Widi.Gröbner Bases and Generalized Sylvester Matrices. Technical report no. 15-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2015.PhD Thesis.[bib]
2014
Alexander Baumgartner, Temur Kutsia.Unranked Second-Order Anti-Unification. RISC, JKU Linz. Technical report no. 14-05, March2014.[pdf][bib]
Alexander Baumgartner, Temur Kutsia.A Library of Anti-Unification Algorithms. Technical report no. 14-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2014.[url][pdf][bib]
Besik Dundua, Mario Florido, Temur Kutsia, Mircea Marin.Constraint Logic Programming for Hedges: A Semantic Reconstruction. Technical report no. 14-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2014.[pdf][bib]
Temur Kutsia, Christophe Ringeissen.Proceedings of the 28th International Workshop on Unification, UNIF 2014. Technical report no. 14-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2014.[url][pdf][bib]
Temur Kutsia, Andrei Voronkov (eds.).Sixth International Symposium on Symbolic Computation in Software Science, SCSS 2014. Short Papers. Technical report no. 14-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2014.[url][pdf][bib]
A. Maletzky, B. Buchberger.Complexity Analysis of the Bivariate Buchberger Algorithm in Theorema. Technical report no. 14-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October2014.[zip][bib]
2013
Laura Kovacs, Temur Kutsia (ed.).Proceedings of the Fifth International Symposium on Symbolic Computation in Software Science, SCSS 2013. Technical report no. 13-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2013.[pdf][bib]
Hamid Rahkooy, Zafeirakis Zafeirakopoulos.On Computing Elimination Ideals Using Resultants with Applications to Groebner Bases. Research Institute for Symbolic Computations, Doctoral College Computational Mathematics. Technical report, 2013.[url][bib]
2012
Tudor Jebelean, Anna Medve.Formalization of Workflows Using Fork-Join Automata. Technical report no. 12-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2012.[pdf][bib]
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.A Variant of Higher-Order Anti-Unification. Technical report no. 12-19 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Semi-automatic Synthesis of Some Sorting Programs in Theorema. Research Institute for Symbolic Computation (RISC), University of Linz. Technical report no. 12-01, Schloss Hagenberg, 4232 Hagenberg, Austria, January2012.RISC Report Series.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Systematic Exploration of the Theory of Lists in Theorema. Technical report no. 12-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2012.RISC Report Series.[pdf][bib]
Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia.A Dynamic Pattern Calculus with Hedge Variables. Technical report no. 12-20 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Madalina Erascu.Computational Logic and Quantifier Elimination Techniques for (Semi-)automatic Static Analysis and Synthesis of Algorithms. Technical report no. 12-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Temur Kutsia, Mircea Marin.Solving, Reasoning, and Programming in Common Logic. Technical report no. 12-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
Temur Kutsia, Mircea Marin.Regular Expression Order-Sorted Unification and Matching. Technical report no. 12-14 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2012.[pdf][bib]
2011
Isabela Dramnesc, Tudor Jebelean.Automated Reasoning on Tuples - Case Studies in Proof Based Synthesis. Technical report no. 11-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July2011.[pdf][bib]
Madalina Erascu.Symbolic Computation and Program Verification. Proving Partial Correctness and Synthesizing Optimal Algorithms. Technical report no. 11-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2011.[pdf][bib]
Temur Kutsia, Jordi Levy, Mateu Villaret.Anti-Unification for Unranked Terms and Hedges. Technical report no. 11-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2011.[pdf][bib]
Loredana Tec.Computing and Proving with Integro-Differential Polynomials in Theorema. Technical report no. 11-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2011.[bib]
Loredana Tec.A Symbolic Framework for General Polynomial Domains in Theorema: Applications to Boundary Problems. Research Institute for Symbolic Computation. Technical report no. 11-09, July2011.PhD Thesis.[bib]
Manuela Wiesinger-Widi.Sylvester Matrix and GCD for Several Univariate Polynomials. Technical report no. 11-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2011.[pdf][bib]
Manuela Wiesinger-Widi.Towards Computing a Groebner Basis of a Polynomial Ideal over a Field by Using Matrix Triangularization. Technical report no. 11-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2011.[pdf][bib]
2010
Isabela Dramnesc, Tudor Jebelean and Adrian Craciun.Case Studies in Systematic Exploration of Tuple Theory. Technical report no. 10-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2010.[pdf][bib]
Isabela Dramnesc and Tudor Jebelean.Proof Based Synthesis of Sorting Algorithms. Technical report no. 10-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July2010.[pdf][bib]
Jorge Coelho, Besik Dundua, Mario Florido, Temur Kutsia.A Rule-Based Approach to XML Processing and Web Reasoning. Technical report no. 10-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2010.[pdf][bib]
Madalina Erascu, Tudor Jebelean.A Purely Logical Approach to Imperative Program Verification. Technical report no. 10-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2010.[pdf][bib]
Tudor Jebelean, Gabor Kusper.Experiments with Multi-Domain Logic: Variable Merging and Split Strategies. Technical report no. 10-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2010.[pdf][bib]
Maria Alpuente (ed.).Proceedings of the 20th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2010. Technical report no. 10-14 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2010.[pdf][bib]
T. Jebelean, M. Mosbah, N. Popov (eds.).Proceedings of SCSS 2010 Symbolic Computation in Software Science. Technical report no. 10-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2010.[pdf][bib]
Dietmar Kerbl.An automated induction prover for finite sets implemented in the Theorema system. Technical report no. 10-24 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October2010.[pdf][bib]
2009
Camelia Rosenkranz, Bruno Buchberger, Tudor Jebelean.Knowledge Archives in Theorema: A Logic-Internal Approach. Technical report no. 09-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2009.[ps][pdf][bib]
B. Buchberger, R. McCasland, A. Craciun.Automatheo 2009: Proceedings of the Workshop on Automated Mathematical Theory Exploration. Technical report no. 09-12 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2009.[bib]
Mircea Marin, Temur Kutsia.Computational Methods in an Algebra of Regular Hedge Expressions. Technical report no. 09-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March2009.[pdf][bib]
Günther Mayrhofer.Symbolic Computation Prover with Induction. Technical report no. 09-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2009.Master Thesis.[pdf][bib]
Camelia Rosenkranz.Retrieval and Structuring of Large Mathematical Knowledge Bases in Theorema. Technical report no. 09-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2009.[pdf][bib]
Vajda Robert.Supporting Exploration in Elementary Analysis by Computational, Graphical and Reasoning Tools. Technical report no. 09-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2009.[pdf][bib]
2008
Tom Schrijvers, Frank Raiser, Thom Frühwirth.CHR 2008, Fifth Workshop on Constraint Handling Rules. Technical report no. 08-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2008.[url][pdf][bib]
Aart Middeldorp.WRS 2008, 8th International Workshop on Reduction Strategies in Rewriting and Programming. Technical report no. 08-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2008.[url][pdf][bib]
Bruno Buchberger, Tetsuo Ida, Temur Kutsia.Austrian-Japanese Workshop on Symbolic Computation in Software Science, SCSS 2008. Technical report no. 08-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2008.[url][pdf][bib]
Florina Piroi, Bruno Buchberger, Camelia Rosenkranz.Mathematical Journals as Reasoning Agents: Literature Review. Technical report no. 08-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March2008.[pdf][nb][bib]
Camelia Rosenkranz, Bruno Buchberger, Tudor Jebelean.Mathematical Knowledge Archives in Theorema. Technical report no. 08-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2008.[pdf][bib]
Adrian Craciun.Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory. Technical report no. 08-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2008.[pdf][bib]
Madalina Erascu.Automated Formal Static Analysis and Retrieval of Source Code. Technical report no. 08-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2008.[pdf][bib]
Mircea Marin.UNIF 2008, The 22nd International Workshop on Unification. Submitted to the RISC Report Series. 2008.[url][pdf][bib]
Alexander Zapletal.Compilation of Theorema Programs. Technical report no. 08-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2008.[pdf][bib]
2007
Martin Giese, Bruno Buchberger.Towards Practical Reflection for Formal Mathematics. Technical report no. 07-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2007.[pdf][bib]
Martin Giese, Bruno Buchberger.Towards Practical Reflection for Formal Mathematics, extended abstract. In Proceedings of Austria-Japan Workshop on Symbolic Computation and Software Verification. RISC. Technical report no. 07-09, July 12007.pages 30-34.[pdf][bib]
Florina Piroi, Bruno Buchberger, Camelia Rosenkranz, Tudor Jebelean.Organisational Tools for MKM in Theorema. Technical report no. 07-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2007.[ps][bib]
M. Hodorog, A. Craciun.A Case Study in Systematic Theory Exploration: Natural Numbers. Technical report no. 07-18 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October2007.RISC, University of Linz, Austria.[pdf][bib]
M. Erascu, T. Jebelean.Verification of Imperative Programs using Symbolic Execution and Forward Reasoning in the Theorema System. RISC Linz. Technical report no. 07-12, July 12007.Presented at First Austria-Japan Workshop on Symbolic Computation and Software Verification, Linz, Austria, July 1st 2007.[pdf][bib]
M. Giese, T. Jebelean.Proc. Workshop on Invariant Generation, WING 2007. Technical report no. 07-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).062007.Workshop Proceedings.[pdf][bib]
Manuel Kauers, Manfred Kerber, Robert Miner, Wolfgang Windsteiger.Calculemus/MKM 2007 - Work in Progress. Technical report no. 07-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2007.[ps][pdf][bib]
L. Kovacs.Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. Technical report no. 07-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).PhD Thesis,October2007.[bib]
Temur Kutsia, Mircea Marin.Austria-Japan Workshop on Symbolic Computation and Software Verification. Technical report no. 07-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2007.[pdf][bib]
Camelia Rosenkranz.The Statusquo of MKM. Current Trends in Knowledge Buildup and Retrieval. Technical report no. 07-13 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2007.[ps][bib]
2006
B. Buchberger, E.P. Klement, G. Pilz, S. Saminger, W. Windsteiger.CreaComp: e-Schulung von Kreativität und Problemlösekompetenz. Technical report no. 06-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2006.[pdf][bib]
L. Kovacs, T. Jebelean.Finding Polynomial Invariants for Imperative Loops in the Theorema System. Technical report no. 03-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2006.[pdf][bib]
L. Kovacs, T. Jebelean, D. Kapur.Using Symbolic Summation and Polynomial Algebra for Imperative Program Verification in Theorema. RISC-Linz. Technical report, 2006.submitted to MatCom Journal.[pdf][bib]
Temur Kutsia, Mircea Marin.A Rule-Based Framework for Solving Regular Context Sequence Constraints. Submitted to the RISC Report Series. 2006.[pdf][bib]
2005
Temur Kutsia, Bruno Buchberger.Predicate Logic with Sequence Variables and Sequence Function Symbols. Technical report no. 05-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2005.[pdf][bib]
L. Kovacs.Using Combinatorial and Algebraic Techniques for Automatic Generation of Loop Invariants. Technical report no. 05-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2005.[zip][bib]
Temur Kutsia, Mircea Marin.Matching with Regular Constraints. Technical report no. 05-05 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).2005.[pdf][bib]
N. Popov.Verification of Simple Recursive Programs in Theorema: Completeness of the Method. Technical report no. 05-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2005.[pdf][bib]
G. Regensburger.Parametrizing compactly supported orthonormal wavelets by discrete moments. J. Kepler University Linz. Technical report, 2005.SFB Report.[bib]
W. Windsteiger.Wie erfinde ich mathematische Algorithmen? Wie beweise ich mathematische Algorithmen?. Technical report no. 05-18 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2005.Presentation slides for a presentation given at Schwerpunktfach Mathematik, Europagymnasium Auhof, December 15, 2005.[nb][pdf][bib]
2004
F. Piroi, B. Buchberger.Label Management in Mathematical Theories. Johann Radon Institute for Computational and Applied Mathematics (RICAM). Technical report no. 2004-16, November2004.[bib]
B. Buchberger, K. Nakagawa.Mathematical Knowledge Editor: A Research Plan. Johannes Kepler University Linz. Technical report, SFB Report, 2004.Spezialforschungsbereich SF013 "Scientific Computing", FWF (Austrian National Science Foundation).[nb][bib]
B. Buchberger.A Note on Automated Generation of an Algorithm Verification Method. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2004-03, SFB Report, March2004.[pdf][bib]
B. Buchberger.Computer-Supported Mathematical Theory Exploration: Schemes, Failing Proof Analysis, and Metaprogramming. Submitted to the RISC Report Series. Juni2004.[bib]
A. Craciun, B. Buchberger.Algorithm Synthesis Case Studies: Sorting of Tuples by Lazy Thinking. Technical report no. 04-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October2004.[ps][bib]
A. Craciun, B. Buchberger.Preprocessed Lazy Thinking: Synthesis of Sorting Algorithms. Technical report no. 04-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October2004.[ps][bib]
Nikolaj Popov, Tudor Jebelean.Verification of Simple Recursive Programs: Sufficient Conditions. Technical report no. 04-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2004.[pdf][ps][ps][bib]
2003
B. Buchberger.Groebner Rings in Theorema: A Case Study in Functors and Categories. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2003-49, SFB Report, November2003.[nb][bib]
B. Buchberger.Algorithm Retrieval: Concept Clarification and Case Study in Theorema. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2003-44, SFB Report, October2003.[nb][bib]
M. Rosenkranz, B. Buchberger, H. W. Engl.A Symbolic Algorithm for Solving Two-Point BVPs on the Operator Level. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2003-41, SFB Report, October2003.[pdf][bib]
B. Buchberger.Algorithm Invention and Verification by Lazy Thinking. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2003-29, SFB Report, October2003.[nb][bib]
B. Buchberger, T. Ida.Origami Theorem Proving. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2003-23, SFB Report, October2003.[pdf][bib]
B. Buchberger.Focus Windows: A New Approach to Presenting Mathematical Proofs (In Automated Proving Systems). Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 2003-22, SFB Report, October2003.[pdf][ps][bib]
Mircea Marin, Florina Piroi.Rule-based deduction and views in Mathematica. Johannes Kepler University, Linz, Spezialforschungsbereich F013, Numerical and Symbolic Scientific Computing. Technical report no. 2003-43, October2003.Eds.: T. Jebelean, J. Schicho.[url][bib]
2002
Florina Piroi, Bruno Buchberger.Focus Windows: A New Technique for Proof Presentation. Technical report no. 02-25 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2002.[ps][bib]
F. Piroi, B. Buchberger.Focus Windows: A New Technique for Proof Presentation. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 02-32, SFB Report, December2002.[pdf][bib]
A. Craciun, B. Buchberger.Proving the Correctness of the Merge-Sort Algorithm with Theorema. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 02-31, SFB Report, December2002.[bib]
Temur Kutsia.Unification in a Free Theory with Sequence Variables and Flexible Arity Symbols and its Extensions. Johannes Kepler University, Linz, Austria. Technical report no. 02-6, 2002.SFB Report.[bib]
2001
Bruno Buchberger, Olga Caprotti.MKM'01. First International Workshop on Mathematical Knowledge Management. Technical report no. 01-31 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).September2001.[tar.gz][ps][bib]
K. Nakagawa, B. Buchberger.Two Tools for Mathematical Knowledge Management in Theorema. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 01-37, SFB Report, December2001.[bib]
K. Nakagawa, B. Buchberger.Presenting Proofs Using Logicographic Symbols. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 01-35, SFB Report, December2001.[bib]
Wolfgang Windsteiger.Theorema: Ein Rahmen fuer Mathematik, Algorithmik und Didaktik. Technical report no. 01-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2001.Course for mathematics teachers given in the frame of the ``Tag der Mathematik 2001'' at the University of Linz, November 23, 2001. In German.[ps][tar.gz][bib]
Wolfgang Windsteiger.A Set Theory Prover within Theorema. Technical report no. 01-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2001.Also available as SFB report 01-23.[ps][bib]
2000
B. Buchberger, D. Vasaru, T. Jebelean.The Theorema System: Current Status and the Proving-Solving-Computing Cycle. Technical report no. 00-37 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2000.[ps][bib]
B. Buchberger, U.Langer.Annual Report of the SFB F013: 1.11.99-31.12.99. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 00-06, SFB Report, March2000.[bib]
B. Buchberger.Focus Windows: A New Technique for Presenting Mathematical Proofs (in Automated Theorem Proving Systems). Research Institute for Symbolic Computation, Johannes Kepler University Linz. Technical report no. 2000-01-30, Theorema Technical Report, 2000.[ps][abstract][pdf][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Theorema System: Proving, Solving, and Computing for the Working Mathematician. Technical report no. 00-38 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).August2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Natural Style Provers of Theorema: A Survey of Strategies for Different Mathematical Domains. Technical report no. 00-39 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
B. Buchberger, C. Dupre, T. Jebelean, B. Konev, F. Kriftner, T. Kutsia, K. Nakagawa, F. Piroi, D. Vasaru, W. Windsteiger.The Facilities of Theorema for Teaching Logic and Mathematics. Technical report no. 00-41 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2000.[ps][bib]
Daniela Vasaru Dupre.Automated Theorem Proving by Integrating Proving, Solving and Computing. Technical report no. 00-19 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2000.PhD Thesis.[zip][bib]
1999
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Progress Report. Technical report no. 99-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[ps][bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Short Demo. Technical report no. 99-45 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[tar.gz][bib]
Bruno Buchberger.Computer-Mathematik in der Schule. Technical report no. 99-39 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.[zip][bib]
Bruno Buchberger.Views on the Future of Computer Science. Technical report no. 99-40 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.[ppt.gz][bib]
Bruno Buchberger.Mathematics: The Technology of Reasoning. Technical report no. 99-41 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.[ppt.gz][bib]
Bruno Buchberger, Tudor Jebelean.Distance Teaching of Mathematics Using Theorema. Technical report no. 99-43 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report No. 99-36, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[doc][bib]
Bruno Buchberger.Theory Exploration Versus Theorem Proving. Technical report no. 99-46 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July1999.Also available as SFB Report No. 99-38, Johannes Kepler University Linz, Spezialforschungsbereich F013, December 1999.[tar.gz][bib]
B. Buchberger.Mathematik am Computer: Die naechste Ueberforderung? (Mathematics on the Computer: The Next Overtaxation?). Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 99-39, SFB Report, December1999.Annual Conference of the Austrian Mathematical Society, Graz, Austria, September 24, 1999.[bib]
B. Buchberger, U.Langer.Annual Report of the SFB F013: 1.4.98-31.12.98. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 99-02, SFB Report, March1999.[bib]
Wolfgang Windsteiger.Theorema: Overview on Using the System and Details on Composing Hierarchical Knowledge Bases. Technical report no. 99-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1999.Presented at the Edinburgh School in Logic and Computation.[tar.gz][bib]
1998
Bruno Buchberger, Klaus Aigner, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Mircea Marin, Koji Nakagawa, Ovidiu Podisor, Elena Tomuta, Yaroslav Usenko, Daniela Vasaru, Wolfgang Windsteiger.Theorema: An Integrated System for Computation and Deduction in Natural Style. Technical report no. 98-25 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1998.Also available as SFB Report No. 98-06.[ps][bib]
B. Buchberger, W. Windsteiger.The Theorema Language: Implementing Object- and Meta-Level Usage of Symbols. SFB F013 Numerical and Symbolic Scientific Computing. Technical report no. 98-07, 1998.[pdf][bib]
Ulrich Langer, Bruno Buchberger.Numerical and Symbolic Scientific Computing. Technical report no. 98-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1998.FWF proposal (SFB).[ps][bib]
Elena Tomuta, Bruno Buchberger.Combining Provers in the Theorema System. Technical report no. 98-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January1998.Presented at the Sixth Rhine Workshop on Computer Algebra, March 31-April 3, 1998, Sankt Augustin, Germany. Also available as SFB Report No. 98-01.[ps][bib]
Bruno Buchberger, Tudor Jebelean.The Second International Theorema Workshop. Technical report no. 98-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1998.[bib]
B. Buchberger, T. Jebelean, D. Vasaru.Theorema: A System for Formal Scientific Training in Natural Language Presentation. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 98-05, SFB Report, June1998.[bib]
B. Buchberger.Theorema: Theorem Proving for the Masses Using Mathematica. Johannes Kepler University Linz, Spezialforschungsbereich F013. Technical report no. 98-04, SFB Report, June1998.Worldwide Mathematica Conference, Chicago, USA, June 20, 1998.[bib]
B. Buchberger, T. Ida, W. Schreiner.Knowledge Web: A Design and Feasibilty Study. Institute of Information Sciences and Electronics, University of Tsukuba. Technical report, 1998.ISE-TR-98-151.[bib]
1997
Bruno Buchberger, Tudor Jebelean, Franz Kriftner, Mircea Marin, Elena Tomuta, Daniela Vasaru.A Survey of the Theorema Project. Technical report no. 97-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March1997.[ps][bib]
Bruno Buchberger, Wolfgang Schreiner.CONCERT: A Software Architecture for Coordinating Education. Technical report no. 97-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February1997.[ps][bib]
Bruno Buchberger, Tudor Jebelean, Daniela Vasaru.Theorema: A System for Formal Scientific Training in Natural Language Presentation. Technical report no. 97-34 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).October1997.[bib]
Bruno Buchberger, Tetsuo Ida, Daniela Vasaru.First International Theorema Workshop. Technical report no. 97-20 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1997.Proceedings of the workshop, including also some older papers for reference.[bib]
1996
Bruno Buchberger.Symbolic Computation: Computer Algebra and Logic. Technical report no. 96-36 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[ps][bib]
Bruno Buchberger.Introduction to Groebner Bases. Technical report no. 96-39 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[bib]
Bruno Buchberger.Mathematica as a Rewrite Language. Technical report no. 96-40 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1996.[bib]
1994
Editors: B. Buchberger, S. Stifter, J. Volkert, P. Zinterhof.Workshop PARAGRAPH'94 (Collection of Abstracts). Technical report no. 94-17 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.[bib]
Bruno Buchberger.Symbolic Computation: Foundations and Applications. Technical report no. 94-34 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1994.Published in Presented at GAMM'94, April 6, 1994, Braunschweig, Germany..[bib]
1991
Bruno Buchberger, Hoon Hong.Speeding-up Quantifier Elimination by Groebner Bases. Technical report no. 91-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February1991.[pdf][bib]
1983
B. Buchberger.A Critical-Pair/Completion Algorithm in Reduction Rings. Technical report no. 83-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).1983.[pdf][bib]
B. Buchberger.Miscellaneous Results on the Groebner-Bases for Polynomial Ideals II. Department of Computer And Information Sciences, University of Delaware. Technical report no. 83-1, 1983.[bib]
1981
B. Buchberger.Computer-unterstuetzter mathematisches Problemloesen: Eine Uebersicht (Computer-Aided Mathematical Problem Solving: A Survey). CAMP-LINZ (Computer-Aided Mathematical Problem Solving), Johannes Kepler University, Linz, Austria. Technical report no. Camp-Publ.-Nr.: 81-9.0, October1981.Lecture Notes, October 1981.[bib]
B. Buchberger.H-bases and Groebner-Bases for Polynomial Ideals. CAMP-LINZ (Computer-Aided Mathematical Problem Solving), Johannes Kepler University, Linz, Austria. Technical report no. Camp-Publ.-Nr.: 81-2.0, Internal Report, February1981.[bib]
1980
B. Buchberger.Ein Fallstudie in systematischer Algorithmenentwicklung und Algorithmenverifikation: Ein Algorithmus für ein Nimmspiel (A Case Study in Systematic Algorithm Development and Algorithm Verification: An Algorithm for the Game of Nim). Johannes Kepler University, Technisch-Naturwissenschaftliche Fakultaet, Institut fuer Mathematik. Technical report no. 162, February1980.[bib]
1979
B. Buchberger, R. Neubauer, H. Rolletschek, G. Seeber.A Note on Some Variants of the Notion of Creative Set. Johannes Kepler University, Technisch-Naturwissenschaftliche Fakultaet, Insitut fuer Mathematik. Technical report no. 139, July1979.[bib]
B. Buchberger, F. Winkler.Miscellaneous Results on the Construction of Groebner-Bases for Polynomial Ideals. Johannes Kepler University, Technisch-Naturwissenschaftliche Fakultaet, Insitut fuer Mathematik. Technical report no. 137, June1979.[bib]
1977
B. Buchberger, W. Menzel.Simulation-Universal Automata. Universitaet Karlsruhe, Fakultaet fuer Informatik I. Technical report no. 14/77, 1977.[bib]
1976
B. Buchberger.Eine Bemerkung zu rekursiven Komponenten und 1-1-Splintern (A Remark on Recursive Components and 1-1 Splinters). University of Linz, Institute for Mathematics. Technical report, September1976.[bib]
1975
B. Buchberger.Einige Resultate ueber universelle Automaten (Some Results on Universal Automata). Mathematisches Forschungsinstitut Oberwolfach. Technical report no. 46|1975, Tagunsbericht, Automatentheorie und Formale Sprachen, pp. 6-7, November 24-281975.[bib]
B. Buchberger.Some Results on Universal Automata and Input/Output Codings. Hochschule Linz, Technische-Naturwissenschaftliche Fakultaet, Institut fuer Mathematik. Technical report no. 34, November1975.[bib]
1973
B. Buchberger, F. Jenewein.Implementierung einer Metasprache zur Definition von Programmiersprachen (Implementation of a Meta-language for the Definition of Programming Languages). Institut fuer Informatik und Numerische Mathematik, Universitaet Innsbruck. Technical report no. 228 (ZUSE Z 23V), Programmbibliothek, November1973.[bib]
B. Buchberger.On Certain Decompositions of Goedel Numberings. Institut fuer Informatik, Universitaet Innsbruck. Technical report, 1973.(Appeared in Archiv fuer Mathematische Logik und Grundlagenforschung).[bib]
1972
B. Buchberger, B.Roider.A Study on Universal Functions. Institut fuer Numersiche Mathematik und Elektronische Informationsverarbeitung, Universitaet Innsbruck. Technical report no. 72-5, December1972.[bib]
B. Buchberger.A Basic Problem in the Thoery of Programming Languages. Institut fuer Numersiche Mathematik und Elektronische Informationsverarbeitung Universitaet Innsbruck. Technical report no. 72-1, February1972.[pdf][bib]
1971
B. Buchberger.A Comment on Blum's Signal Function. Institut fuer Numerische Mathematik und Elektronische Informationsverarbeitung, Universitaet Innsbruck. Technical report no. 71-3, August1971.[pdf][bib]
1969
B. Buchberger.Grundbegriffe der Algorithmentheorie (Basic Notions of Algorithm Theory). Angewandte Mathematik, Universitaet und Technische Hochschule Graz. Technical report, October 6-91969.Steiermaerkisches Mathematisches Symposium, Grottenhof-Hardt.[pdf][bib]