RISC Publications and Technical Reports of research area 'Theorema'
2023
Mircea Marin, Temur Kutsia, Cleo Pau, Mikheil Rukhaia.Enumerating All Maximal Clique-Partitions of an Undirected Graph. In: Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Horatiu Cheval, Laurentiu Leustean, and Andrei Sipos (ed.), pp. 65-79.2023.[doi][bib]
2022
Besik Dundua, Temur Kutsia, Mikheil Rukhaia.Unranked Nominal Unification. In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Proceedings of 13th International Tbilisi Symposium on Logic, Language, and Computation, Lecture Notes in Computer Science13206, pp. 279-296.2022.Springer,ISBN 978-3-030-98478-6.[doi][pdf][bib]
2021
I. Dramnesc, T. Jebelean.AlCons: Deductive Synthesis of Sorting Algorithms in Theorema. In: Theoretical Aspects of Computing - ICTAC 2021, A. Cerone, P. Csaba Ölveczky (ed.), Proceedings of 18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan, LNCS12819, pp. 314-333.September 2021.Springer,978-3-030-85315-0.[pdf][bib]
Besik Dundua, Temur Kutsia, Mircea Marin.Variadic equational matching in associative and commutative theories.Journal of Symbolic Computation106, pp. 78-109.2021.Elsevier,ISSN 0747-7171.[doi][pdf][bib]
2020
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, Mircea Marin, Cleopatra Pau.Constraint Solving over Multiple Similarity Relations. In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs)167, pp. 30:1-30:19.2020.Schloss Dagstuhl-Leibniz-Zentrum für Informatik,ISBN 978-3-95977-155-9, ISSN 1868-8969.[doi][bib]
Besik Dundua, Temur Kutsia, Mircea Marin, Cleo Pau.Extending the 𝜌Log Calculus with Proximity Relations. In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics334, pp. 83-100.2020.Springer,ISBN 978-3-030-56356-1, 978-3-030-56355-4.[doi][pdf][bib]
Besik Dundua, Temur Kutsia, Mircea Marin, Mikheil Rukhaia.Specification and Analysis of ABAC Policies in a Rule-Based Framework. In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics334, pp. 101-116.2020.Springer,ISBN 978-3-030-56356-1, 978-3-030-56355-4.[doi][pdf][bib]
Mircea Marin, Besik Dundua, Temur Kutsia.A Rule-Based System for Computation and Deduction in Mathematica. In: WRLA 2020: Rewriting Logic and Its Applications, Santiago Escobar, Narciso Martí-Oliet (ed.), Lecture Notes in Computer Science12328, pp. 57-74.2020.Springer,ISBN 978-3-030-63595-4, 978-3-030-63594-7.[doi][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]
2019
Besik Dundua, Temur Kutsia, Mircea Marin.Variadic Equational Matching. In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen (ed.), Lecture Notes in Computer Science11617, pp. 77-92.2019.Springer,ISBN 978-3-030-23249-8.[pdf][bib]
Mircea Marin, Temur Kutsia, Besik Dundua.A Rule-based Approach to the Decidability of Safety of ABACα. In: Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019, Florian Kerschbaum, Atefeh Mashatan, Jianwei Niu, Adam J. Lee (ed.), pp. 173-178.2019.ACM,ISBN 978-1-4503-6753-0.[doi][pdf][bib]
2018
N. Amiridze, T. Kutsia.Anti-Unification and Natural Language Processing. In: Fifth Workshop on Natural Language and Computer Science, NLCS’18, A. Asudeh, V. de Paiva, L. Moss (ed.), EasyChair preprints203, pp. 1-12.2018.[doi][pdf][bib]
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques.Journal of Symbolic Computation90, pp. 3-41.2018.Elsevier,07477171.[doi][bib]
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. In: Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17), Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef (ed.), Proceedings of CICM 2018, Lecture Notes in Computer Science11006, pp. 178-193.2018.Springer,ISBN 978-3-319-96811-7.The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16.[doi][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]
Temur Kutsia, Cleo Pau.Proximity-Based Generalization. In: 32nd International Workshop on Unification, UNIF 2018, Mauricio Ayala-Rincon and Philippe Balbiani (ed.), pp. - .2018.[pdf][bib]
2017
Alexander Baumgartner, Temur Kutsia.Unranked Second-Order Anti-Unification.Information and Computation255(2), pp. 262-286.2017.ISSN: 0890-5401.[doi][bib]
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Higher-Order Pattern Anti-Unification in Linear Time. Journal of Automated Reasoning58(2), pp. 293-310.2017.ISSN 0168-7433.[doi][bib]
Bruno Buchberger.Gröbner Bases Computation by Triangularizing Macaulay Matrices.Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)75, pp. 1-9.2017.Mathematical Society of Japan,0.[bib]
Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna Maria , Brain Martin , Buchberger Bruno , Cimatti Alessandro , Davenport James , England Matthew , Fontaine Pascal , Forrest Stephen , Griggio Alberto , Kröning Daniel , Seiler Werner M. , Sturm .Satisfiability Checking and Symbolic Computation.ACM Communications in Computer Algebra50(4), pp. 145-147.2017.0.[bib]
Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayr.An overview of PρLog. In: Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017, Y. Lierler and W. Taha (ed.), Lecture Notes in Computer Science10137, pp. 34-49.2017.Springer,ISBN 978-3-319-51675-2.[pdf][bib]
Mauricio Ayala-Rincon, Besik Dundua, Temur Kutsia, Mircea Marin.Rewriting Logic from a ρLog Point of View. In: Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) , Sandra Alves and Renata Wasserman (ed.), pp. -.2017.[pdf][bib]
Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia.Pattern-Based Calculi with Finitary Matching.Logic Journal of the IGPL, pp. -.2017.Oxford University Press,ISSN 1367-0751.To appear.[doi][bib]
E. Abraham, T. Jebelean.Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks. In: ICAI 2017: 10th International Conference on Applied Informatics, G. Kusper (ed.), Proceedings of ICAI 2017: 10th International Conference on Applied Informatics, pp. 0-0.2017.ISBN 0.In print.[url][pdf][bib]
Manfred Schmidt-Schauss, Temur Kutsia, Jordy Levy, Mateu Villaret.Nominal Unification of Higher Order Expressions with Recursive Let. In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, M. Hermenegildo and P. Lopez-Garcia (ed.), LNCS10184, pp. 328-344.2017.Springer,ISBN 978-3-319-63138-7.[pdf][bib]
Johannes Blömer, Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos, editors.Mathematical Aspects of Computer and Information Sciences.Lecture Notes in Computer Science10693,2017.Springer,ISBN 978-3-319-72452-2.[doi][bib]
A. Maletzky, W. Windsteiger.The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema. In: Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke (ed.), Lecture Notes in Computer Science10383, pp. 25-39.2017.Springer,ISBN 978-3-319-62075-6.doi 10.1007/978-3-319-62075-6_3.[url][pdf][bib]
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
Bruno Buchberger.Stam's Identities Collection: A Case Study for Math Knowledge Bases. In: Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Gert-Martin Greuel, Thorsten Koch, Peter Paule and Andrew Sommese (ed.), pp. 437-442.2016.Springer International Publishing,Cham,978-3-319-42432-3.[doi][pdf][bib]
Bruno Buchberger.The GDML and EuKIM Projects: Short Report on the Initiative. In: Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Gert-Martin Greuel, Thorsten Koch, Peter Paule and Andrew Sommese (ed.), pp. 443-446.2016.Springer International Publishing,Cham,978-3-319-42432-3.[doi][pdf][bib]
Erika Abraham, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm.Satisfiability Checking meets Symbolic Computation (Project Paper).CoRRabs/1607.08028, pp. -.2016.-.[url][pdf][bib]
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Proof-based Synthesis of Sorting Algorithms for Trees. In: Proceedings of LATA 2016, the 10th International Conference on Language and Automata Theory and Applications, Adrian-Horia Dediu, Jan Janousek, Carlos Martin-Vide, Bianca Truthe (ed.), Proceedings of LATA 2016, LNCS9618, pp. 562-575.2016.Springer,ISBN 978-3-319-29999-0.[bib]
Isabela Dramnesc and Tudor Jebelean, Sorin Stratulat.A case study on algorithm discovery from proofs: The insert function on binary trees. In: 11th IEEE International Symposium on Applied Computational Intelligence and Informatics, SACI 2016, Timisoara, Romania, May 12-14, 2016, IEEE (ed.), pp. 231-236.2016.978-1-5090-2380-6.[doi][bib]
Besik Dundua, Mario Florido, Temur Kutsia, Mircea Marin.CLP(H): Constraint Logic Programming for Hedges.Theory and Practice of Logic Programming16(2), pp. 141-162.2016.ISSN 1471-0684.[url][bib]
Mircea Marin, Temur Kutsia, Besik Dundua.A rewrite-based computational model for functional logic programming. In: Proceedings of the 7th International Symposium on Symbolic Computation in Software Science, SCSS 2016, James H. Davenport (ed.), EPiC Series in Computing39, pp. 95-106.2016.EasyChair,ISSN 2398-7340.[url][bib]
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]
B. Dundua, T. Kutsia, K. Reisenberger-Hagmayr.PρLog: Combining Logic Programming with Conditional Transformation Systems (Tool Description). In: Technical Communications of the 32nd International Conference on Logic Programming, ICLP 2016, M. Carro, A. King, N. Saeedloei, and M. De Vos (ed.), OpenAccess Series in Informatics (OASIcs)52, pp. 10.1-10.5.2016.Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,ISBN 978-3-95977-007-1, ISSN 2190-6807.[url][bib]
Boris Konev, Temur Kutsia.Anti-Unification of Concepts in Description Logic EL. In: Proceedings of the 15th International Conference on Principles of Knowledge Representation and Reasoning, KR 2016, Chitta Baral, James P. Delgrande, Frank Wolter (ed.), pp. 227-236.April 25-292016.AAAI Press,Cape Town, South Africa,978-1-57735-755-1.[url][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]
Bruno Buchberger, Tudor Jebelean, Temur Kutsia, Alexander Maletzky, Wolfgang Windsteiger.Theorema 2.0: Computer-Assisted Natural-Style Mathematics.JFR9(1), pp. 149-185.2016.ISSN 1972-5787.[doi][bib]
A. Maletzky.Mathematical Theory Exploration in Theorema: Reduction Rings. In: Intelligent Computer Mathematics (Proceedings of CICM 2016, Bialystok, Poland, July 25-29), Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura, Frank Tompa (ed.), Proceedings of CICM 2016, Lecture Notes in Artificial Intelligence9791, pp. 3-17.July2016.Springer-Verlag,ISBN 978-3-319-42546-7.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-42547-4_1. Preprint on arXiv: 1602.04339 [cs.SC].[doi][bib]
A. Maletzky.Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0. In: Mathematical Software - ICMS 2016, Gert-Martin Greuel and Peter Paule and Andrew Sommese (ed.), Proceedings of 5th International Congress on Mathematical Software, Berlin, Germany, July 11-14, Lecture Notes in Computer Science9725, pp. 59-66.2016.Springer-Verlag,ISBN 978-3-319-42432-3.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-42432-3_8.[doi][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]
A. Maletzky.Computer-Assisted Exploration of Gröbner Bases Theory in Theorema. RISC, Johannes Kepler University Linz. PhD Thesis.May2016.[bib]
2015
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal Anti-Unification. RISC. Technical report no. 15-03, April2015.[pdf][bib]
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal Anti-Unification. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15, Maribel Fernandez (ed.), Leibniz International Proceedings in Informatics (LIPIcs), pp. 57-73.2015.ISSN 1868-8969.[pdf][bib]
Alexander Baumgartner.Anti-Unification Algorithms: Design, Analysis, and Implementation. RISC, JKU Linz. PhD Thesis.September2015.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Combinatorial Techniques for Proof-based Synthesis of Sorting Algorithms. In: SYNASC 2015: Proceedings of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Laura Kovacs (ed.), pp. 137-144.2015.IEEE Computer Society,ISBN 978-0-7695-5742-2.[bib]
Isabela Dramnesc, Tudor Jebelean.Synthesis of list algorithms by mechanical proving.Journal of Symbolic Computation69, pp. 61-92.2015.ISSN 0747-7171.[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]
Isabela Dramnesc, Tudor Jebelean.A Case Study in Proof Based Synthesis of Algorithms on Monotone Lists. In: The 10th International Symposium on Applied Computational Intelligence and Informatics, . (ed.), Proceedings of SACI 2015, pp. 483-488.2015.IEEE Xplore,_.[bib]
Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat.Theory Exploration of Binary Trees. In: The IEEE 13th Jubilee International Symposium on Intelligent Systems and Informatics, . (ed.), Proceedings of SISY 2015, pp. 139-144.2015.IEEE Xplore,..[bib]
Besik Dundua, Mario Florido, Temur Kutsia.Lambda Calculus with Regular Types. In: Proceeding of the 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2015, , pp. -.2015.To appear.[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]
Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos.Constructing Orthogonal Designs in Powers of Two: Groebner Bases Meet Equational Unification. In: Proceedings of the 26th International Conference on Rewriting Techniques and Applications, RTA'15, Maribel Fernandez (ed.), Leibniz International Proceedings in Informatics (LIPIcs), pp. 241-256.2015.Schloss Dagstuhl,ISSN 1868-8969.[pdf][bib]
A. Maletzky.Automated Reasoning in Reduction Rings using the Theorema System. In: Computer Algebra in Scientific Computing, Vladimir P. Gerdt and Wolfram Koepf and Werner M. Seiler and Evgenii V. Vorozhtsov (ed.), Proceedings of CASC 2015 (September 14-18, Aachen, Germany), LNCS9301, pp. 305-319.2015.Springer-Verlag Berlin Heidelberg,ISSN 0302-9743.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-24021-3_23.[doi][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]
A. Maletzky.Verifying Buchberger's Algorithm in Reduction Rings. In: Proceedings of the 4th International Seminar on Program Verification, Automated Debugging, and Symbolic Computation, Tudor Jebelean and Dongming Wang (ed.), Proceedings of PAS'2015, Beijing, China, October 21-23, pp. 16-23.October2015.??.arXiv:1604.08736 [cs.SC].[url][bib]
Temur Kutsia, Mircea Marin.Regular Expression Order-Sorted Unification and Matching.Journal of Symbolic Computation67, pp. 42-67.2015.ISSN 0747-7171.[doi][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]
H. Rahkooy.Dual Space Algorithms for Computing Multiplicity Structure of Isolated Points. RISC, JKU Linz. PhD Thesis.July2015.[bib]
Manuela Wiesinger-Widi.Gröbner Bases and Generalized Sylvester Matrices. Johannes Kepler University Linz. PhD Thesis.072015.[url][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.Unranked Second-Order Anti-Unification. In: Proceedings of the 21st Workshop on Logic, Language, Information and Computation, WoLLIC 2014 , Ulrich Kohlenbach (ed.), Lecture Notes in Computer Science8652, pp. 66- 80.2014.Springer,ISBN 978-3-662-44144-2.[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]
Alexander Baumgartner, Temur Kutsia.A library of anti-unification algorithms. In: Proceedings of the 14th European Conference on Logics in Artificial Intelligence, JELIA 2014, Eduardo Ferme and Joao Leite (ed.), Lecture Notes in Computer Science, pp. 543-557.2014.Springer,ISBN 978-3-319-11557-3.[pdf][bib]
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.Nominal anti-unification. In: Proceedings of the 28th International Workshop on Unification, UNIF 2014, Temur Kutsia, Christophe Ringeissen (ed.), pp. 62-68.2014.[pdf][bib]
Isabela Dramnesc, Tudor Jebelean.Theory Exploration of Sets Represented as Monotone Lists. In: Proceedings of SISY 2014 IEEE 12th International Symposium on Intelligent Systems and Informatics, IEEE Xplore (ed.), pp. 163-168.2014. ..[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]
Besik Dundua, Mario Florido, Temur Kutsia, Mircea Marin.Constraint Logic Programming for Hedges: A Semantic Reconstruction. In: Proceedings of the Twelfth International Symposium on Functional and Logic Programming, FLOPS 2014, Michael Codish and Eijiro Sumii (ed.), LNCS8475, pp. 285-301.2014.Springer,ISBN 978-3-319-07150-3.[pdf][bib]
Temur Kutsia, Jordi Levy, Mateu Villaret.Anti-Unification for Unranked Terms and Hedges. Journal of Automated Reasoning52(2), pp. 155-190.2014.ISSN 0168-7433.[doi][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. In: Mathematical Software - ICMS 2014, Hoon Hong and Chee Yap (ed.), Proceedings of The 4th International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-9, 2014, Lecture Notes in Computer Science8592, pp. 41-48.2014.Springer Berlin Heidelberg,ISBN 978-3-662-44198-5.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44199-2_8.[doi][pdf][bib]
B. Buchberger, A. Maletzky.Groebner Bases in Theorema. In: Mathematical Software - ICMS 2014, Hoon Hong and Chee Yap (ed.), Proceedings of The 4th International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-9, 2014, Lecture Notes in Computer Science8592, pp. 374-381.2014.Springer Berlin Heidelberg,ISBN 978-3-662-44198-5.The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-44199-2_58.[doi][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]
W. Windsteiger.Theorema 2.0: A System for Mathematical Theory Exploration. In: Proceedings International Congress on Mathematical Software (ICMS'2014), Seoul, Korea, August 5-8, 2014, Chee Yap and Hoon Hong (ed.), Proceedings of International Congress on Mathematical Software (ICMS'2014), Lecture Notes in Computer Science (LNCS)8592, pp. 49-52.2014.ISBN 978-3-662-44198-5.[url][pdf][bib]
2013
Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret.A Variant of Higher-Order Anti-Unification. In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications, RTA 2013, Femke van Raamsdonk (ed.), Leibniz International Proceedings in Informatics21, pp. 113-127.2013.ISBN 978-3-939897-53-8, ISSN 1868-8969.[url][bib]
Alexander Baumgartner, Temur Kutsia.Unranked Anti-Unification with Hedge and Context Variables. In: Proceedings of the 27th International Workshop on Unification, UNIF 2013, Barbara Morawska, Konstantin Korovin (ed.), pp. 13-21.2013.[url][bib]
Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia.A Confluent Pattern Calculus with Hedge Variables. In: Proceedings of the 2nd International Workshop on Confluence, IWC 2013, Nao Hirokawa, Vincent van Oostrom (ed.), pp. 41-45.2013.[url][bib]
M. Erascu, H. Hong.The Secant-Newton Map is Optimal Among Contracting Quadratic Maps for Square Root Computation. Journal of Reliable Computing18, pp. 73-81.2013.1573-1340.[pdf][bib]
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]
S. El Bedewy.Gesture-Based Browsing of Mathematics. Internationaler Universitätslehrgang Informatics: Engineering and Management (ISI), Johannes Kepler University Linz. Master Thesis.2013.[pdf][bib]
Manfred Kerber, Christoph Lange, Colin Rowat and Wolfgang Windsteiger.Developing an Auction Theory Toolbox. In: AISB 2013, Manfred Kerber, Christoph Lange, Colin Rowat (ed.), pp. 1-4.2013.no ISSN.proceedings available online.[url][pdf][bib]
Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger.A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. In: Conference on Intelligent Computer Mathematics (CICM 2013), Jacques Carette (ed.), Lecture Notes in Artificial Intelligence (LNAI)7961, pp. 200-215.2013.Springer,ISBN 978-3-642-39319-8.[pdf][bib]
2012
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]
Isabela Dramnesc, Tudor Jebelean.Theory Exploration in Theorema: Case Study on Lists. In: Proceedings of the 7th IEEE International Symposium on Applied Computational Intelligence and Informatics, . (ed.), Proceedings of SACI 2012, pp. 421-426.May 24-262012.IEEE Xplore,Obuda University, Budapest, Hungary and "Politehnica" University of Timisoara, Romania,Print ISBN 978-1-4673-1013-0.[bib]
Isabela Dramnesc, Tudor Jebelean.Systematic Exploration of List Theory in Theorema.Scientific Bulletin of the "Politehnica" University of Timisoara, Transactions on Automatic Control and Computer Science(4/2012), pp. 203-210.2012.ISSN 1224-600X.[bib]
Isabela Dramnesc, Tudor Jebelean.Discovery of Inductive Algorithms through Automated Reasoning: A Case Study on Sorting. In: Proceedings of SISY 2012: the IEEE 10th Jubilee International Symposium on Intelligent Systems and Informatics, . (ed.), pp. 293-298.September2012.IEEE Xplore,ISBN 978-1-4673-4751-8.[url][bib]
Isabela Dramnesc, Tudor Jebelean.Automated Synthesis of Some Algorithms on Finite Sets. In: Proceedings of SYNASC 2012: the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, . (ed.), pp. 143-151.September2012.IEEE Computer Society,ISBN-13: 978-0-7695-4934-7.[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]
M. Erascu, T. Jebelean.Soundness of a Logic-Based Verification Method for Imperative Loops. In: Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, A. Voronkov, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. Watt, D. Zaharie (ed.), pp. 127-134.2012.IEEE Computer Society, 978-0-7695-4934-7.[pdf][bib]
Madalina Erascu.Computational Logic and Quantifier Elimination Techniques for (Semi-)automatic Static Analysis and Synthesis of Algorithms. Research Institute for Symbolic Computation. PhD Thesis.2012.RISC Technical Report 12-16.[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.Solving, Reasoning, and Programming in Common Logic. In: Proc. 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2012, Andrei Voronkov (ed.), pp. 119-126.2012.IEEE Computer Society,ISBN 978-0-7695-4934-7.[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]
Ph. Kügler, W. Windsteiger.Algorithmische Methoden - Funktionen, Matrizen, Multivariate Polynome.Reihe: Mathematik kompakt.1st edition,May2012.Birkhäuser Basel Boston Berlin,ISBN 978-3-7643-8515-6.[url][bib]
W. Windsteiger.Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System. In: 24th OpenMath Workshop, 7th Workshop on Mathematical User Interfaces (MathUI), and Intelligent Computer Mathematics Work in Progress, James Davenport and Johan Jeuring and Christoph Lange and Paul Libbrecht (ed.), CEUR Workshop Proceedings921, pp. 73-81.2012.Aachen,1613-0073.[url][pdf][bib]
W. Windsteiger.Theorema 2.0: A Graphical User Interface for a Mathematical Assistant System. In: Proceedings 10th International Workshop On User Interfaces for Theorem Provers, Bremen, Germany, July 11th 2012, Cezary Kaliszyk and Christoph Lüth (ed.), Proceedings of UITP 2012, Electronic Proceedings in Theoretical Computer Science118, pp. 72-82.2012.Open Publishing Association,ISBN 2075-2180 (ISSN).doi: 10.4204/EPTCS.118.5.[url][bib]
2011
Markus Rosenkranz, Georg Regensburger, Loredana Tec, Bruno Buchberger.Symbolic Analysis for Boundary Problems: From Rewriting to Parametrized Groebner Bases. In: Numerical and Symbolic Scientific Computing: Progress and Prospects, Ulrich Langer and Peter Paule (ed.), pp. 273-331.2011.Springer, Wien,ISBN 978-3-7091-0793-5.Also available as RICAM Report 2010-05, September 2010.[pdf][bib]
Bruno Buchberger, Manuel Kauers.Buchberger's Algorithm.Scholarpedia6(10), pp. 7764-7764.October2011.1941-6016.[url][bib]
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]
Isabela Dramnesc, Tudor Jebelean .Proof Techniques for Synthesis of Sorting Algorithms. In: Proceedings of the 13th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, D. Wang, V. Negru, T. Ida, T. Jebelean, D. Petcu, S. Watt and D. Zaharie (ed.), pp. 101-109.September2011.IEEE Computer Society,ISBN 978-0-7695-4630-8.[url][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]
Tudor Jebelean, Gabor Kusper.SAT Solving Experiments in Multi-Domain Logic. In: ICAI 2001, Emod Kovacs (ed.)I, pp. 95-105.2011.Eger, Hungary,0.[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]
Temur Kutsia, Jordi Levy, Mateu Villaret.Anti-Unification for Unranked Terms and Hedges. In: Proceedings of the 22st International Conference on Rewriting Techniques and Applications, RTA 2011, Manfred Schmidt-Schauss (ed.), Leibniz International Proceedings in Informatics (LIPIcs)10, pp. 219-234.2011.Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl Publishing,ISBN 978-3-939897-30-9, ISSN 1868-8969.[url][bib]
N. Popov, T. Jebelean.Sound and Complete Verification Condition Generator for Functional Recursive Programs.. In: Numerical and Symbolic Scientific Computing: Progress and Prospects, U. Langer and P. Paule (ed.), pp. 219-256.2011.Springer,Wien,ISBN 978-3-7091-0793-5.[bib]
Marek Sacha.Structuring and Reusing Knowledge in the Theorema System. Internationaler Universitätslehrgang Informatics: Engineering and Management (ISI), Johannes Kepler University Linz. Diploma Thesis.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.Groebner Bases and Generalized Sylvester Matrices.ACM Communications in Computer Algebra45(2), pp. -.June2011.Accepted extended abstract from ISSAC 2011 poster presentation.[pdf][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]
Manfred Kerber, Colin Rowat, and Wolfgang Windsteiger.Using Theorema in the Formalization of Theoretical Economics. In: Intelligent Computer Mathematics, James H. Davenport, William M. Farmer, Florian Rabe, Josef Urban (ed.), Proceedings of CICM 2011, Lecture Notes in Artificial Intelligence (LNAI)6824, pp. 58-73.2011.Springer,ISSN 0302-9743.[doi][pdf][bib]
2010
Loredana Tec, Georg Regensburger, Markus Rosenkranz and Bruno Buchberger.An Automated Confluence Proof for an Infinite Rewrite System Parametrized over an Integro-Differential Algebra. In: Mathematical Software - ICMS 2010, Third International Congress on Mathematical Software, Kobe, Japan, September 13-17, Komei Fukuda and Joris van der Hoeven and Michael Joswig and Nobuki Takayama (ed.), Proceedings of ICMS, Lecture Notes in Computer Science6327, pp. 245-248.2010.Springer,978-3-642-15581-9.[pdf][bib]
Bruno Buchberger, Manuel Kauers.Groebner Bases.Scholarpedia5(10), pp. 7763-7763.October2010.ISSN 1941-6016.[url][bib]
N. Popov, T. Jebelean, B. Buchberger.From Program Verification to Automated Debugging. In: Workshop on Symbolic Computation in Software Science, T. Jebelean and M. Mosbah and N. Popov (ed.), Proceedings of SCSS 2010, pp. 55-65.July2010.RISC-Linz Report Series,Johannes Kepler University of Linz, Austria,..[bib]
Isabela Dramnesc, Tudor Jebelean, Adrian Craciun.A Case Study in Systematic Exploration of Tuple Theory. In: Workshop of Symbolic Computation in Software Science, Tudor Jebelean, Mohamed Mosbah, Nikolaj Popov (ed.), Proceedings of SCSS 2010 Symbolic Computation in Software Science, Hagenberg1/10-10, pp. 82-95.29-30 July2010.RISC-Linz Report Series,Johannes Kepler University of Linz, Austria,.[pdf][bib]
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]
Isabela Dramnesc, Tudor Jebelean.A Case Study in Proof Based Synthesis of Sorting Algorithms. In: Analele Universitatii de Vest, Timisoara, D.Gaspar, D.Zaharie, B.Buchberger, D.Burghelea, G.Cassier (ed.), Proceedings of 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2010), Matematica - InformaticaXLVIII/3, pp. 47-58.23-26 September2010.West University of Timisoara, Romania,ISSN-1841-3293.[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]
Besik Dundua, Temur Kutsia, Mircea Marin.Strategies in P$\rho$Log.Electronic Proceedings in Theoretical Computer Science, pp. 32-43.2010.ISSN 2075-2180 .[pdf][bib]
Jorge Coelho, Besik Dundua, Mario Florido and Temur Kutsia.A Rule-Based Approach to XML Processing and Web Reasoning. In: Proceedings of the 4th International Conference on Web Reasoning and Rule Systems, RR 2010, Pascal Hitzler and Thomas Lukasiewicz (ed.), Lecture Notes in Computer Science6333, pp. 164-172.2010.Springer,ISSN 0302-9743, ISBN 978-3-642-15917-6.[url][bib]
Madalina Erascu, Tudor Jebelean.A Purely Logical Approach to Program Termination. In: Proceedings of the 11th International Workshop on Termination, Peter Schneider-Kamp (ed.), Proceedings of Federated Logic Conference, Edinburgh, 9-21 July, pp. - .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]
M. Erascu, T. Jebelean.A Purely Logical Approach to the Termination of Imperative Loops. In: Proceedings of the 12th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, T. Ida, V. Negru, T. Jebelean, D. Petcu, S. M. Watt, D. Zaharie (ed.), pp. 142-149.September2010.IEEE Computer Society, 978-0-7695-4324-6.[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]
Temur Kutsia, Jordi Levy, Mateu Villaret. On the Relation Between Context and Sequence Unification.Journal of Symbolic Computation45(1), pp. 74-95.2010.ISSN 0747-7171.[pdf][bib]
Mircea Marin, Temur Kutsia.On the Computation of Quotients and Factors of Regular Languages.Frontiers of Computer Science in China4(2), pp. 173-184.2010.Springer,ISSN 1673-7350.[url][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]
Mircea Marin and Temur Kutsia.Regular Hedge Language Factorization Revisited. In: Proceedings of the 14th International Conference on Developments in language Theory, DLT 2010, Sheng Yu (ed.), Lecture Notes in Computer Science6224 , pp. 328-339.2010.Springer,ISSN 0302-9743, ISBN 978-3-642-14454-7.[url][bib]
Temur Kutsia and Mircea Marin.Order-Sorted Unification with Regular Expression Sorts. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, Christopher Lynch (ed.), Leibniz International Proceedings in Informatics (LIPIcs)6, pp. 193-208.2010.Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl Publishing,ISSN 1868-8969, ISBN 978-3-939897-18-7.[url][bib]
Mircea Marin, Temur Kutsia.Linear Systems for Regular Hedge Languages. In: Advances in Databases and Information Systems, Associated Workshops and Doctoral Consortium of the 13th East European Conference, ADBIS 2009. Revised Selected Papers , Janis Grundspenkis, Marite Kirikova, Yannis Manolopoulos, Leonids Novickis (ed.), Lecture Notes in Computer Science5968, pp. 104-112.2010.Springer,ISSN 0302-9743, ISBN 978-3-642-12081-7.[pdf][bib]
A. Anisimov, T. Jebelean, A. Lyaletski, N. Popov.Projects of Evidence Algorithm and Theorema. In: Theoretical and Applied Aspects of Program Systems Development, A. Anisimov, V. Redko (ed.), pp. 54-58.October2010.Kiev, Ukraine,..[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]
N. Popov, T. Jebelean.Proving Partial Correctness and Termination of Mutually Recursive Programs. In: SYNASC 2010, T. Ida, V. Negru, T. Jebelean, D. Petcu, S. Watt, and, D. Zaharie (ed.), Proceedings of Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 153-158.September2010.IEEE ,ISBN 978-0-7695-4324-6.[pdf][bib]
Dietmar Kerbl.An automated induction prover for finite sets implemented in the Theorema system. RISC, Johannes Kepler University Linz. Diploma Thesis.October2010.[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]
R. Vajda, T. Jebelean, B. Buchberger.Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis.Mathematics and Computers in Simulation79(8), pp. 2310-2316.April2009.Elsevier,ISSN: 0378-4754.Special Issue on Nonstandard Applications of Computer Algebra.[url][pdf][bib]
Markus Rosenkranz, Georg Regensburger, Loredana Tec, Bruno Buchberger.A Symbolic Framework for Operations on Linear Boundary Problems. In: Proceedings of the 11th International Workshop on Computer Algebra in Scientific Computing , Gerdt, Vladimir P.; Mayr, Ernst W.; Vorozhtsov, Evgenii H. (ed.), Proceedings of CASC '09, Kobe, Japan, LNCS5743, pp. 269-283.September2009.Springer-Verlag,ISBN: 978-3-642-04102-0.Also available as RICAM Report 09-10, May 2009.[url][bib]
Tudor Jebelean, Bruno Buchberger, Temur Kutsia, Nikolaj Popov, Wolfgang Schreiner, Wolfgang Windsteiger.Automated Reasoning. In: Hagenberg Research, B. Buchberger, M. Affenzeller, A. Ferscha, M. Haller, T. Jebelean, E.P. Klement, P. Paule, G. Pomberger, W. Schreiner, R. Stubenrauch, R. Wagner, G. Weiss, W. Windsteiger (ed.), pp. 63-101.2009.Springer Dordrecht Heidelberg London New York,ISBN 978-3-642-02126-8.[url][bib]
Peter Paule, Bruno Buchberger, Lena Kartashova, Manuel Kauers, Carsten Schneider, Franz Winkler.Algorithms in Symbolic Computation. In: Hagenberg Research, Bruno Buchberger et al. (ed.), Chapter 1, pp. 5-62.2009.Springer,978-3-642-02126-8.[doi][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]
Besik Dundua, Temur Kutsia, Mircea Marin.Strategies in P$\rho$Log. In: 9th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'09), Maribel Fernandez (ed.), pp. 19-25.2009.-.[pdf][bib]
Madalina Erascu, Tudor Jebelean.A Calculus for Imperative Programs: Formalization and Implementation. In: Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing , S. Watt, V. Negru, T. Ida, T. Jebelean, D. Petcu, D. Zaharie (ed.), pp. 77- 84.2009.IEEE , 978-0-7695-3964-5.[pdf][bib]
Jorge Coelho, Mario Florido, Temur Kutsia.Collaborative Schema Construction using Regular Sequence Types. In: Proceedings of the 2009 IEEE International Conference of Information Reuse and Integration (IRI'09), Kang Zhang, Reda Alhajj (ed.), pp. 290-295.2009.ISBN 978-1-4244-4114-3 .[pdf][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]
Temur Kutsia, Mircea Marin.Order-Sorted Unification with Regular Expression Sorts. In: Proc. UNIF/ADDCT 2009, Christopher Lynch et al. (ed.), pp. 2-16.2009.-.[pdf][bib]
Temur Kutsia, Mircea Marin.Matching of Order-Sorted Terms with Regular Expression Sorts and Second-Order Variables . In: Proc. SCSS 2009, Adel Bouhoula, Tetsuo Ida (ed.), pp. -.2009.-.[bib]
Günther Mayrhofer.Symbolic Computation Prover with Induction. Johannes Kepler University. Diploma Thesis.September2009.[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]
N. Popov, T. Jebelean.Using Computer Algebra Techniques for the Specification, Verification and Synthesis of Recursive Programs.Mathematics and Computers in Simulation79(8), pp. 2293-2301.April2009.Elsevier,ISSN: 0378-4754.[pdf][bib]
N. Popov, T. Jebelean.Verification of Mutual Recursive Functional Programs. In: Proceedings of Workshop on Symbolic Computation in Software Science SCSS'09, T. Ida, A. Bouhoula (ed.), pp. 120-122.September2009.Carthage, Tunisia,..[pdf][bib]
N. Popov, T. Jebelean.Functional Program Verification in Theorema. Soundness and Completeness. In: Proceedings of 15th Biennial Workshop on Programmiersprachen und Grundlagen der Programmierung KPS'09, J. Knoop, A. Prantl (ed.), pp. 221-229.October2009.Maria Taferl, Austria,..[pdf][bib]
N. Popov, T. Jebelean.A Complete Method for Algorithm Validation. In: Proceedings of the Workshop on Automated Mathematical Theory Exploration AUTOMATHEO'09, B. Buchberger, R. McCasland, A. Craciun (ed.), pp. 21-25.June2009.Hagenberg, Austria,-.[pdf][bib]
Georg Regensburger, Markus Rosenkranz, Johannes Middeke.A skew polynomial approach to integro-differential operators. In: Proceedings of ISSAC 2009, Jeremy R. Johnson, Hyungju Park, Erich Kaltofen (ed.), Proceedings of Symbolic and Algebraic Computation, International Symposium, ISSAC 2009, pp. 287-294.2009.ACM,978-1-60558-609-0.[url][pdf][bib]
Camelia Rosenkranz.Retrieval and Structuring of Large Mathematical Knowledge Bases in Theorema. Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria. PhD Thesis.Available as RISC Technical Report 09-04,February2009.[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]
Zsuzsanna Sinka.Interactive Tools for Inspecting Proofs in Theorema. International Studies in Informatics: Engineering & Management (ISI Hagenberg). Diploma Thesis.July2009.Master's Thesis.[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]
Vajda Robert.An e-learning environment for elementary analysis: combining computer algebra, graphics and automated reasoning .Teaching Mathematics and Computer Science7(1), pp. 13-34.2009.University of Debrecen, Hungary,ISSN 1589 - 7389.[bib]
Vajda Robert.Supporting Exploration in Elementary Analysis by Computational, Graphical and Reasoning Tools. Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria. PhD Thesis.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]
B. Buchberger, G. Regensburger, M. Rosenkranz, L. Tec.General Polynomial Reduction with Theorema Functors: Applications to Integro-Differential Operators and Polynomials .SIGSAM Bulletin42(3), pp. 135-137.September2008.ISSN 0163-5824.Extended abstract from ISSAC 2008 poster presentation.[url][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]
Adrian Craciun.Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory. Research Institute for Symbolic Computation (RISC). PhD Thesis.2008.[pdf][bib]
Madalina Erascu, Tudor Jebelean.Practical Program Verification by Forward Symbolic Execution: Correctness and Examples. In: Austrian-Japan Workshop on Symbolic Computation in Software Science, Bruno Buchberger, Tetsuo Ida, Temur Kutsia (ed.)08-08, pp. 47-56.2008.RISC Report Series, University of Linz, Austria,[pdf][bib]
Madalina Erascu.Automated Formal Static Analysis and Retrieval of Source Code. International School for Informatics - Johannes Kepler University . Diploma Thesis.August2008.in RISC Raport Series 08-21.[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]
Tudor Jebelean, Gabor Kusper.Multi-Domain Logic and its Applications to SAT. In: SYNASC 2008, V. Negru et. al. (ed.), Proceedings of International Simposium on Symbolic and Numeric Scientific Computation, pp. 3-8.2008.IEEE Society Press,978-0-7695-3523-4.[pdf][bib]
Temur Kutsia.Flat Matching.JSC43(12), pp. 858-873.2008.ISSN 0747-7171.[url][pdf][bib]
Mircea Marin.UNIF 2008, The 22nd International Workshop on Unification. Submitted to the RISC Report Series. 2008.[url][pdf][bib]
N. Popov, T. Jebelean.A Prototype Environment for Verification of Recursive Programs. In: FORMED'08, Z. Istenes (ed.), Proceedings of Formal Methods in Computer Science Education, Budapest, Hungary, ENTCS, pp. 121-130.March2008.Elsevier,..[pdf][bib]
Nikolaj Popov.Functional Program Verification in Theorema. RISC, Johannes Kepler University. PhD Thesis.July2008.Technical report no. 08-12 in RISC Report Series.[pdf][bib]
N. Popov, T. Jebelean.Verification of Functional Programs Containing Nested Recursion . In: SCSS'08, B. Buchberger, T. Ida and T. Kutsia (ed.), Proceedings of Austrian-Japan Workshop on Symbolic Computation in Software Science, Hagenberg, Austria, pp. 163-175.July2008...[pdf][bib]
E. Kartashova, C. Raab, Ch. Feurer, G. Mayrhofer, W. Schreiner.Symbolic Computations for Nonlinear Wave Resonances. In: "Extreme Ocean Waves", E. Pelinovsky, Ch. Kharif (ed.), pp. 97-128.2008.Springer,ISBN: 978-1-4020-8313-6.[url][pdf][bib]
W. Windsteiger.Stimulating Students' Creativity Through Computer-Supported Experiments and Automated Theorem Proving. In: Promoting Creativity for all Students in Mathematics Education, Emiliya Velikova, Agnis Andzans (ed.), pp. 351-357.2008.8 Studentska Str., 7017 Rousse, Bulgaria,University of Rousse, Bulgaria,ISBN 978-954-712-420-2.Proceedings of Discussion Group 9, the 11th International Congress on Mathematical Education (ICME 11).[pdf][bib]
Ph. Kügler, W. Windsteiger.Algorithmische Methoden - Zahlen, Vektoren, Polynome.Reihe: Mathematik kompakt.1st edition,December2008.Birkhäuser Basel Boston Berlin,ISBN: 978-3-7643-8434-0.[url][bib]
Alexander Zapletal.Compilation of Theorema Programs. RISC, Johannes Kepler University Linz. PhD Thesis.May2008.[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]
A. Craciun, M. Hodorog.Decompositions of Natural Numbers: From A Case Study in Mathematical Theory Exploration. In: Proceedings of the 9th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC07), D. Petcu, V. Negru, D. Zaharie and T. Jebelean (ed.), pp. 1-8.26-29 September2007.West University of Timisoara, Romania,ISBN: 0-7695-3078-8.[pdf][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]
Martin Giese.First-Order Logic. In: Verification of Object-Oriented Software: The KeY Approach, Bernhard Beckert and Reiner Hähnle and Peter H. Schmitt (ed.), Chapter 2, LNCS4334, pp. 21-68.2007.Springer-Verlag,978-3-540-68977-5.[bib]
B. Beckert, M. Giese, R. Hähnle, V. Klebanov, P. Rümmer, S. Schlager, P. H. Schmitt.The KeY System 1.0 (Deduction Component). In: Proceedings of CADE-21, Bremen, Frank Pfenning (ed.), Proceedings of Conference on Automated Deduction, LNCS4603, pp. 379-384.2007.Springer,Heidelberg,ISBN 978-3-540-73594-6.[pdf][bib]
L. Ruff, T. Jebelean.Functional Based Synthesis of a Systolic Array for GCD Computation. In: Implementation and Application of Functional Languages, Z. Horvath, V. Zsok (ed.), LNCS4449, pp. 37-54.2007.Springer,978-3-540-74129-9.[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.Aligator: a Package for Reasoning about Loops. In: Proc. of 14th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), , pp. -.October2007.Yerevan, Armenia,Short paper. to appear.[bib]
L. Kovacs.Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. In: Proc. of WING'07, RISC, Austria, M. Giese and T. Jebelean (ed.), pp. 56-69.2007.-.RISC Report Series No. 07-07.[bib]
L. Kovacs.Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. RISC, Johannes Kepler University Linz, Austria. PhD Thesis.October2007.RISC Technical Report No. 07-16.[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.Solving Equations with Sequence Variables and Sequence Functions.JSC42(3), pp. 352-388.2007.ISSN 0747-7171.[url][pdf][bib]
T. Kutsia, J. Levy, M. Villaret.Sequence Unification Through Currying. In: Proceedings of the 18th International Conference on Rewriting Techniques and Applications (RTA'07), F. Baader (ed.), Lecture Notes in Computer Science4533, pp. 288-302.2007.ISBN 978-3-540-73447-5.[pdf][bib]
Jorge Coelho, Mario Florido, Temur Kutsia.Sequence Disunification and its Application in Collaborative Schema Construction. In: Web Information Systems - WISE 2007 Workshops, M. Weske, M.-S. Hacid, C. Godart (ed.), Lecture Notes in Computer Science4832, pp. 91-102.2007.Springer,ISSN 0302-9743.[url][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]
G. Mayrhofer, S. Saminger, W. Windsteiger.CreaComp: Experimental Formal Mathematics for the Classroom. In: Symbolic Computation and Education, Shangzhi Li, Dongming Wang, and Jing-Zhong Zhang (ed.), pp. 94-114.2007.World Scientific Publishing Co.,Singapore, New Jersey,ISBN 978-981-277-599-3.[url][pdf][bib]
G. Mayrhofer, S. Saminger, W. Windsteiger.CreaComp: Computer-Supported Experiments and Automated Proving in Learning and Teaching Mathematics. In: Proceedings of ICTMT8, Eva Milkova (ed.), pp. ?-?.2007.ISBN 978-80-7041-285-5.[pdf][bib]
N. Popov, T. Jebelean.Proving Termination of Recursive Programs by Matching Against Simplified Program Versions and Construction of Specialized Libraries in Theorema. In: Proceedings of 9-th International Workshop on Termination, D. Hofbauer, A. Serebrenik (ed.), pp. 48-52.June2007.Paris, France,ISSN-0935-3232.[pdf][bib]
Judit Robu.Automated Proof of Geometry Theorems Involving Order Relation in the Frame of the Theorema Project. In: Knowledge Engineering: Principles and Techniques, Horia F. Pop (ed.), Proceedings of Conference on Knowledge Engineering, Principles and Techniques, KEPT2007, Studia Universitatis "Babes-Bolyai", Series InformaticaSpecial Issue, pp. 307-315.2007.ISSN: 1224-869x.[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
J. Robu, D. Tepeneu, T. Ida, H. Takahashi, B. Buchberger.Computational Origami Construction of a Regular Heptagon with Automated Proof of its Correctness. In: Proceedings of ADG 2004 (The Fifth International Workshop on Automated Deduction in Geometry), Hoon Hong, Dongming Wang (ed.), Lecture Notes in Computer Science3763, pp. 19-33.2006.Springer Berlin / Heidelberg,University of Florida, Gainesville, FL, USA,ISBN 978-3-540-31332-8.[bib]
W. Windsteiger, B. Buchberger, M. Rosenkranz.Theorema. In: The Seventeen Provers of the World, Freek Wiedijk (ed.), Lecture Notes in Artificial Intelligence (LNAI)3600, pp. 96-107.2006.Springer Berlin Heidelberg New York,ISBN 3-540-30704-4.[url][pdf][bib]
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]
B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, W. Windsteiger.Theorema: Towards Computer-Aided Mathematical Theory Exploration.Journal of Applied Logic4(4), pp. 470-504.2006.ISSN 1570-8683.[doi][pdf][bib]
M. Hodorog, A. Craciun.Scheme-Based Systematic Exploration of Natural Numbers. In: Proc. of the 8th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC06), D. Petcu, V. Negru, D. Zaharie, T. Jebelean (ed.), pp. 23-34.26-29 September2006.Department of Computer Science, West University of Timisoara, Romania,ISBN:0-7695-2740-X.[pdf][bib]
Guenther Fuchs.Logic Foundation of Geometry and Didactics. RISC, Johannes Kepler University Linz. PhD Thesis.2006.[bib]
Martin Giese.Saturation up to Redundancy for Tableau and Sequent Calculi. In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th Intl. Conf., LPAR 2006, Phnom Penh, Cambodia, Miki Hermann and Andrei Voronkov (ed.), Proceedings of LPAR06, LNCS4246, pp. 182-196.2006.Springer,3540482814.[pdf][bib]
T. Jebelean, L. Kovacs, N. Popov.Experimental Program Verification in the Theorema System.Int. Journal on Software Tools for Technology Transfer (STTT), pp. _-_.2006.Springer, ISSN: 1433-2779 (Paper) 1433-2787 (Online).in press.[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.Finding Polynomial Invariants for Imperative Loops in the Theorema System. In: Proceedings of Verify'06 Workshop, IJCAR'06, The 2006 Federated Logic Conference, S. Autexier and H. Mantel (ed.), pp. 52-67.August 15-162006.[url][pdf][bib]
L. Kovacs, N. Popov, T. Jebelean.Combining Logic and Algebraic Techniques for Program Verification in Theorema. In: Proceedings ISOLA 2006, T. Margaria, A. Philippou, B. Steffen (ed.), Proceedings of Second International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2006), pp. 59-68.November2006.IEEE,Paphos, Cyprus,ISBN 978-0-7695-3071-0.[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]
A. Kovacs, Gh. Tigan, L. Kovacs, C. Milici.Computer Assisted Mathematics (in romanian: "Matematic Superioare Asistae de Calculator").1st edition,2006.Politechnica Publisher, Timisoara,ISBN (10) 973-625-346-5, ISBN (13) 978-973-625-346-1.[bib]
Temur Kutsia, Mircea Marin.Solving Regular Constraints for Hedges and Contexts. In: Proceedings of 20th International Workshop on Unification, UNIF'06, Jordi Levy (ed.), pp. 89-107.2006.[pdf][bib]
Temur Kutsia.Context Sequence Matching for XML..Electronic Notes on Theoretical Computer Science157(2), pp. 47-65.2006.Elsevier,ISSN: 1571-0661.[pdf][bib]
Mircea Marin, Temur Kutsia.Foundations of the Rule-Based System RhoLog. Journal of Applied Non-Classical Logics16(1-2), pp. 151-168.2006.ISBN 2-7462-1479-2.[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]
W. Windsteiger.An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema.JSC41(3-4), pp. 435-470.2006.Elsevier,ISSN 0747-7171.[url][pdf][bib]
E. M. Clarke, A. S. Gavlovski, K. Sutner, W. Windsteiger.Analytica V: Towards the Mordell-Weil Theorem. In: Proceedings of Calculemus'06, A. Bigatti, S. Ranise (ed.), Proceedings of Calculemus'06, pp. ?-?.2006.[pdf][bib]
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]
F. Piroi, B. Buchberger.Label Management in Theorema. In: Informal proceedings of the 4th International Conference on Mathematical Knowledge Management, M. Kohlhase (ed.), pp. -.July2005.Bremen, Germany.[bib]
L. Kovacs, T. Jebelean, A. Kovacs.Practical Aspects of Algebraic Invariant Generation for Loops with Conditionals. In: Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-147/148, F.Fazekas et al (ed.), pp. --.26-29 May2005.Technical University of Budapest, PAMM-Centre,Balatonalmadi, Hungary,-.[pdf][bib]
A. Kovacs, L. Kovacs.The Lagrange Interpolation Formula in Determining the Fluid's Velocity Potential through Profile Grids. In: Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-147/148, F.Fazekas et al (ed.), pp. --.26-29 May2005.Technical University of Budapest, PAMM-Centre,Balatonalmadi, Hungary,-.[pdf][bib]
L. Kovacs, T. Jebelean.An Algorithm for Automated Generation of Invariants for Loops with Conditionals. In: Proceedings of the Computer-Aided Verification on Information Systems Workshop (CAVIS05), 7th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC05), D. Petcu et al (ed.), pp. 16-19.September 25-282005.Department of Computer Science, West University of Timisoara, Romania,-.to appear in IEEE journal.[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]
L. Kovacs, N. Popov, T. Jebelean.Verification Environment in Theorema.Annals of Mathematics, Computing and Teleinformatics (AMCT)1(2), pp. 27-34.2005.ISSN 1109-9305.[url][pdf][bib]
Gabor Kusper.Solving the Resolution-Free SAT
Problem by Hyper-Unit Propagation in Linear Time.Annals of
Mathematics and Artificial Intelligence 43(1-4), pp. 129-136.2005.Kluwer Academic Publishers,Dordrecht, Netherlands,[bib]
Gabor Kusper.Solving and Simplifying the Propositional Satisfiability Problem by Sub-Model Propagation. RISC, Johannes Kepler University, Linz, Austria. PhD Thesis.2005.[bib]
Temur Kutsia.Context Sequence Matching for XML. In: Proceedings of the 1th International Workshop on Automated Specification and Verification of Web Sites (WWV'05), Maria Alpuente and Santiago Escobar and Moreno Falaschi (ed.), pp. 103-119.March 14-152005.Valencia, Spain,(Final version to appear in Elsevier ENTCS).[pdf][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]
Temur Kutsia, Mircea Marin.Matching with Regular Constraints. In: Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference LPAR'05, G. Sutcliffe and A. Voronkov (ed.), Lecture Notes in Artificial Intelligence3835, pp. 215-229.2005.Springer Verlag,ISSN 0302-9743, ISBN 3-540-30553-X.[url][pdf][bib]
Temur Kutsia, Mircea Marin.Can Context Sequence Matching be Used for Querying XML?. In: Proceedings of the 19th International Workshop on Unification (UNIF'05), L. Vigneron (ed.), pp. 77-92.2005.[pdf][bib]
Florina Piroi, Temur Kutsia.The Theorema Environment for Interactive Proof Development. In: Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference, LPAR'05, G. Sutcliffe, A. Voronkov (ed.), Lecture Notes in Artificial Intelligence3835, pp. 261-275.2005.Springer Verlag,ISSN 0302-9743, ISBN 3-540-30553-X.[url][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, O. Scherzer.Symbolic Computation for Moments and Filter Coefficients of Scaling Functions.Annals of Combinatorics9(2), pp. 223-243.July2005.ISSN 0218-0006.[doi][bib]
G. Regensburger.Parametrizing compactly supported orthonormal wavelets by discrete moments. J. Kepler University Linz. Technical report, 2005.SFB Report.[bib]
Tudor Jebelean, Laura Szakacs.Functional-Based Synthesis of Systolic Online Multipliers. In: SYNASC-05 (International Symposium on Symbolic and Numeric Scientific Computing), D. Zaharie, D. Petcu, V. Negru, T. Jebelean, G. Ciobanu, A. Cicortas, A. Abraham, M. Paprzycki (ed.), Proceedings of SYNASC-05, pp. 267-275.2005.IEEE Computer Society,ISBN 0-7695-2453-2.[pdf][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
T. Kutsia, B. Buchberger.Predicate Logic with Sequence Variables and Sequence Function Symbols. In: Proceedings of the 3rd International Conference on Mathematical Knowledge Management, MKM'04, Andrea Asperti and Grzegorz Bancerek and Andrzej Trybulec (ed.), Lecture Notes in Computer Science3119, pp. 205-219.Sep 19-212004.Springer Verlag,Bialowieza, Poland,ISBN 3-540-23029-7.[pdf][bib]
T. Ida, D. Tepeneu, B. Buchberger, J. Robu.Proving and Constraint Solving in Computational Origami. In: Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation), B. Buchberger and John Campbell (ed.), Springer Lecture Notes in Artificial Intelligence3249, pp. 132-142.22-24 September2004.Copyright: Springer-Berlin,RISC, Johannes Kepler University, Austria,ISSN 0302-9743, ISBN 3-540-232.[bib]
B. Buchberger.Algorithm Supported Mathematical Theory Exploration: A Personal View and Stragegy. In: Proceedings of AISC 2004 (7 th International Conference on Artificial Intelligence and Symbolic Computation), B. Buchberger, John Campbell (ed.), Springer Lecture Notes in Artificial Intelligence3249, pp. 236-250.22-24 September2004.Copyright: Springer, Berlin-Heidelberg,RISC, Johannes Kepler University, Austria,ISSN 0302-9743, ISBN 3-540-232.[pdf][bib]
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, T. Ida.Computational Origami: Interaction of Solving, Proving and Computing. In: Proceedings of World Conference on 21st Century Mathematics, , pp. -.18-20 March2004.Lahore, Pakistan,accepted.[nb][bib]
B. Buchberger.Towards the Automated Synthesis of a Groebner Bases Algorithm.RACSAM - Revista de la Real Academia de Ciencias (Review of the Spanish Royal Academy of Science), Serie A: Mathematicas98(1), pp. 65-75.2004.ISSN 1578 7303.[pdf][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]
F. Piroi, B. Buchberger.An Environment for Building Mathematical Knowledge Libraries. In: Proceedings of the Workshop on Computer-Supported Mathematical Theory Development, Second International Joint Conference (IJCAR), Wolfgang Windsteiger and Christoph Benzmueller (ed.), pp. 19-29.4-8 July2004.Cork, Ireland,ISBN 3-902276-04-5.[pdf][bib]
B. Buchberger.Computer-Supported Mathematical Theory Exploration: Schemes, Failing Proof Analysis, and Metaprogramming. Submitted to the RISC Report Series. Juni2004.[bib]
B. Buchberger, A. Craciun.Algorithm Synthesis by Lazy Thinking: Using Problem Schemes. In: Proceedings of SYNASC 2004, 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, D.Petcu and V.Negru and D.Zaharie and T.Jebelean (ed.), pp. 90-106.26-30 September2004.Copyright: Mirton Publisher,Timisoara, Romania,ISBN 973-661-441-7.[pdf][bib]
B. Buchberger, A. Craciun.Algorithm Synthesis by Lazy Thinking: Examples and Implementation in Theorema. In: Electronic Notes in Theoretical Computer Science, Fairouz Kamareddine (ed.)93, pp. 24-59.18 February2004.ISBN 044451290X.Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, Nov. 25, 2003.[url][pdf][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]
L. Kovacs, T. Jebelean.Generation of Loop Invariants in Theorema by Combinatorial and Algebraic Methods. In: Bulletins for Applied and Computer Mathematics, Pannonian Applied Mathematical Meetings, PC-144, F. Fazekas et al (ed.) vol. CVI/2172, pp. 125-134.20-23 May2004.Technical University of Budapest, PAMM-Centre,Balatonalmadi, Hungary,ISSN 0133-3526.[pdf][bib]
L. Kovacs, T. Jebelean.Automated Generation of Loop Invariants by Recurrence Solving in Theorema. In: Proc. of the 6th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC04), D. Petcu and V. Negru and D. Zaharie and T. Jebelean (ed.), pp. 451-464.26-30 September2004.Mirton Publisher,Timisoara, Romania,ISBN 973-661-441-7.[pdf][bib]
T. Jebelean, L. Kovacs, N. Popov.Experimental Program Verification in the Theorema System. In: Proceedings ISOLA 2004, T. Margaria, B. Steffen (ed.), Proceedings of International Symposium on Leveraging Applications of Formal Methods ISOLA 2004, pp. 92-99.November2004.Paphos, Cyprus,University of Cyprus,[pdf][ps][bib]
L. Kovacs, T. Jebelean.Automated Generation of Loop Invariants by Recurrence Solving in Theorema.Analele Universitatii din Timisoara, Seria Matematica - InformaticaXLII, pp. 151-166.2004.Mirton Publisher,Timisoara, Romania,ISSN 1224-970X.special issue on Computer Science - Proceedings of SYNASC'04.[pdf][bib]
L. Kovacs.Verification of Imperative Programs in Theorema. West University of Timisoara, Romania. Diploma Thesis.2004.[bib]
Temur Kutsia.Solving Equations Involving Sequence Variables and Sequence Functions. In: Proceedings of the 7th International Conference on Artificial Intelligence and Symbolic Computation, AISC'04, Bruno Buchberger and John A. Campbell (ed.), Lecture Notes in Artificial Intelligence3249, pp. 157-170.Sep 22-242004.Springer Verlag,Hagenberg, Austria,ISBN 3-540-23212-5.[pdf][bib]
Mircea Marin, Temur Kutsia.A Rule-based Approach to the Implementation of Evaluation Strategies. In: Proceedings of the 6th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'04), Dana Petcu and Daniela Zaharie and Viorel Negru and Tudor Jebelean (ed.), pp. 227-241.Sep 26-302004.Mirton Publishing Company,Timisoara, Romania,ISBN 973-661-441-4.[bib]
Temur Kutsia, Mircea Marin.Unification Procedure for Terms with Sequence Variables and Sequence Functions (Extended Abstract).. In: Proceedings of the 18th International Workshop on Unification (UNIF'04), Michael Kohlhase (ed.), pp. 1-13.52004.Cork, Ireland,[pdf][bib]
Mircea Marin, Florina Piroi.Rule-Based Programming with Mathematica. In: Proceedings of the 6th International Mathematica Conference, Alberta, Canada, 2004, , pp. -.August2004.Wolfram Institute,Also as RICAM report series 2004-16.[bib]
Mircea Marin, Florina Piroi.Deduction and Presentation in $\rho$Log. In: Proceedings of the Mathematical Knowledge Management Symposium, F. Kamareddine (ed.), ENTCS93, pp. 161-182.February2004.Elsevier,Heriot-Watt University, Edinburgh,ISBN 044451290X.[bib]
Florina Piroi.User Interface Features in Theorema: A Summary. In: In Proceedings of "Mathematical User-Interfaces Workshop" At the Third Mathematical Knowledge Management Conference, Paul Libbrecht (ed.), pp. 1-16.2004.Also available as SFB Technical Report 2004-46.[url][bib]
Florina Piroi.Tools for Using Automated Provers in Mathematical Theory Exploration. Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria. PhD Thesis.August2004.Also available as RISC Tech Report no. 04-12.[url][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]
N. Popov, T. Jebelean.A Practical Approach to Proving Termination of Recursive Programs in Theorema. In: Proceedings of 7th International Workshop on Termination, M. Codish, A. Middeldorp (ed.), pp. 43-46.June2004.Aachen, Germany,ISSN-0935-3232.[pdf][bib]
M. Rosenkranz.New Symbolic Method for Solving Linear Two-Point Boundary Value Problems on the Level of Operators.Journal of Symbolic Computation39(2), pp. 171-199.2004.Elsevier,ISBN 0747-7171.[bib]
M. Rosenkranz.The Algorithmization of Physics: Math Between Science and Engineering. In: Proceedings of AISC 2004, B. Buchberger, J.A. Campbell (ed.), Proceedings of Artificial Intelligence and Symbolic Computation: 7th International Conference, Linz, Austria, Lecture Notes in Artificial Intelligence (LNAI)3249, pp. 1-7.September2004.Springer,Castle of Hagenberg, Austria,ISBN 3-540-23212-5.Invited talk.[bib]
2003
T.Ida, B. Buchberger.Proving and Solving in Computational Origami.Analele Universitatii din Timisoara, Seria Matematica - InformaticaXLI, pp. 247-263.2003.Copyright: Mirton Publisher,Timisoara, Romania,ISSN 1224-970X.special issue on Computer Science - Proceedings of SYNASC'03.[ps][nb][pdf][bib]
B. Buchberger.Algorithm Invention and Verification by Lazy Thinking.Analele Universitatii din Timisoara, Seria Matematica - InformaticaXLI, pp. 41-70.2003.Copyright: Mirton Publisher, Timisoara, Romania,ISSN 1224-970X.special issue on Computer Science - Proceedings of SYNASC'03.[pdf][bib]
B. Buchberger.Algorithm Invention and Verification by Lazy Thinking. In: Proceedings of SYNASC 2003, 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, D. Petcu, V. Negru, D. Zaharie, T. Jebelean (ed.), pp. 2-26.1-4 October2003.Copyright: Mirton Publisher,Timisoara, Romania,ISBN: 973-661-104-3.[nb][bib]
M. Rosenkranz, B. Buchberger, H. W. Engl.Solving Linear Boundary Value Problems Via Non–commutative Groebner Bases.Applicable Analysis82(7), pp. 655-675.July2003.Copyright: Taylor & Francis Ltd.,ISSN 0003-6811, ISSN 1563-504X.[bib]
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]
B. Buchberger.Computational Mathematics, Computational Logic and Symbolic Computation. In: Computer Science Logic - Proceedings of 17th International Workshop CSL 2003, 12th Annual Conference of the EACSL, 8th Kurt Gödel Colloqium, KGC 2003, M.Baaz, J. A. Makowsky (ed.), Lecture Notes in Computer ScienceVol. 2803, pp. 98-99.August 25-302003.Springer - Verlag Berlin,Vienna, Austria,ISSN 0302-9743.[nb][bib]
B. Buchberger, G. Gonnet, M. Hazewinkel.Preface on Mathematical Knowledge Management. In: Special Issue of Annals of Mathematics and Artificial Intelligence, B. Buchberger, G. Gonnet, M. Hazewinkel (ed.)38/1-3, pp. 1-2.May2003.Kluwer Academic Publishers, Dordrecht, Netherlands,ISSN 1012-2443.[doc][bib]
B. Buchberger.F 1322: Computer Algebra for Pure and Applied Functional Analysis. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, P. Paule, U. Langer (ed.), pp. 335-364.October2003.Johannes Kepler University Linz, Austria,-.[bib]
T. Jebelean, B. Buchberger.Theorema: Computation and Deduction in Natural Style. In: Computer Algebra Handbook, J. Grabmeier, E. Kaltofen, V. Weispfennig (ed.), pp. 453-454.2003.Springer - Verlag Berlin,ISBN 3-540-65466-6.[bib]
B. Buchberger, G. Gonnet, M. Hazewinkel.Preface on Mathematical Knowledge Management. In: Special Issue of Annals of Mathematics and Artificial Intelligence, 38/1-3, pp. 1-2.May2003.Kluwer Academic Publishers, Dordrecht, Netherlands,ISSN 1012-2443.[doc][bib]
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz, L. Kovacs, C. Kocsis.F 1302: THEOREMA: Proving, Solving, and Computing in the Theory of Hilbert Spaces. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, P. Paule, U. Langer (ed.), pp. 58-73.October2003.Johannes Kepler University Linz, Austria,-.[bib]
L. Kovacs, T. Jebelean.Practical Aspects of Imperative Program Verification in Theorema. In: Proceedings of SYNASC 2003, 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, D. Petcu, V. Negru, D. Zaharie, T. Jebelean (ed.), pp. 317-320.1-4 October2003.Mirton Publisher,Timisoara, Romania,ISBN: 973-661-104-3.[pdf][bib]
L. Kovacs, T. Jebelean, N. Popov.Verification of Imperative Programs in Theorema. In: Proceedings of the 1st South-East European Workshop on Formal Methods (SEEFM'03), D. Dranidis and K. Tigka (ed.), pp. 140-147.November2003.Thessaloniki, Greece,ISSN: 960-87869-1-6.[pdf][bib]
L. Kovacs, T. Jebelean.Generation of Invariants in Theorema. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, N.Boja (ed.), Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics, pp. 407-415.6-9 November2003.Timisoara, Romania,ISSN 1224-6069.[pdf][talk.nb][bib]
L. Kovacs, T. Jebelean.Generation of Invariants in Theorema. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, N.Boja (ed.), pp. 407-415.6-9 November2003.ISSN 1224-6069.Scientific Bulletins of the Politehnica University Timisoara, Transactions on Mathematics and Physics.[bib]
A. Kovacs, L. Kovacs Nicolae Boja.Rechnungsalgorytmus der Potentialintegralgleichung der Kompressiblen Fluidgeschwindigkeit durch Profilgitter. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, Nicolae Boja (ed.), Scientific Bulletins of the Politehnica University of Timisoara, Transactions on Mathematics and Physics, pp. 427-434.6-9 November2003.Timisoara, Romania,ISSN 1224-6069.english title: The Calculus Algorithm for the Integral Equation of the Compressible Fluids Speeds Potentials through Specialized Networks.[bib]
A. Kovacs, L. Kovacs Nicolae Boja.Rechnungsalgorytmus der Potentialintegralgleichung der Kompressiblen Fluidgeschwindigkeit durch Profilgitter. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, Nicolae Boja (ed.), Scientific Bulletins of the Politehnica University of Timisoara, Transactions on Mathematics and Physics, pp. 427-434.6-9 November2003.Timisoara, Romania,ISSN 1224-6069.english title: The Calculus Algorithm for the Integral Equation of the Compressible Fluids Speeds Potentials through Specialized Networks.[bib]
A. Kovacs, L. Kovacs.Rechnungsalgorytmus der Potentialintegralgleichung der Kompressiblen Fluidgeschwindigkeit durch Profilgitter. In: Proceedings of the 10th International Symphosium of Mathematics and its Application, N. Boja (ed.), Scientific Bulletins of the Politehnica University of Timisoara, Transactions on Mathematics and Physics, pp. 427-434.6-9 November2003.Timisoara, Romania,ISSN 1224-6069.english title: The Calculus Algorithm for the Integral Equation of the Compressible Fluids Speeds Potentials through Specialized Networks.[bib]
Temur Kutsia.Unification Modulo Flatness. In: Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Dana Petcu and Daniela Zaharie and Viorel Negru and Tudor Jebelean (ed.), pp. 135-148.1-42003.Mirton Publishing Company,Timisoara, Romania,ISBN 973-661-104-3.[bib]
Temur Kutsia.Equational Prover of Theorema. In: Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03), Robert Nieuwenhuis (ed.), Lecture Notes in Computer Science2706, pp. 367-379.June 9-112003.Springer Verlag,Valencia, Spain,ISBN 3-540-40254-3.[pdf][bib]
Temur Kutsia.Matching in Flat Theories. In: Proceedings of the 17th International Workshop on Unification (UNIF'03), Jordi Levy and Michael Kohlhase and Joachim Niehren and Mateu Villaret (ed.), pp. 57-64.June 8-92003.Valencia, Spain,ISBN 84-96221-00-8.[pdf][bib]
Mircea Marin, Temur Kutsia.Programming with Transformation Rules.Analele Universitatii de Vest din TimisoaraXVI, pp. 163-177.2003.Mirton Publishing Company,ISSN 1224-970X.[bib]
Mircea Marin, Temur Kutsia.Programming with Transformation Rules. In: Proceedings of the 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'03), Dana Petcu and Daniela Zaharie and Viorel Negru and Tudor Jebelean (ed.), pp. 157-167.Oct 1-42003.Mirton Publishing Company,Timisoara, Romania,ISBN 973-661-104-3.[bib]
Mircea Marin, Temur Kutsia.On the Implementation of a Rule-Based Programming System and some of its Applications. In: Proceedings of the 4th International Workshop on the Implementation of Logics (WIL'03), Boris Konev and Renate Schmidt (ed.), pp. 55-68.2003.Almaty, Kazakhstan,[pdf][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]
Nikolaj Popov, Tudor Jebelean.A Practical Approach to Verification of Recursive Programs in Theorema. In: Proceedings of SYNASC'03 (International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara, Romania, 2003), T. Jebelean, V. Negru, A. Popovici (ed.), pp. 329-332.October2003.Mirton,ISBN 973-661-104-3.[ps][pdf][bib]
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz, L. Kovacs, C. Kocsis.F 1302: THEOREMA: Proving, Solving and Computing in General Domains. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 2001-September 2003, P. Paule, U. Langer (ed.), pp. 148-170.October2003.Johannes Kepler University Linz, Austria,[bib]
Markus Rosenkranz.A Symbolic Algorithm for Generating Solutions of Boundary Value Problems. RISC, Johannes Kepler University Linz. PhD Thesis.2003.[bib]
W. Windsteiger.Mathematica. In: Computer Algebra Handbook: Foundations, Applications, Systems, J. Grabmeier, E. Kaltofen, and V. Weispfenning (ed.), pp. 314-320.2003.Springer,ISBN 3-540-65466-6.[bib]
W. Windsteiger.Exploring an Algorithm for Polynomial Interpolation in the Theorema System. In: Proceedings of the Calculemus 2003 Symposium, T. Hardin and R. Rioboo (ed.), pp. 130-136.September2003.Aracne Editrice S.R.L.,Rome Italy,ISBN 88-7999-545-6.[pdf][bib]
2002
B. Buchberger.Groebner Bases: The Commutative Case. In: The Concise Handbook of Algebra, A. V. Mikhalev, G. F. Pilz (ed.), pp. 262-265.2002.Copyright: Kluwer Academic Publishers,Dordrecht, Netherlands,ISBN 0-7923-7072-4.[bib]
B. Buchberger.Groebner Bases: Applications. In: The Concise Handbook of Algebra, A. V. Mikhalev and G. F. Pilz (ed.), pp. 265-268.2002.Kluwer Academic Publishers, Dordrecht, Netherlands.,ISBN 0-7923-7072-4.[bib]
A. Craciun, B. Buchberger.Proving the Correctness of the Merge-Sort Algorithm with Theorema. In: Proceedings of SYNASC 2002, 4th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, D. Petcu, V. Negru, D. Zaharie, T. Jebelean (ed.), pp. 97-111.9-12 October2002.Mirton Publisher,Timisoara, Romania,ISBN 973-585-785-5.[bib]
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]
B. Buchberger.Symbolic Computation. In: Handbuch der Informatik, G. Pomberger, P. Rechenberg (ed.), 1st edition, pp. 955-974.2002.Carl Hanser Verlag Munich,ISBN 3446401857.(3rd edition, pp. 963 - 981).[bib]
M. Rosenkranz, B. Buchberger, H. W. Engl.Solving Linear Boundary Value Problems Via Non–commutative Groebner Bases. In: Proceedings of SYNASC 2002, 4th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, D. Petcu, V. Negru, D. Zaharie, T. Jebelean (ed.), pp. 300-313.9-12 October2002. Mirton Publisher, Timisoara, Romania,ISBN 973-585-785-5.[bib]
B. Buchberger.Invention by Lazy Thinking. In: "A Min Tjoa @ Work"- In honor of the 50th birthday of Univ.Prof.Dr. A Min Tjoa, R. Wagner (ed.), pp. 11-31.December2002.Austrian Computer Society,ISBN 3-85403-164-5.[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]
F. Piroi, B. Buchberger.Focus Windows: A New Technique for Proof Presentation. In: Proceedings of the 8th Rhine Workshop on Computer Algebra, Mannheim, Germany, H. Kredel, W. Seiler (ed.), pp. 297-313.March 21-222002._.[pdf][abstract][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]
B. Buchberger, T. Jebelean, W. Windsteiger, T. Kutsia, K. Nakagawa, J. Robu, F. Piroi, A. Craciun, N. Popov, G. Kusper, M. Rosenkranz.F 1302: Solving and Proving in General Domains. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Annual Report 2002, U. Langer, F. Winkler (ed.), pp. 4-5.February2002.Johannes Kepler University Linz, Austria,[bib]
Tudor Jebelean.Nonconventional Algorithms for Multiprecision Arithmetic. In: Proceeding of SYNASC'02, Negru at al (ed.), pp. 3-7.October2002.Mirton,Timisoara, Romania,ISBN: 973-585-785-5.[bib]
Gabor Kusper.Integrating Temporal Assertions into a Parallel Debugger. In: Proceedings of the 8th International Euro-Par Conference, B. Monien and R. Feldmann (ed.), pp. 113-120.2002.Springer-Verlag,Paderborn, Germany,ISBN:3-540-44049-6.[bib]
Temur Kutsia.Theorem Proving with Sequence Variables and Flexible Arity Symbols. In: Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 9th International Conference, LPAR'02, Matthias Baaz and Andrei Voronkov (ed.), Lecture Notes in Artificial Intelligence2514, pp. 278-291.Oct14-182002.Springer Verlag,Tbilisi, Georgia,ISBN 3-540-00010-0.[pdf][bib]
Temur Kutsia.Pattern Unification with Sequence Variables and Flexible Arity Symbols.Electronic Notes on Theoretical Computer Science66(5), pp. 1-18.2002.ISSN 1571-0661.[pdf][bib]
Temur Kutsia.Unification with Sequence Variables and Flexible Arity Symbols and its Extension with Pattern-Terms. In: Artificial Intelligence, Automated Reasoning and Symbolic Computation. Proceedings of Joint AISC'2002 - Calculemus'2002 conference, Jacques Calmet and Belaid Benhamou and Olga Caprotti and Laurent Henocque and Volker Sorge (ed.), Lecture Notes in Artificial Intelligence2385, pp. 290-304.July 1-52002.Springer Verlag,Marseille, France,ISBN 3-540-43865-3.[pdf][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]
Temur Kutsia.Solving and Proving in Equational Theories with Sequence Variables and Flexible Arity Symbols. RISC, Johannes Kepler University of Linz. PhD Thesis.2002.[ps][bib]
Koji Nakagawa.Variable Shape Logicographic Symbols. In: Logic, Mathematics and Computer Science: Interactions (LMCS 2002), K. Nakagawa (ed.), Proceedings of Symposium in Honor of Bruno Buchberger's 60th Birthday, Appears in RISC-report Series Nr. 02-60, pp. 202-216.October2002.RISC, Schloss Hagenberg, Austria,ISBN 3-902276-03-7.[bib]
Koji Nakagawa.Supporting User-Friendliness in the Mathematical Software System Theorema. RISC, Johannes Kepler University Linz. PhD Thesis.2002.[bib]
Judit Robu.Automated Geometric Theorem Proving in the Frame of the Theorema Project. RISC, Johannes Kepler University Linz. PhD Thesis.2002.[bib]
W. Windsteiger.An Automated Prover for Set Theory in Theorema. In: Calculemus 2002, 10th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning: Work in Progress Papers, O. Caprotti, V. Sorge (ed.), pp. 56-67.June2002.Marseille, France,ISSN 14274447.Appears in Seki-Report Series Nr. SR-02-04, Universitaet des Saarlandes.[ps][bib]
W. Windsteiger.An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema. In: Logic, Mathematics and Computer Science: Interactions (LMCS 2002), K. Nakagawa (ed.), pp. 266-280.October2002.RISC, Schloss Hagenberg, Austria,ISBN 3-902276-03-7.Symposium in Honor of Bruno Buchberger's 60th Birthday, Appears in RISC-report Series Nr. 02-60.[pdf][bib]
2001
B. Buchberger.Computers and Mathematical Research. In: Mathematical Glimpses into the 21st Century, Round Table at the Third European Congress of Mathematics, Barcelona, C.Casacuberta, R. M. Miro-Roig, J. M. Ortega and S. Xambo-Descamps (ed.), pp. 140-147.2001.Copyright: Centro Internacional de Metodos Numericos en Ingenieria, Gran Capitan,Barcelona, Espana,Artes Graficas Torres S.A,ISBN: 84-89925-85-2.[bib]
B. Buchberger.Groebner Rings and Modules. In: Proceedings of SYNASC 2001 (The 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing), S. Maruster, B. Buchberger, V. Negru, T. Jebelean (ed.), pp. 22-25.2-5 October2001.University of the West Timisoara, Romania,RISC-Linz Report Series No. 01-20.[abstract][pdf][ps][bib]
B. Buchberger.Groebner Bases and Systems Theory.Multidimensional Systems and Signal Processing, Special Issue on "Applications of Groebner Bases in Multidimensional Systems and Signal Processing"12(3/4), pp. 223-253.October2001. Kluwer Academic Publishers, Boston,ISSN 0923-6082.Z. Lin, L. Xu (eds.).[bib]
B. Buchberger.Logicographic Symbols: A New Feature in Theorema. In: Symbolic Computation - New Horizons (Proceedings of the 4th International Mathematica Symposium), Y. Tazawa (ed.), pp. 23-30.25-27 June2001.Copyright: Tokyo Denki University Press,Tokyo Denki University, Chiba New Town Campus, Japan,ISBN 4-501-73020-X C3041.[pdf][abstract][ps][bib]
K. Nakagawa, B. Buchberger.Presenting Proofs Using Logicographic Symbols. In: Proceedings of the Workshop on Proof Transformation and Presentation at the IJAR-2001, A. Fiedler, H. Horacek (ed.), pp. -.18 June2001.Siena,[abstract][ps][pdf][bib]
B. Buchberger.Theorema: A Proving System Based on Mathematica.The Mathematica Journal8(2), pp. 247-252.2001.Copyright: Wolfram Research,ISSN: 1047-5974.[bib]
B. Buchberger.The PCS Prover in Theorema. In: Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), R. Moreno-Diaz, B. Buchberger, J.L. Freire (ed.), Lecture Notes in Computer Science 2178, pp. 469-478.19-23 February2001.Copyright: Springer - Verlag Berlin,Las Palmas de Gran Canaria,ISSN 0302-9743, ISBN 3-540-429.[ps][pdf][abstract][bib]
B. Buchberger.Groebner Bases: A Short Introduction for Systems Theorists. In: Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), R. Moreno-Diaz, B. Buchberger, J.L. Freire (ed.), Lecture Notes in Computer Science 2178, pp. 1-19.19-23 February2001.Copyright: Springer - Verlag Berlin,Las Palmas de Gran Canaria,ISSN 0302-9743, ISBN 3-540-429.[abstract][pdf][bib]
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]
B. Buchberger.Mathematical Knowledge Management using THEOREMA. In: First International Workshop on Mathematical Knowledge Management (MKM 2001), B.Buchberger, O. Caprotti (ed.), pp. --.2001.RISC-Linz, A-4232 Schloss Hagenberg, September 24-26, 2001, 17 pages.,-.[ps][bib]
B. Buchberger, K. Nakagawa.The Role of Logicographic Symbols for Mathematical Knowledge Management. In: Proceedings of the First International Workshop on Mathematical Knowledge Management (MKM), B. Buchberger, O. Caprotti (ed.), pp. -.September 24-262001.RISC-Linz, A-4232 Schloss Hagenberg,[bib]
B. Buchberger.Mathematical Knowledge Management in THEOREMA. In: First International Workshop on Mathematical Knowledge Management (MKM 2001), B. Buchberger, O. Caprotti (ed.), pp. -.September 24-262001.RISC-Linz, A-4232 Schloss Hagenberg,[bib]
Tudor Jebelean.Non-conventional Algorithms for Multiple Precision Arithmetic. RISC, University of Linz. PhD Thesis.December2001.Habilitation thesis.[bib]
Boris Konev, Tudor Jebelean.Solution Lifting Method for Handling Meta-variables in Theorema. In: Proceedings of SYNASC01, S. Maruster, B. Buchberger, V. Negru, T. Jebelean (ed.), Proceedings of 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, pp. 15-23.October2001.Mirton,Timisoara, Romania,ISSN: 973-661-441-7.[bib]
Temur Kutsia.Unification in the Empty and Flat Theories with Sequence Variables and Flexible Arity Symbols. In: Proceedings of the 17th International Workshop on Unification (UNIF'03), Franz Baader and Volker Diekert and Cesare Tinelli and Ralf Treinen (ed.), pp. 20-23.June 18-192001.Siena, Italy,[bib]
Temur Kutsia, Koji Nakagawa.An Interface between Theorema and External Automated Deduction Systems. In: Proceedings of 9th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus'01), Steve Linton and Roberto Sebastiani (ed.), pp. 178-182.Jun 21-232001.Siena, Italy,[bib]
Florina Piroi, Tudor Jebelean.Advanced Proof Presentation in Theorema.Special Issue of the Annals of the University of the West, Timisoara.XXXIX, pp. 181-199.September2001.ISSN 1224-970X.Proceedings of SYNASC 01, 3rd International Workshop on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, October 2-5, 2001.[bib]
W. Windsteiger.A Set Theory Prover in Theorema. In: Computer Aided Systems Theory, R. Moreno-Diaz and B. Buchberger and J.L. Freire (ed.), LNCS2178, pp. 525-539.2001.Springer,ISSN 0302-9743, ISBN 3-540-429.Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory - Formal Methods and Tools for Computer Science), extended version available as RISC report 01-07.[bib]
W. Windsteiger.On a Solution of the Mutilated Checkerboard Problem using the Theorema Set Theory Prover. In: Proceedings of the Calculemus 2001 Symposium, S. Linton and R. Sebastiani (ed.), pp. 28-47.2001.[pdf][bib]
Wolfgang Windsteiger.A Set Theory Prover in Theorema: Implementation and Practical Applications. RISC Institute. PhD Thesis.May2001.[tar.gz][bib]
Wolfgang Windsteiger.Theorema: Ein Rahmen fuer Mathematik, Algorithmik und Didaktik. Technical report no. 01-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2001.Course for mathematics teachers given in the frame of the ``Tag der Mathematik 2001'' at the University of Linz, November 23, 2001. In German.[ps][tar.gz][bib]
Wolfgang Windsteiger.A Set Theory Prover within Theorema. Technical report no. 01-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2001.Also available as SFB report 01-23.[ps][bib]
2000
B. Buchberger.Computer-assisted Proving by the PCS Method. In: Proceedings of the Workshop on Constructive Algebra, - (ed.), pp. -.1-3 November2000.Amsterdam,-.Springer Lecture Notes in Computer Science, submitted.[pdf][abstract][pdf][bib]
B. Buchberger.Mathematics and Computer Science: A Personal View.Analele Universitatii din Timisoara, Seria Matematica - Informatica38(1), pp. 3-15.2000.ISSN 1224-970X.[bib]
B. Buchberger.Theory Exploration with Theorema.Analele Universitatii Din Timisoara, Seria Matematica-InformaticaXXXVIII(2), pp. 9-32.2000.ISSN 1124-970X.Selected papers of the 2nd International Workshop on Symbolic and Numeric Algorithms in Scientific Computing, Oct. 4-6, 2000, Timisoara, Romania (T. Jebelean, V. Negru, A. Popovici eds.).[abstract][ps][pdf][bib]
B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, W. Windsteiger.The Theorema Project: A Progress Report. In: Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning), M. Kerber, M. Kohlhase (ed.), pp. 98-113.6-7 August2000.Copyright: A.K. Peters, Natick, Massachusetts,St. Andrews, Scotland,ISBN 1-56881-145-4.[ps][pdf][abstract][bib]
B. Buchberger.Theorem Proving For and With Gröbner Bases Theory. In: 2nd International Workshop on Multidimensional (nD) Systems, June 27-30, 2000, Csocha Castle, Lower Silesia, Poland., K. Galkowski (ed.), pp. 15-22.2000.Copyright: Technical University Press, Zielona Gora, Poland,ISBN: 83-85911-71-5.[bib]
B. Buchberger.Computer-Algebra: Das Ende der Mathematik? (Computer Algebra: The End of Mathematics?). In: Mitteilungen der Deutschen Mathematiker-Vereinigung, 2, pp. 16-19.2000.Copyright: Birkhaeuser Verlag AG, Basel, Switzerland,ISSN 0947-4471, ISSN 1399-590.(English Translation in: ACM SIGSAM Bulletin, March 2002. Danish Translation in: Matilde, Nr. 8, February 2000, pp. 4-7, Univ. of Kobenhavn).[pdf][ps][abstract][bib]
B. Buchberger.Mathematik am Computer: Die naechste Ueberforderung? (Mathematics on the Computer: The Next Overtaxation?). In: Didaktik-Reihe der Oesterreichischen Mathematischen Gesellschaft (Proceedings of a Symposium for High-school Teachers, September 24, 1999, Graz, Austria), Vol.131, pp. 37-56.March2000.[bib]
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, J. Schicho.F 1303: Proving and Solving Over the Reals. In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, B. Buchberger and U.Langer (ed.), pp. 126-142.October2000.Johannes Kepler University Linz, Austria,[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.Symbolisches Rechnen: Eliminieren sich die Mathematiker selbst? (Symbolic Computation: Are the Mathematicians Eliminating Their Own Jobs). In: Exhibition Catalogue "Mathematische Machinen: Von der Rechenmaschine zum Computer", F. Pichler (ed.), pp. 1-13.2000.Strom-Museum, Ybbs, Austria,[bib]
B. Buchberger et al.F1302: Proving, Solving, and Computing in the Theory of Hilbert Spaces (Research Proposal). In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part II: Proposal, , pp. 54-85.October 62000.Johannes Kepler University Linz, Austria,[bib]
B. Buchberger, J. Schicho.F 1303: Proving and Solving Over the Reals (Progress Report). In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, B. Buchberger and U.Langer (ed.), pp. 126-142.October2000.Johannes Kepler University Linz, Austria,[bib]
B. Buchberger et al.F 1302: THEOREMA: Proving, Solving, and Computing in General Domains (Progress Report). In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, B. Buchberger, U. Langer (ed.), pp. 101-125.October2000.Johannes Kepler University Linz, Austria,-.[bib]
B. Buchberger et al.F 1301: Coordination and Service Project (Progress Report). In: Special Research Program (SFB) F 013, Numerical and Symbolic Scientific Computing, Proposal for Continuation, Part I: Progress Report, April 1998-September 2000, B. Buchberger, U. Langer (ed.), pp. 88-100.October2000.Johannes Kepler University Linz, Austria,-.[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]
Mircea Marin.Functional Logic Programming with Distributed Constraint Solving. RISC, Johannes Kepler University Linz. PhD Thesis.2000.[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]
Daniela Vasaru Dupre.Automated Theorem Proving by Integrating Proving, Solving and Computing. RISC, Johannes Kepler University of Linz. PhD Thesis.2000.[zip][bib]
1999
B. Buchberger, T. Jebelean.Teaching of Mathematics Using Theorema. The International Journal of Computer Algebra in Mathematical Education6(1), pp. 25-50.1999.Copyright: Research Information Ltd., UK.,ISSN 1362-7368.[bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Progress Report. Technical report no. 99-42 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-35, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[ps][bib]
Bruno Buchberger, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Koji Nakagawa, Daniela Vasaru, Wolfgang Windsteiger.Theorema: A Short Demo. Technical report no. 99-45 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1999.Also available as SFB Report 99-37, Johannes Kepler University Linz, Spezialforschungsbereich F013, December, 1999.[tar.gz][bib]
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, T. Jebelean.Distance Teaching of Mathematics Using Theorema. In: Proceedings of the 3rd Technion Symposium on Software for Communication, H. Gutmann (ed.), pp. -.April 1-31999.Hagenberg, Austria,[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]
B. Buchberger.Theory Exploration Versus Theorem Proving. In: Proceedings of the Calculemus '99 Workshop, A. Armando, T. Jebelean (ed.), Electronic Notes in Theoretical Computer Science23/3, pp. 386-386.1999.Elsevier,-.[bib]
Windsteiger W..Building Up Hierarchical Mathematical Domains Using Functors in THEOREMA. In: Electronic Notes in Theoretical Computer Science, A. Armando and T. Jebelean (ed.), Proceedings of Calculemus'99, Trento, Italy, ENTCS23/3, pp. 401-419.1999.Elsevier,ISSN: 1571-0661.[url][pdf][bib]
Wolfgang Windsteiger.Theorema: Overview on Using the System and Details on Composing Hierarchical Knowledge Bases. Technical report no. 99-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June1999.Presented at the Edinburgh School in Logic and Computation.[tar.gz][bib]
1998
B. Buchberger, T. Jebelean, D.Vasaru.Theorema: A System for Formal Scientific Training in Natural Language Presentation. In: Proceedings of Ed-Media 1998 (International Conference on Educational Multimedia), - (ed.), pp. 174-179.June 20-231998.Freiburg, Germany,[bib]
B. Buchberger.Introduction to Groebner Bases. In: Groebner Bases and Applications, B. Buchberger, F. Winkler (ed.), London Mathematical Society Lecture Notes Series 251, pp. 3-31.1998.Cambridge University Press,ISBN 0-521-63298-6.[pdf][bib]
Bruno Buchberger, Klaus Aigner, Claudio Dupre, Tudor Jebelean, Franz Kriftner, Mircea Marin, Koji Nakagawa, Ovidiu Podisor, Elena Tomuta, Yaroslav Usenko, Daniela Vasaru, Wolfgang Windsteiger.Theorema: An Integrated System for Computation and Deduction in Natural Style. Technical report no. 98-25 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December1998.Also available as SFB Report No. 98-06.[ps][bib]
B. Buchberger, W. Windsteiger.The Theorema Language: 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.Theorema: Using the Predicate Logic Prover for Proof Training. In: Proceedings of the Second International Theorema Workshop, B. Buchberger, T. Jebelean (ed.), pp. -.June 29-301998.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 98-10.[bib]
B. Buchberger, W.Windsteiger.The Theorema Language: Implemening Object- and Meta-Level Usage of Symbols. In: Proceedings of the Second International Theorema Workshop, B. Buchberger, T. Jebelean (ed.), pp. -.June 29-301998.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 98-10.[bib]
B. Buchberger.Theorema: The Current Status. In: Proceedings of the Second International Theorema Workshop, B. Buchberger, T. Jebelean (ed.), pp. -.June 29-301998.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 98-10.[bib]
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]
B. Buchberger.An Algorithmic Criterion for the Solvability of a System of Algebraic Equations. In: Gröbner Bases and Applications, B. Buchberger, F. Winkler (ed.), London Mathematical Society Lecture Notes Series 251, pp. 535-545.1998.Cambridge University Press,ISBN 0-521-63298-6.[pdf][bib]
B. Buchberger, F. Winkler (ed.).Gröbner Bases and Applications - Proceedings of 33 Years of Gröbner Bases.London Mathematical Society Lecture Note Series 251,1 edition,March1998.Cambridge University Press,ISBN-10: 0521632986; ISBN-13: 978-0521632980.[bib]
Nikolaj Popov.Periodic Interactions. Department of Mathematical Logic and Applications, Faculty of Mathematics and Computer Science, Sofia University, Bulgaria. Diploma Thesis.November1998.[bib]
Elena Tomuta.An Architecture for Combining Provers and its Applications in the Theorema System.. RISC, Johannes Kepler University of Linz. PhD Thesis.1998.[ps][bib]
1997
B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta, D. Vasaru.A Survey of the Theorema project. In: Proceedings of ISSAC'97 (International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, July 21-23, 1997), W. Kuechlin (ed.), pp. 384-391.1997.ACM Press, ISBN 0-89791-875-4.[bib]
B. Buchberger.Introduction to Groebner Bases. In: Logic of Computation, H.Schwichtenberg (ed.), Proceedings of NATO Advanced Study Institute on Logic of Computation, Marktoberdorf, Germany, July 25-August 6, 1995, NATO ASI Series, Series F: Computer and Systems SciencesVol. 157, pp. 35-66.1997.Springer - Verlag Berlin,ISBN 3-540-62963-7.[bib]
B. Buchberger.Groebner Bases.Encyclopaedia of Mathematics SupplementVolume I, pp. 275-275.1997.Kluwer Acad. Publ.,ISBN 0-7923-4709-9.(Editor-in-Chief: M. Hazewinkel).[bib]
B. Buchberger.Mathematica: Doing Mathematics by Computer?. In: Advances in the Design of Symbolic Computation Systems, A. Miola, M. Temperini (ed.), pp. 2-20.1997.Springer Vienna,ISSN 0943-853X, ISBN 3-211-82-844-3.RISC Book Series on Symbolic Computation.[bib]
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]
B. Buchberger, M. Marin.Proving by Simplification. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger.A Note on Computing Times in Different Programming Styles in Mathematica. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger, D. Vasaru.Theorema: The Induction Prover over Lists. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger, T. Jebelean.Theorema: The Predicate Logic Prover. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger.The Theorema Prover for Equalities over the Natural Numbers. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger.Theorema: Natural Language and Nested Cells Representation of Proofs. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger, F. Kriftner.Theorema: The Language. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
B. Buchberger.Theorema: An Overview on the Project and the Proceedings. In: First International Theorema Workshop, B. Buchberger, T. Ida, D. Vasaru (ed.), pp. -.June 9-101997.RISC, Hagenberg, Austria,-.RISC-Linz Report Series No. 97-20.[bib]
M. Rosenkranz.Lagrange Inversion. RISC, J. Kepler University Linz. Diploma Thesis.1997.[ps][ps][pdf][bib]
1996
B. Buchberger.Using Mathematica for Doing Simple Mathematical Proofs. In: Proceedings of the 4th Mathematica Users' Conference, Tokyo, November 2, 1996., - (ed.), pp. 80-96.1996.Copyright: Wolfram Media Publishing,-.[bib]
B. Buchberger.Mathematica as a Rewrite Language. In: Functional and Logic Programming (Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming, November 1-4, 1996, Shonan Village Center), T. Ida, A. Ohori, M. Takeichi (ed.), pp. 1-13.1996.Copyright: World Scientific, Singapore - New Jersey - London - Hong Kong,ISBN 981-02-2923-2.[ps][pdf][abstract][bib]
B. Buchberger.Symbolic Computation: Computer Algebra and Logic. In: Frontiers of Combining Systems, Proceedings of FROCOS 1996 (1st International Workshop on Frontiers of Combining Systems), March 26-28, 1996, Munich, F. Bader, K.U. Schulz (ed.), Applied Logic SeriesVol.3, pp. 193-220.1996.Kluwer Academic Publisher, Dordrecht - Boston - London, The Netherlands,-.[ps][pdf][abstract][bib]
B. Buchberger.Mathematische Software-Systeme: Die Zukunft (Mathematical Software Systems: The Future).Informatik-Spektrum19(2), pp. 100-101.1996.Springer, Heidelberg,ISSN 0170-6012.[bib]
W. Jacak, B. Buchberger, S. Stifter.Intelligent Systems Combining Reactive and Learning Capabilities. In: Proceedings of the 13th European Meeting on Cybernetics and Systems Research, Vienna, Austria, R. Trappl (ed.), pp. 77-82.1996.Austrian Society for Cybernetic Studies, Vienna,ISBN 3 85206 133 4.[bib]
W. Jacak, B. Buchberger, S. Dreiseitl, T. Kubik.Intelligent Robotic Arm Based on Reactive Control. In: Proceeding of the 5th International Workshop on Robotics in Alpe-Adria-Danube Region (RAAD'96), Budapest, Hungary, June 10-13, I. J. Rudas (ed.), pp. 297-302.1996.Hungarian Robotics Association, Budapest,ISBN 963 420 482 1.[bib]
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]
B. Buchberger.Mathematiksoftware und Mathematikunterricht: Ein Vorwort (Mathematical Software and Mathematics Teaching: A Preface). In: Matheamatikunterricht mit Computeralgebra-Systemen, H.Heugl, W. Klinger, J. Lechner (ed.), pp. 9-13.1996.Addison-Wesley, Bonn - Reading,ISBN 3-8273-1082-2.[bib]
1995
I. Duleba, W. Jacak, R. Muszynski, B. Buchberger.Symbolic Computation-Based Synthesis of Neural Network Dynamics and Controllers for Robots. In: Proceedings of the 1995 IEEE International Conference on Neural Networks (ICNN'95), Perth, Australia, - (ed.), pp. 2720-2725.1995.-.[bib]
B. Buchberger.Symbolic Computation Software Systems: The Current State of Technology. In: Proceedings of the EUROSIM 95 Conference, F. Breitenecker, I. Husinsky (ed.), pp. 85-94.September 5-71995.Elsevier,Technical University, Vienna,ISBN 0-444-82241-0.[bib]
Ana Maria Mandache.Gröbner Bases Computation and Gaussian Elimination. RISC, Johannes Kepler University Linz. PhD Thesis.1995.[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]
Tudor Jebelean.Systolic Multiprecision Arithmetics. RISC, Johannes Kepler University Linz. PhD Thesis.1994.[bib]
1993
B. Buchberger, T. Jebelean.Systolic Multiprecision Arithmetic. In: Proceedings of Impact TEMPUS JEP and Hungarian Transputer Users Group Workshop "Parallel Processing in Education", - (ed.), pp. -.March1993.Miskolc, Hungary,-.[bib]
1992
B. Buchberger, J. Elias.Using Groebner Bases for Detecting Polynomial Identities. A Case Study on Fermat's Ideal.Journal of Number Theory41(3), pp. 272-279.July1992.Academic Press, New York,0022-314X/92.[pdf][bib]
1991
B. Buchberger.Groebner Bases in Mathematica: Enthusiasm and Frustration. In: Proceedings of the IFIP Working Conference on Programming Environments for High-Level Symbolic Computation, September 23-27, Karlsruhe, Germany, P. W. Gaffney, E. N. Houstis (ed.), pp. 80-91.1991.Copyright: IBM, Bergen Scientific Center Publishing,-.[pdf][bib]
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]
B. Buchberger, T. Jebelean.Systolic Algorithms in Computer Algebra. In: Proceedings of the NATO ASI on Parallel Processing on Distributed Memory Multiprocessors, - (ed.), pp. -.July1991.Ankara,-.[bib]
1990
B. Buchberger.Should Students Learn Integration Rules?.ACM SIGSAM Bulletin24(1), pp. 10-17.January1990.-.[pdf][bib]
E. Kaltofen, B. Buchberger.Editorial for Special Issue Computational Algebraic Complexity. In: Journal of Symbolic Computation, E. Kaltofen, B. Buchberger (ed.)Vol.9, pp. 225-228.1990.Academic Press Limited,0747-7171/90.[pdf][bib]
1989
F. Winkler.Equational Theorem Proving and Rewrite Rule Systems. In: 5. Österreichische Artificial-Intelligence-Tagung, J. Retti and K. Leidlmair (ed.), Informatik Fachberichte 208, pp. 26-39.1989.Springer-Verlag,ISBN:3-540-51039-7.[pdf][bib]
1988
B. Buchberger, G. E. Collins, B. Kutzler.Algebraic Methods for Geometric Reasoning. In: Annual Reviews in Computer Science, J. F. Traub (ed.)Vol. 3, pp. 85-119.1988.Copyright: Annual Reviews Inc.,ISSN 8756-7016/88.[pdf][bib]
1987
B. Buchberger.History and Basic Features of the Critical-Pair/Completion Procedure.Journal of Symbolic Computation3(1/2), pp. 3-38.1987.Copyright: Academic Press Inc., Harcourt Brace Jovanovich Publishers, London,ISSN 0747-7171.(Earlier version appeared in: Proceedings of the Conference on Rewrite Technique and Applications, Dijon, May 1985, Lecture Notes in Computer Science, Vol. 202, Springer, 1985, pp. 1-45).[pdf][bib]
B. Buchberger.Applications of Groebner Bases in Non-Linear Computational Geometry. In: IMA Volumes in Mathematics and its Applications, Vol. 14, J. R. Rice (ed.), Proceedings of Workshop on Scientific Software, Minneapolis, USA, March 23-26, 1987, pp. 59-88.1987.Copyright: Springer, New York,-.[pdf][pdf][pdf][bib]
B. Buchberger.The Parallelization of Critical-Pair/Completion Procedures on the L-Machine. In: Proceedings of the Japanese Symposium on Functional Programming, RIKEN Institute, - (ed.), pp. 54-61.February1987.-.[bib]
1986
B. Buchberger, B. Kutzler.Computer-Algebra fuer den Ingenieur (Computer Algebra for the Engineer). In: Rechnerorientierte Verfahren, B. Buchberger and B. Kutzler and M. Feilmeier and M. Kratz and U. Kulisch and S. Rump (ed.), pp. 11-68.1986.Teubner Verlag, Stuttgart,ISBN 3-519-02617-1.[pdf][pdf][pdf][bib]
F. Winkler, B. Buchberger.A Criterion for Eliminating Unnecessary Reductions in the Knuth-Bendix Algorithm. In: Proceedings of Algebra and Logic in Computer Science, Gyor, Hungary, J. Demetrovics, G. Katona, A. Salomaa (ed.), Colloquia Mathematica Societatis Janos Bolyai42, pp. 849-869.September1986.North Holland,ISBN-10: 0444986952; ISBN-13: 978-0444986955.[pdf][bib]
1985
F. Winkler, B. Buchberger, F. Lichtenberger, H. Rolletschek.Algorithm 628: An Algorithm for Constructing Canonical Bases of Polynomial Ideals.ACM Transactions on Mathematical Software11(1), pp. 66-78.March1985.ACM,no.[pdf][bib]
B. Buchberger.Mathematik fuer Informatiker: Ein algorithmenorientierte Ansatz an der Universitaet Linz (Mathematics for Computer Scientists: An Algorithm Oriented Approach at the University of Linz). In: Proceedings of the Mathematica Didactics Conference, Kassel, Oct. 4-6, 1984, R. Schaper (ed.), pp. 156-172.1985.Copyright: Leuchtturm Verlag,-.[bib]
B. Buchberger, P. Hintenaus.The L-Language for the Parallel L-Machine (A Parallel Architecture for AI Applications). In: Proceedings of the Conference of the Austrian Society for Aritificial Intelligence, Vienna, H. Trost, J. Retti (ed.), Informatik-Fachberichte106, pp. 120-131.September1985.Copyright: Springer - Verlag Berlin,ISBN 3-540-15695-X.[pdf][bib]
B. Buchberger.The L-Machine: An Attempt at Parallel Hardware for Symbolic Computation. In: Proceedings of the AAECC Conference, Grenoble, J. Calmet (ed.), Springer Lecture Notes in Computer Science229, pp. 333-347.July1985.ISBN 978-3-540-16776-1.[pdf][bib]
B. Buchberger.History and Basic Features of the Critical-Pair/Completion Approach. In: Proceedings of the Conference on Rewriting Techniques and Applications, Dijon, J.-P. Jouannaud (ed.), Lecture Notes in Computer Science202, pp. 1-45.May1985.Springer,ISBN 978-3-540-15976-6.[bib]
B. Buchberger.The Parallel L-Machine for Symbolic Computation. In: Proceedings of EUROCAL '85 (European Conference on Computer Algebra), Linz, Austria, April 1-3, 1985, Proceedings Vol.2: Research Contributions, B.F. Caviness (ed.), Lectures Notes in Computer Science204, pp. 541-542.1985.Copyright: Springer - Verlag Berlin,ISBN 3-540-15984-3.[pdf][bib]
F. Lichtenberger, B. Buchberger.Mathematik fuer Informatiker: Ein algorithmenorienter Ansatz an der Universitaet Linz (Mathematics for Computer Scientists: An Algorithm Oriented Approach at the University of Linz). In: Special issue: Proceedings of the Symposium "Lehr- und Lernprozesse in der Ingenieurausbildung", Technische Universitaet Graz, Austria, October 8-9, 1985, - (ed.), Zeitschrift fuer Hochschuldidaktik9/10, pp. 103-110.1985.ISBN 3-900386-10-2.[pdf][bib]
B. Buchberger.Groebner-Bases: An Algorithmic Method in Polynomial Ideal Theory. In: Multidimensional Systems Theory - Progress, Directions and Open Problems in Multidimensional Systems, N.K. Bose (ed.), Chapter 6, pp. 184-232.1985.Copyright: Reidel Publishing Company, Dordrecht - Boston - Lancaster, The Netherlands, ISBN 90-277-1764-8, ISBN 1-4020-1623-9.(Second editioin: N.K.Bose (ed.): Multidimensional Systems Theory and Application, Kluwer Academic Publisher, 2003, pp.89-128.).[pdf][pdf][bib]
B. Buchberger et al..Symbolic Computation (An Editorial). In: Journal of Symbolic Computation, B. Buchberger (ed.)Vol. 1/1, pp. 1-6.1985.Academic Press Inc., Harcourt Brace Jovanovich Publishers, London,ISSN 0747-7171.[pdf][bib]
1984
W. Bibel, B. Buchberger.Towards a Connection Machine for Logical Inference. In: Fifth Generation and Supercomputer Conference, Rotterdam, - (ed.), pp. 177-188.December1984.-.( Appeared in Future Generation Computer Systems 1/3).[pdf][bib]
B. Buchberger.The Present State of the L-Networks Project. In: Proceedings MIMI 84 (Conference on Mini- and Microcomputers and Their Applications), Bari, Juni 5-8, 1984, G. Mastronardi (ed.), pp. 178-181.1984.Copyright: Acta Press, Anaheim - Calgary - Zurich,ISBN 0-88986-058-0.[pdf][bib]
B. Buchberger.A Critical-Pair/Completion Algorithm for Finitely Generated Ideals in Rings. In: Logic and Machines: Decision Problems and Complexity (Proceedings of the Symposium "Rekursive Kombinatorik", Muenster, May 23-28, 1983), E. Boerger, G. Hasenjaeger, D. Roedding (ed.), Lecture Notes in Computer Science171, pp. 137-161.1984.Copyright: Springer - Verlag, Berlin - Heidelberg - New York -Tokyo, ISBN 3-540-13331-3, ISBN 0-387-13331-3.[pdf][bib]
B. Buchberger.Automatisches Programmieren (Automated Programming). In: Artificial Intelligence - Eine Einfuehrung, J. Retti et al. (ed.), pp. 169-198.1984.Teubner, Stuttgart, ISBN 3-519-02473-X.[pdf][pdf][pdf][pdf][bib]
1983
B. Buchberger.Components for Restructurable Multi-Microprocessor Systems of Arbitrary Topology. In: Proceedings of the 21st Symposium on Mini- and Microcomputers, MIMI 83, Lugano, - (ed.), pp. 67-71.June1983.-.[bib]
B. Buchberger.A Note on the Complexity of Constructing Groebner-Bases. In: Computer Algebra (Proceedings of EUROCAL 83, European Computer Algebra Conference, London, March 28-30, 1983), J.A. van Hulzen (ed.), Lecture Notes in Computer Science162, pp. 137-145.1983.Copyright: Springer- Verlag Berlin - Heidelberg - New York - Tokyo,ISBN 3-540-12868-9.[pdf][bib]
B. Buchberger.Groebner Bases: A Method in Symbolic Mathematics. In: Proceedings of "Les Journées de Saint-Etienne: Algorithmique, Calcul Formel, Arithmetique", - (ed.), pp. II.1-II.10.October 3-81983.Université de Saint-Etienne, U.E.R de Sciences,CAMP Punl.Nr. 83-24.0.[bib]
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]
1982
H. Moeller, B. Buchberger.The Construction of Multivariate Polynomials with Pre-assigned Zeros. In: Computer Algebra (Proceedings of EUROCAM '82, European Computer Algebra Conference), Marseille, April 5-7, 1982, J. Calmet (ed.), Lecture Notes in Computer Science144, pp. 24-31.1982.Copyright: Springer - Verlag Berlin - Heidelberg - New York,ISBN 3-540-11607-9.[pdf][bib]
B. Buchberger.Computer-unterstuetzter Algorithmenentwurf (Computer-Aided Algorithm Design). In: Proceedings of the Fruehjahrsschule Kuenstliche Intelligenz, Teisendorf, March 15-24, 1982, W. Bibel, J. H. Siekmann (ed.), Informatik-Fachberichte59, pp. 141-202.1982.Copyright: Springer -Verlag Berlin - Heidelberg - New York,ISBN 3-540-11974-4.[pdf][bib]
B. Buchberger, R. Loos.Algebraic Simplification. In: Computer Algebra - Symbolic and Algebraic Computation, B. Buchberger, G. E. Collins, R. Loos (ed.), pp. 11-43.1982.Copyrigth: Springer Verlag, Vienna - New York,-.[pdf][bib]
1981
B. Buchberger, F. Lichtenberger.Mathematik für Informatik I – Die Methode der Mathematik (Mathematics for Computer Science I – The Method of Mathematics).Second edition,1981.Springer-Verlag, Berlin - Heidelberg - New York,ISBN 3-540-11150-6.[pdf][bib]
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, K. Aspetsberger.A Universal Variable-Topology Multi-Microcomputer-System. In: Proc. of the 6th International Symphosium on Mini- and Microcomputers, MIMI '80, Budapest, Hungary, - (ed.), pp. 136-140.September1980.-.[pdf][bib]
L. Bachmair, B. Buchberger.A Simplified Proof of the Characterization Theorem for Groebner-Bases.ACM SIGSAM Bull.14(4), pp. 29-34.November1980.Copyright: ACM, New York.,no.[pdf][bib]
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.A Criterion for Detecting Unnecessary Reductions in the Construction of Groebner Bases. In: Proceedings of the EUROSAM 79 Symposium on Symbolic and Algebraic Manipulation, Marseille, June 26-28, 1979, E. W. Ng (ed.), Lecture Notes in Computer Science72, pp. 3-21.1979.Copyright: Springer, Berlin - Heidelberg - New York,ISBN 3-540-09519-5.[pdf][bib]
B. Buchberger, J. Fegerl, F. Lichtenberger.Computer Trees: A Concept for Parallel Processing.Microprocessing and Microsystems3(6), pp. 244-248.1979.-.[pdf][bib]
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]
1978
B. Buchberger, B. Roider.Input/Output Codings and Transition Functions in Effective Systems.Internat. Journal on General Systems4(3), pp. 201-209.1978.-.[pdf][bib]
B. Buchberger.Computer-Trees and Their Programming. In: Proceedings of the 4th Coll. "Les arbres en algebre et en programmation", February16-18, 1978, University of Lille, Dept. of Computer Science, - (ed.), pp. 1-18.1978.-.[pdf][bib]
B. Buchberger, B. Quatember.Systems with Universal Subsystems: Realization and Application. In: Proceedings of the Fourth European Meeting on Cybernetics and Systems Research, Linz, - (ed.), Progress in Cybernetics and Systems ResearchVol. VII, pp. 25-32.April1978.Hemisphere Publ. Corp.,-.[pdf][bib]
C. Kollreider, B. Buchberger.An Improved Algorithmic Construction of Groebner Bases for Polynomial Ideals.ACM SIGSAM Bull.12(2), pp. 27-36.May1978.-.[pdf][bib]
1977
B. Buchberger, W. Menzel.Simulation-Universal Automata. In: Proceedings of the Internat. Workshop on Semantics of Programming Languages, - (ed.)41, pp. 30-34.March 21-251977.Bad Honnef,Universitaet Dortmund, Abteilung Informatik,-.[bib]
B. Buchberger, W. Menzel.Simulation-Universal Automata. Universitaet Karlsruhe, Fakultaet fuer Informatik I. Technical report no. 14/77, 1977.[bib]
1976
B. Buchberger.Das Problem der Programmverifikation (The Problem of Program Verification). In: Jahrbuch Ueberblicke Mathematik 1976, Bibliographischs Institut, Mannheim, - (ed.), pp. 163-188.1976.Copyright: Bibliographisches Institut AG Zuerich,ISBN 3-411-01505-5.[pdf][bib]
B. Buchberger.A Theoretical Basis for the Reduction of Polynomials to Canonical Forms.ACM SIGSAM Bull.10(3), pp. 19-29.1976.Copyright: ACM, New York,-.[pdf][bib]
B. Buchberger.Some Properties of Groebner Bases for Polynomial Ideals.ACM SIGSAM Bull.10(4), pp. 19-24.1976.Copyright: ACM, New York,-.[pdf][bib]
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]
1974
B. Buchberger.Certain Decompositions of Goedel Numberings and the Semantics of Programming Languages. In: Proceedings of the International Symposium on Theoretical Programming, August 7-11, 1972, Novosibirsk, A. Ershov, V. A. Nepomniaschy (ed.), Lecture Notes in Computer Science5, pp. 152-171.1974.Copyright: Springer - Verlag Berlin - Heidelberg - New York,ISBN 3-540-067200-5.(Appeared earlier in Russian in: Teoriya Programmirovaniya, part I., Trudy Simposiuma, Novosibirsk, 7-11 August, 1972, Ak. Nauk SSSR, Sibirian Division, Computing Center, pp. 250-266).[pdf][bib]
B. Buchberger.On Certain Decompositions of Goedel Numberings.Archiv fuer Math. Logik und Grundlagenforschung16(1-2), pp. 85-96.1974.-.[pdf][bib]
1973
B. Buchberger, G.A. Yemel`yananko.Metody obratscheniya trechdiagonal'nyx matrits (Methods for the Inversion of Tridiagonal Matrices).Zhurnal vych. mat. i mat. fiziki13(3), pp. 546-554.1973.-.(English translation: USSR Computational Mathematics and Mathematical Physics, Vol. 13/3, 1973, pp. 10-20.).[pdf][bib]
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.Bemerkung zu den Reduzierbarkeitskriterien von R.Albrecht fuer das Optimum-Mix-Problem (A Comment on the Reducibility Criteria of R. Albrecht for the Optimum-Mix-Problem).Zeitschrift fuer Operations Research16, pp. 137-143.1972.Physica-Verlag, Wuerzburg,-.[pdf][bib]
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, G.A. Emelyanenko.Metody obrashteniya trehdiagonal'nih matrits (Methods of Inverting Tridiagonal Matrices).Communications of the Joint Institute for Nuclear Research (JINR), DubnaNo. P11-5686, pp. 1-16.1971.-.[pdf][bib]
B. Buchberger.O Velichinah S(i) Opredelennih Rekursiej S(i+1)= u(i) . S(i) + v(i) . S(i-1). (On the Values S(i) Determined by the Recursion S(i+1)= u(i) . S(i) + v(i) . S(i-1)).Communications of the Joint Institute for Nuclear Research (JINR), DubnaNo. P5-5789, pp. 1-12.1971.-.[abstract][pdf][ps][bib]
B. Buchberger.Associiruyushtshije Funksii i Operator Obyslovlennoj Iteratsii (Associating Functions and the Operator of Conditioned Iteration).Communications of the Joint Institute for Nuclear Research (JINR), DubnaNo. P5-5788, pp. 1-18.1971.no.(English Translation: Bericht Nr. 71-1, June 1971, 16 pages, Universitaet Innsbruck, Institut fuer Informatik.).[pdf][pdf][abstract][bib]
B. Buchberger.An Extension of ALGOL 60.Communications of the Joint Institute for Nuclear Research (JINR), DubnaNo. E5-5787, pp. 1-14.1971.-.[abstract][pdf][bib]
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]
1970
R. Albrecht, B. Buchberger.Algorithm 13: Loesung eines Optimum-Mix Problemes (Solution of an Optimum-Mix-Problem).Computing5, pp. 324-331.1970.Copyright: Springer Verlag,-.[pdf][bib]
B. Buchberger.Ein algorithmisches Kriterium fuer die Loesbarkeit eines algebraischen Gleichungssystems (An Algorithmic Criterion for the Solvability of Algebraic Systems of Equations).Aequationes mathematicae3, pp. 374-383.1970.Copyright: Birkhaeuser Verlag AG, Basel, Switzerland,-.(english transl.: B. Buchberger, F. Winkler: Groebner Bases and Applications, Proc. of the International Conference "33 Years of Groebner Bases", 1998, RISC, Austria, London Math. Society Lecture Note Series 251, Cambridge Univ. Press, 1998, pp.535 -545).[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]
1965
B. Buchberger.Ein Algorithmus zum Auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal (An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal). Mathematical Institute, University of Innsbruck, Austria. PhD Thesis.1965.English translation in J. of Symbolic Computation, Special Issue on Logic, Mathematics, and Computer Science: Interactions. Vol. 41, Number 3-4, Pages 475-511, 2006.[pdf][bib]