J. Ablinger, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, Kay Schoenwald.The two-mass contributions to the three-loop massive operator matrix elements $tilde{A}_{Qg}^{(3)}$ and $Delta tilde{A}_{Qg}^{(3)}$.Journal of High Energy Physics2026(111), pp. 1-52.2026.ISSN 1029-8479.arXiv:2510.09403 [hep-ph].[doi][bib]
J. Ablinger, A. Behring, J. Bluemlein, d, A. De Freitas, A. von Manteuffel, C. Schneider, and K. Schoenwald.The single-mass variable flavor number scheme at three-loop order.Journal of High Energy Physics2026(248), pp. 0-33.2026.SSN 1029-8479.arXiv:2510.02175 [hep-ph].[doi][bib]
J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald.The complete three-loop unpolarized and polarized massive operator matrix elements and asymptotic Wilson coefficients. Technical report no. 26-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2026. Licensed under CC BY 4.0 International.[doi][pdf][bib]
A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald.The heavy quark-antiquark asymmetry in the variable flavor number scheme.Physics Letters B876(140411), pp. 1-8.2026.ISSN 1873-2445.arXiv:2512.13508 [hep-ph].[doi][bib]
J. Ablinger, A. Behring, J. Blümlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schönwald.The three-loop single-mass heavy-flavor corrections to the structure functions $F_2(x, Q^2)$ and $g_1(x, Q^2)$.Physics Letters B878(140540), pp. 1-8.2026.ISSN 0370-2693.arXiv:2509.16124 [hep-ph].[doi][bib]
Besik Dundua, Georg Ehling, Santiago Escobar, Maribel Fernández, Temur Kutsia.Quantitative Equational Rewriting. Technical report no. 26-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).June2026. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Mara Antesberger.Extending Approximate Reasoning to Unranked Term Structures. Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Master Thesis.2026.[pdf][bib]
C. Schneider.A Survey on Symbolic Summation in Difference Rings. Technical report no. 26-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).May2026. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Wolfgang Schreiner.Building a Logical Agent with LangChain ... and Quite Some Vibe Coding. Technical report no. 26-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March2026. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Tereso del Río, Wolfgang Schreiner, Martina Seidl, Temur Kutsia, Wolfgang Windsteiger .An Intermediate Representation Format for Industrial Optimization Problems - The Translation of OptDSL to MiniZinc. Technical report no. 26-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2026. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Wolfgang Schreiner.On the Rapid Prototyping of a Logical Agent. In: SCML-2026: International Conference on Symbolic Computation and Machine Learning - Extended Abstracts, Bruno Buchberger, François Charton, Matthew England, Cezary Kaliszyk, Manuel Kauers, Hiroshi Kera, Temur Kutsia, Bernhard Moser, Markus Schedl, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteiger (ed.), RISC Proceedings on Symbolic Computation and Machine Learning3, pp. 78-79.2026.SCML,https://scml.risc.jku.at/,ISSN XXXX.[doi][bib]
Verena Praher, Endre Szasz-Revai, Wolfgang Windsteiger.Reasoning over Legal Texts Using Large Language Models and Automated Reasoning. In: SCML-2026: International Conference on Symbolic Computation and Machine Learning - Extended Abstracts, Bruno Buchberger, François Charton, Matthew England, Cezary Kaliszyk, Manuel Kauers, Hiroshi Kera, Temur Kutsia, Bernhard Moser, Markus Schedl, Wolfgang Schreiner, Martina Seidl, Wolfgang Windsteig (ed.), RISC Proceedings on Symbolic Computation and Machine Learning3, pp. 76-77.2026.SCML,https://scml.risc.jku.at/,ISSN xxxx.[doi][pdf][bib]
2025
Alexander Baumgartner, Temur Kutsia, Daniele Nantes-Sobrinho, Manfred Schmidt-Schauss.Equational Generalization Problems with Atom-Variables. In: Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings, Valeria de Paiva and Peter Koepke (ed.), Lecture Notes in Computer Science16136, pp. 133-151.2025.Springer,ISBN 978-3-032-07020-3.[doi][bib]
Alexander Baumgartner, Temur Kutsia.Quantitative generalization of variadic structures with binders. Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Technical report, 2025.[pdf][bib]
Mauricio Ayala-Rincón, David Cerna, Temur Kutsia, Christophe Ringeissen.Combining Generalization Algorithms in Regular Collapse-Free Theories. In: Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), Maribel Fernandez (ed.), LIPIcs - Leibniz International Proceedings in Informatics337, pp. 7:1-7:18.2025.Schloss Dagstuhl - Leibniz-Zentrum für Informatik,ISBN 978-3-95977-374-4.[doi][bib]
Shaoshi Chen, Hao Du, Yiman Gao, Hui Huang, Ziming Li.A Unified Reduction for Hypergeometric and $q$-Hypergeometric Creative Telescoping.The Ramanujan J.68(14), pp. 1-39.2025.ISSN 1572-9303.arXiv:2501.03837 [cs.SC].[doi][pdf][bib]
Diego Dominici, Francisco Marcellán.Linear functionals and Δ-coherent pairs of the second kind .Revista Union Matematica Argentina68(2), pp. 405-422.2025.1669-9637.[doi][bib]
Besik Dundua, Temur Kutsia.Higher-Order Pattern Unification Modulo Similarity Relations. Technical report no. 25-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2025. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Besik Dundua, Temur Kutsia.Higher-Order Pattern Unification Modulo Similarity Relations. In: Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2025, Santiago Escobar and Laura Titolo (ed.), Lecture Notes in Computer Science16117, pp. 75-93.2025.Springer,ISBN 978-3-032-04847-9.[doi][pdf][bib]
Mauricio Ayala-Rincon, Thaynara Arielly de Lima, Georg Ehling, Temur Kutsia.Graded Quantitative Narrowing. In: Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings, Valeria de Paiva and Peter Koepke (ed.), Lecture Notes in Computer Science16136, pp. 113-132.2025.Springer,ISBN 978-3-032-07020-3.[doi][bib]
Nikolai Fadeev.Computer algebra for special functions. RISC, Johannes Kepler University Linz. PhD Thesis.May2025.[bib]
Hao Du, Yiman Gao, Wenqiao Li and Ziming Li.Complete Reduction for Derivatives in a Primitive Tower. In: Proceedings of the 2025 International Symposium on Symbolic and Algebraic Computation (ISSAC’25, Santiago Laplagne (ed.), pp. 42-51.2025.979-8-4007-2075-8/25/07.[bib]
Ralf Hemmecke, Peter Paule, Cristian-Silviu Radu.Computer-assisted construction of Ramanujan-Sato series for 1 over pi. Technical report no. 25-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).January2025. Licensed under CC BY 4.0 International.[doi][pdf][pdf][bib]
Ralf Hemmecke, Peter Paule, Cristian-Silviu Radu.An Algorithm to Compute Algebraic Relations Between Modular Functions. Technical report no. 25-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).November2025. Licensed under CC BY 4.0 International.[doi][pdf][bib]
E. Hoxhaj, J. Schicho.How to reconstruct a planar map from its branching curve.Math. Comp.94, pp. 935-952.2025.ISSN 1088-6842.[doi][bib]
Andr'as Kerekes, Zolt'an Kov'acs.Towards automatic detection of geometric difficulty of geometry problems.Maple Transactions, pp. to appear-.2025. ISSN 2564-3029.to appear.[bib]
Yang Wei-Chi, Kov'acs Zolt'an, Dana-Picard Thierry.Topology of Quartic Loci in 2D and 3D Inspired by A College Entrance Exam.The Electronic Journal of Mathematics and Technology19(1), pp. 1-14.2025.ISSN 1933-2823.[url][bib]
Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano Miguel Moscato, and Temur Kutsia.Verification of an Anti-unification Algorithm in PVS. In: NASA Formal Methods, Aaron Dutle, Laura Humphrey, Laura Titolo (ed.), Proceedings of The 17th NASA Formal Methods Symposium, NFM 2025, Williamsburg, VA, USA, Lecture Notes in Computer Science15682, pp. 54-71.2025.Springer,ISBN 978-3-031-93705-7.[doi][bib]
M. Makhul, J. Schicho, A. Warren.On Galois groups of type I minimally rigid graphs.Discr. Comp. Geom., pp. -.2025.0179-5376.[doi][bib]
N. Lubbes, M. Makhul, J. Schicho, A. Warren.Irreducible components of sets of points in the plane that satisfy distance conditions.Foundations of Computational Mathematics, pp. -.2025.1615-3375.[doi][bib]
P. Paule, C. Schneider.Creative Telescoping for Hypergeometric Double Sums.J. Symb. Comput.128(102394), pp. 1-30.2025.ISSN: 0747-7171.Symbolic Computation and Combinatorics: A special issue in memory and honor of Marko Petkovšek, edited by Shaoshi Chen, Sergei Abramov, Manuel Kauers, Eugene Zima.[doi][bib]
Koustav Banerjee, Peter Paule, Cristian-Silviu Radu, Carsten Schneider.Asymptotics for the reciprocal and shifted quotient of the partition function.Research in Number Theory11(101), pp. 1-46.2025.ISSN 2363-9555. arXiv:2412.02257 [math.NT].[doi][bib]
S. Chen and Y. Gao and H. Huang and C. Schneider.Telescoping Algorithms for $Sigma^*$-Extensions via Complete Reductions. In: Recent Trends in Computer Algebra, Bruno Salvy, Alin Bostan, Mohab Safey El Din, Gilles Villard (ed.), Texts & Monographs in Symbolic Computation, pp. ?-?.2025.Springer Nature,arXiv:2506.08767 [cs.SC].[doi][bib]
Wolfgang Schreiner, William Steingartner.Semantics-Based Rapid Prototyping of a Subset of SQL. Technical report no. 25-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).February2025. Licensed under CC BY 4.0 International.[doi][pdf][bib]
William Steingartner, Wolfgang Schreiner.Executable Semantics for Teaching Concatenative Stack-Based DSLs: The Case of StackLang. In: New Trends in Database and Information Systems, ADBIS 2025 Short Papers, Doctoral Consortium and Tutorials, Tampere, Finland, September 23-26, 2025, Proceedings, Panos K. Chrysanthis, Kjetil Nørvåg, Kostas Stefanidis, Zheying Zhang, Elisa Quintarelli, Ester Zumpano (ed.), Communications in Computer and Information Science (CCIS)2676, pp. 248-263.2025.Springer,Cham, Switzerland,ISBN 978-3-032-05726-6.[doi][bib]
Wolfgang Schreiner.Thinking Programs.Texts & Monographs in Symbolic Computation2nd edition,2025.Springer, Cham, Switzerland,Hardcover ISBN 978-3-031-99704-4, Softcover ISBN 978-3-031-99707-5, eBook ISBN 978-3-031-99705-1.[doi][bib]
Tereso del Rio, Wolfgang Schreiner, Martina Seidl, Temur Kutsia, Wolfgang Windsteiger.A DSL for Specifying a Class of Industrial Optimisation Problems. Technical report no. 25-12 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).December2025. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Jack Heseltine.Theorema Project: Document Processing. Technical report no. 25-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).March 022025.Bachelor Thesis at University of Applied Sciences Hagenberg, bachelor program Software Engineering. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Viktoria Langenreither.A Saturation-Based Automated Theorem Prover for RISCAL. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Master Thesis.December2025.Also available as RISC report no. 25-11.[doi][pdf][bib]
Daniel D. Sunthimer.An Implementation of Approximate Generalization in Quantitative Theories. Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Bachelor Thesis.2025.[pdf][bib]
2024
Maximilian Donnermair.Proximity-based matching with arbitrary T-norms. RISC, Johannes Kepler University Linz. Bachelor Thesis.2024.[pdf][bib]
Thaynara Arielly de Lima, André Luiz Galdino, Bruno Berto de Oliveira Ribeiro, and Mauricio Ayala-Rincón.A Formalization of the General Theory of Quaternions. In: Leibniz International Proceedings in Informatics (LIPIcs), Yves Bertot, Temur Kutsia, and Michael Norrish (ed.), pp. 11:1-11:18.2024.ISSN 1868-8969.[bib]
de Lima Thaynara Arielly, Borges Avelar Andréia, Galdino André Luiz, Ayala-Rincón Mauricio.Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms. In: Electronic Proceedings in Theoretical Computer Science, Temur Kutsia, Daniel Ventura, David Monniaux & José F. Morales (ed.)402, pp. 18–33-18–33.2024.Open Publishing Association, ISSN 2075-2180.[doi][bib]
de Lima Thaynara Arielly, Borges Avelar Andréia, Galdino André Luiz, Ayala-Rincón Mauricio.Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms. In: Electronic Proceedings in Theoretical Computer Science, Temur Kutsia, Daniel Ventura, David Monniaux and José F. Morales (ed.)402, pp. 18–33-18–33.2024.Open Publishing Association, ISSN 2075-2180.[doi][bib]
Bruno Buchberger.Science and Meditation: Creating the Future (English Translation of "Wissenschaft und Meditation").1st edition,2024.Amazon, 979-8332230837.[bib]
Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia.Equational Anti-unification over Absorption Theories. In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence14740, pp. 317-337.2024.Springer,ISBN 978-3-031-63500-7.[doi][bib]
J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald.The first-order factorizable contributions to the three-loop massive operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$.Nuclear Physics B999(116427), pp. 1-42.2024.ISSN 0550-3213.arXiv:2311.00644 [hep-ph].[doi][bib]
J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald.The non-first-order-factorizable contributions to the three-loop single-mass operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$.Physics Letter B854(138713), pp. 1-8.2024.ISSN 0370-2693.arXiv:2403.00513 [[hep-ph].[doi][bib]
J Bluemlein, A. De Freitas, P. Marquard, C. Schneider.Challenges for analytic calculations of the massive three-loop form factors. In: Proceedings of Loops and Legs in Quantum Field Theory, P. Marquard, M. Steinhauser (ed.)PoS(LL2024)031/24-05, pp. 1-18.2024.ISSN 1824-8039. arXiv:2408.07046 [hep-ph].[doi][bib]
J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald.The three-loop single-mass heavy flavor corrections to deep-inelastic scattering. In: Proceedings of Loops and Legs in Quantum Field Theory, P. Marquard, M. Steinhauser (ed.)PoS(LL2024)047 , pp. 1-12.2024.SSN 1824-8039.arXiv:2407.02006 [hep-ph].[doi][bib]
Fabián Fernando Serrano Suárez, Thaynara Arielly de Lima, Mauricio Ayala-Rincón.Compactness Theorem for Propositional Logic and Combinatorial Applications.Arch. Formal Proofs2024, pp. -.2024. ISSN 2150-914x.[url][bib]
de Lima Thaynara Arielly, Galdino André Luiz, de Oliveira Ribeiro Bruno Berto, Ayala-Rincón Mauricio Bertot, Yves and Kutsia, Temur and Norrish, Michael.A Formalization of the General Theory of Quaternions. In: 15th International Conference on Interactive Theorem Proving (ITP 2024), Bertot, Yves and Kutsia, Temur and Norrish, Michael (ed.), Leibniz International Proceedings in Informatics (LIPIcs)309, pp. 11:1-11:18.2024.Dagstuhl, Germany,ISBN 978-3-95977-337-9 ISSN 1868-8969.[url][bib]
Lucas A. da Silveira, Thaynara A. de Lima, Mauricio Ayala-Rincón.On reconfiguring heterogeneous parallel island models.Swarm and Evolutionary Computation89, pp. 101624-101624.2024. ISSN 2210-6502.[url][bib]
Diego Dominici, Juan Carlos García-Ardila, Francisco Marcellán.Symmetrization process and truncated orthogonal polynomials. Analysis and Mathematical Physics14, pp. 0-0.112024. 1664-2368.[bib]
I. Dramnesc, T. Jebelean, S. Stratulat.Certification of Tail Recursive Bubble-Sort in Theorema and Coq. In: LPAR 2024 Complementary Volume, N. Bjørner, M. Heule, A. Voronkov (ed.), Kalpa Publications in Computing18, pp. 53-68.2024.EasyChair, ISSN 2515-1762.[url][bib]
I. Dramnesc, T. Jebelean, S. Stratulat.Certification of Sorting Algorithms Using Theorema and Coq. In: SCSS 2024, Symbolic Computation in Software Science , S. M. Watt, T. Ida (ed.), Lecture Notes in Artificial Intelligence14991, pp. 38-56.2024.Springer,ISBN 978-3-031-69041-9.[bib]
G. Ehling, T. Kutsia.Solving Quantitative Equations. Technical report no. 24-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).April2024. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Georg Ehling, Temur Kutsia.Solving Quantitative Equations. In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence14740, pp. 381-400.2024.Springer,ISBN 978-3-031-63500-7.[doi][bib]
T. Jebelean.A Natural-style Prover in Theorema Using Sequent Calculus with Unit Propagation. In: LPAR 2024 Complementary Volume, N. Bjørner, M. Heule, A. Voronkov (ed.), Kalpa Publications in Computing18, pp. 107-116.2024.EasyChair, ISSN 2515-1762.[url][bib]
Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, Daniele Nantes-Sobrinho.Certified First-Order AC-Unification and Applications.Journal of Automated Reasoning68(4), pp. 25:1-25:48.2024.ISSN 0168-7433.[doi][pdf][bib]
Z. Chen, Z. Chen, J. Obrovsky, A. Winterhof.Maximum-order Complexity and 2-Adic Complexity.IEEE Transactions on Information Theory70(8), pp. 6060-6067.2024.ISSN: 0018-9448.[doi][bib]
George E. Andrews, Peter Paule.MacMahon's partition analysis XIV: Partitions with n copies of n.Journal of Combinatorial Theory203, pp. 0-0.2024.Elsevier,0097-3165.[doi][bib]
Peter Paule.Askey, Heron, and Computer Algebra. RISC. Technical report no. 24-09, 122024.[pdf][bib]
George E. Andrews, Peter Paule.MacMahon's partition analysis XV: Parity.Journal of Symbolic Computation127, pp. 0-0.2024.RISC,0747-7171.[doi][bib]
Jiayue Qi.A tree-based algorithm for the integration of monomials in the Chow ring of the moduli space of stable marked curves of genus zero.Journal of Symbolic Computation122(102253), pp. -.2024.ISSN: 0747-7171.[doi][bib]
N. Lubbes, J. Schicho.Calibrating figures.Comp. Aided Geom. Design112, pp. -.2024.ISSN 1879-2332.[doi][bib]
E.D. Ocansey, C. Schneider.Representation of hypergeometric products of higher nesting depths in difference rings.J. Symb. Comput.120, pp. 1-50.2024.ISSN: 0747-7171.arXiv:2011.08775 [cs.SC].[doi][bib]
Koustav Banerjee, Peter Paule, Cristian-Silviu Radu, Carsten Schneider.Error bounds for the asymptotic expansion of the partition function.Rocky Mt J Math 54(6), pp. 1551-1592.2024.ISSN: 357596.arXiv:2209.07887 [math.NT].[doi][pdf][bib]
Wolfgang Schreiner, William Steingartner.Semantics-Based Rapid Prototyping of a Machine Controller Language. In: 2024 IEEE 17th International Scientific Conference on Informatics, Poprad, Slovakia, November 13-15, Valerie Novitzká, Anikó Szakál (ed.), pp. 348-353.2024.IEEE,ISBN 979-8-3503-8767-4.[doi][bib]
Christian Huber.Highway Node Routing. Technical report no. 24-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July2024.Bachelor thesis at RISC, Johannes Kepler University Linz. Licensed under CC BY 4.0 International.[doi][pdf][bib]
W. Windsteiger.Gray-Box Proving in Theorema. Technical report no. 24-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online).July2024. Licensed under CC BY 4.0 International.[doi][pdf][bib]
Windsteiger Wolfgang.Gray-Box Proving in Theorema . In: 26th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2024), Fairouz Kamareddine, Mircea Marin (ed.), pp. 82-89.2024.IEEE Computer Society,Los Alamitos, CA, USA,ISBN: 979-8-3315-3283-3.[doi][bib]
