# A Special Function Tool-Box for High-Order Finite Element Methods

### Project Description

Subproject of F1301 (FWF-SFB F013)

### Project Lead

### Project Duration

01/03/2004 - 29/02/2008## Partners

### The Austrian Science Fund (FWF)

## Publications

### 2021

[Ablinger]

### Extensions of the AZ-algorithm and the Package MultiIntegrate

#### J. Ablinger

Technical report no. 21-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). January 2021. [doi] [pdf]@

author = {J. Ablinger},

title = {{Extensions of the AZ-algorithm and the Package MultiIntegrate}},

language = {english},

abstract = {We extend the (continuous) multivariate Almkvist-Zeilberger algorithm inorder to apply it for instance to special Feynman integrals emerging in renormalizable Quantum field Theories. We will consider multidimensional integrals overhyperexponential integrals and try to find closed form representations in terms ofnested sums and products or iterated integrals. In addition, if we fail to computea closed form solution in full generality, we may succeed in computing the firstcoeffcients of the Laurent series expansions of such integrals in terms of indefnitenested sums and products or iterated integrals. In this article we present the corresponding methods and algorithms. Our Mathematica package MultiIntegrate,can be considered as an enhanced implementation of the (continuous) multivariateAlmkvist Zeilberger algorithm to compute recurrences or differential equations forhyperexponential integrands and integrals. Together with the summation packageSigma and the package HarmonicSums our package provides methods to computeclosed form representations (or coeffcients of the Laurent series expansions) of multidimensional integrals over hyperexponential integrands in terms of nested sums oriterated integrals.},

number = {21-02},

year = {2021},

month = {January},

keywords = {multivariate Almkvist-Zeilberger algorithm, hyperexponential integrals, iterated integrals, nested sums},

length = {25},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

**techreport**{RISC6272,author = {J. Ablinger},

title = {{Extensions of the AZ-algorithm and the Package MultiIntegrate}},

language = {english},

abstract = {We extend the (continuous) multivariate Almkvist-Zeilberger algorithm inorder to apply it for instance to special Feynman integrals emerging in renormalizable Quantum field Theories. We will consider multidimensional integrals overhyperexponential integrals and try to find closed form representations in terms ofnested sums and products or iterated integrals. In addition, if we fail to computea closed form solution in full generality, we may succeed in computing the firstcoeffcients of the Laurent series expansions of such integrals in terms of indefnitenested sums and products or iterated integrals. In this article we present the corresponding methods and algorithms. Our Mathematica package MultiIntegrate,can be considered as an enhanced implementation of the (continuous) multivariateAlmkvist Zeilberger algorithm to compute recurrences or differential equations forhyperexponential integrands and integrals. Together with the summation packageSigma and the package HarmonicSums our package provides methods to computeclosed form representations (or coeffcients of the Laurent series expansions) of multidimensional integrals over hyperexponential integrands in terms of nested sums oriterated integrals.},

number = {21-02},

year = {2021},

month = {January},

keywords = {multivariate Almkvist-Zeilberger algorithm, hyperexponential integrals, iterated integrals, nested sums},

length = {25},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

[Cerna]

### A Special Case of Schematic Syntactic Unification

#### David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]@

author = {David M. Cerna},

title = {{A Special Case of Schematic Syntactic Unification}},

language = {english},

abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},

year = {2021},

institution = {CAS ICS / RISC},

length = {8}

}

**techreport**{RISC6349,author = {David M. Cerna},

title = {{A Special Case of Schematic Syntactic Unification}},

language = {english},

abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},

year = {2021},

institution = {CAS ICS / RISC},

length = {8}

}

[Dundua]

### Variadic equational matching in associative and commutative theories

#### Besik Dundua, Temur Kutsia, Mircea Marin

Journal of Symbolic Computation 106, pp. 78-109. 2021. Elsevier, ISSN 0747-7171. [doi] [pdf]@

author = {Besik Dundua and Temur Kutsia and Mircea Marin},

title = {{Variadic equational matching in associative and commutative theories}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {106},

pages = {78--109},

publisher = {Elsevier},

isbn_issn = {ISSN 0747-7171},

year = {2021},

refereed = {yes},

length = {32},

url = {https://doi.org/10.1016/j.jsc.2021.01.001}

}

**article**{RISC6260,author = {Besik Dundua and Temur Kutsia and Mircea Marin},

title = {{Variadic equational matching in associative and commutative theories}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {106},

pages = {78--109},

publisher = {Elsevier},

isbn_issn = {ISSN 0747-7171},

year = {2021},

refereed = {yes},

length = {32},

url = {https://doi.org/10.1016/j.jsc.2021.01.001}

}

[Falkensteiner]

### On Initials and the Fundamental Theorem of Tropical Partial Differential Geometry

#### S. Falkensteiner, C. Garay-Lopez, M. Haiech, M. P. Noordman, F. Boulier, Z. Toghani

Journal of Symbolic Computation, pp. 1-22. 2021. ISSN: 0747-7171. [url]@

author = {S. Falkensteiner and C. Garay-Lopez and M. Haiech and M. P. Noordman and F. Boulier and Z. Toghani},

title = {{On Initials and the Fundamental Theorem of Tropical Partial Differential Geometry}},

language = {english},

journal = {Journal of Symbolic Computation},

pages = {1--22},

isbn_issn = {ISSN: 0747-7171},

year = {2021},

refereed = {yes},

keywords = {Differential Algebra, Tropical Differential Algebraic Geometry, Power Series Solutions, Newton Polyhedra, Arc Spaces, Tropical Differential Equations, Initial forms of Differential Polynomials},

length = {22},

url = {http://hal.archives-ouvertes.fr/hal-03122437v1/document}

}

**article**{RISC6335,author = {S. Falkensteiner and C. Garay-Lopez and M. Haiech and M. P. Noordman and F. Boulier and Z. Toghani},

title = {{On Initials and the Fundamental Theorem of Tropical Partial Differential Geometry}},

language = {english},

journal = {Journal of Symbolic Computation},

pages = {1--22},

isbn_issn = {ISSN: 0747-7171},

year = {2021},

refereed = {yes},

keywords = {Differential Algebra, Tropical Differential Algebraic Geometry, Power Series Solutions, Newton Polyhedra, Arc Spaces, Tropical Differential Equations, Initial forms of Differential Polynomials},

length = {22},

url = {http://hal.archives-ouvertes.fr/hal-03122437v1/document}

}

[Grasegger]

### Combinatorics of Bricard's octahedra

#### M. Gallet, G. Grasegger, J. Legerský, J. Schicho

Comptes Rendus. Mathématique 359(1), pp. 7-38. 2021. Académie des sciences, Paris, ISSN 1631-073X. [doi]@

author = {M. Gallet and G. Grasegger and J. Legerský and J. Schicho},

title = {{Combinatorics of Bricard's octahedra}},

language = {english},

journal = {Comptes Rendus. Mathématique},

volume = {359},

number = {1},

pages = {7--38},

publisher = {Académie des sciences, Paris},

isbn_issn = {ISSN 1631-073X},

year = {2021},

refereed = {yes},

length = {32},

url = {https://doi.org/10.5802/crmath.132}

}

**article**{RISC6288,author = {M. Gallet and G. Grasegger and J. Legerský and J. Schicho},

title = {{Combinatorics of Bricard's octahedra}},

language = {english},

journal = {Comptes Rendus. Mathématique},

volume = {359},

number = {1},

pages = {7--38},

publisher = {Académie des sciences, Paris},

isbn_issn = {ISSN 1631-073X},

year = {2021},

refereed = {yes},

length = {32},

url = {https://doi.org/10.5802/crmath.132}

}

[Grasegger]

### On the Existence of Paradoxical Motions of Generically Rigid Graphs on the Sphere

#### M. Gallet, G. Grasegger, J. Legerský, J. Schicho

SIAM Journal on Discrete Mathematics 35(1), pp. 325-361. 2021. ISSN 0895-4801. [doi]@

author = {M. Gallet and G. Grasegger and J. Legerský and J. Schicho},

title = {{On the Existence of Paradoxical Motions of Generically Rigid Graphs on the Sphere}},

language = {english},

journal = {SIAM Journal on Discrete Mathematics},

volume = {35},

number = {1},

pages = {325--361},

isbn_issn = {ISSN 0895-4801},

year = {2021},

refereed = {yes},

length = {37},

url = {https://doi.org/10.1137/19M1289467}

}

**article**{RISC6290,author = {M. Gallet and G. Grasegger and J. Legerský and J. Schicho},

title = {{On the Existence of Paradoxical Motions of Generically Rigid Graphs on the Sphere}},

language = {english},

journal = {SIAM Journal on Discrete Mathematics},

volume = {35},

number = {1},

pages = {325--361},

isbn_issn = {ISSN 0895-4801},

year = {2021},

refereed = {yes},

length = {37},

url = {https://doi.org/10.1137/19M1289467}

}

[Hemmecke]

### Construction of Modular Function Bases for $Gamma_0(121)$ related to $p(11n+6)$

#### Ralf Hemmecke, Peter Paule, Silviu Radu

Integral Transforms and Special Functions 32(5-8), pp. 512-527. 2021. Taylor & Francis, 1065-2469. [doi]@

author = {Ralf Hemmecke and Peter Paule and Silviu Radu},

title = {{Construction of Modular Function Bases for $Gamma_0(121)$ related to $p(11n+6)$}},

language = {english},

abstract = {Motivated by arithmetic properties of partitionnumbers $p(n)$, our goal is to find algorithmicallya Ramanujan type identity of the form$sum_{n=0}^{infty}p(11n+6)q^n=R$, where $R$ is apolynomial in products of the form$e_alpha:=prod_{n=1}^{infty}(1-q^{11^alpha n})$with $alpha=0,1,2$. To this end we multiply theleft side by an appropriate factor such the resultis a modular function for $Gamma_0(121)$ havingonly poles at infinity. It turns out thatpolynomials in the $e_alpha$ do not generate thefull space of such functions, so we were led tomodify our goal. More concretely, we give threedifferent ways to construct the space of modularfunctions for $Gamma_0(121)$ having only poles atinfinity. This in turn leads to three differentrepresentations of $R$ not solely in terms of the$e_alpha$ but, for example, by using as generatorsalso other functions like the modular invariant $j$.},

journal = {Integral Transforms and Special Functions},

volume = {32},

number = {5-8},

pages = {512--527},

publisher = {Taylor & Francis},

isbn_issn = {1065-2469},

year = {2021},

refereed = {yes},

keywords = {Ramanujan identities, bases for modular functions, integral bases},

sponsor = {FWF (SFB F50-06)},

length = {16},

url = {https://doi.org/10.1080/10652469.2020.1806261}

}

**article**{RISC6342,author = {Ralf Hemmecke and Peter Paule and Silviu Radu},

title = {{Construction of Modular Function Bases for $Gamma_0(121)$ related to $p(11n+6)$}},

language = {english},

abstract = {Motivated by arithmetic properties of partitionnumbers $p(n)$, our goal is to find algorithmicallya Ramanujan type identity of the form$sum_{n=0}^{infty}p(11n+6)q^n=R$, where $R$ is apolynomial in products of the form$e_alpha:=prod_{n=1}^{infty}(1-q^{11^alpha n})$with $alpha=0,1,2$. To this end we multiply theleft side by an appropriate factor such the resultis a modular function for $Gamma_0(121)$ havingonly poles at infinity. It turns out thatpolynomials in the $e_alpha$ do not generate thefull space of such functions, so we were led tomodify our goal. More concretely, we give threedifferent ways to construct the space of modularfunctions for $Gamma_0(121)$ having only poles atinfinity. This in turn leads to three differentrepresentations of $R$ not solely in terms of the$e_alpha$ but, for example, by using as generatorsalso other functions like the modular invariant $j$.},

journal = {Integral Transforms and Special Functions},

volume = {32},

number = {5-8},

pages = {512--527},

publisher = {Taylor & Francis},

isbn_issn = {1065-2469},

year = {2021},

refereed = {yes},

keywords = {Ramanujan identities, bases for modular functions, integral bases},

sponsor = {FWF (SFB F50-06)},

length = {16},

url = {https://doi.org/10.1080/10652469.2020.1806261}

}

[Jebelean]

### A Heuristic Prover for Elementary Analysis in Theorema

#### Tudor Jebelean

Technical report no. 21-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]@

author = {Tudor Jebelean},

title = {{A Heuristic Prover for Elementary Analysis in Theorema}},

language = {english},

abstract = {We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.},

number = {21-07},

year = {2021},

month = {April},

keywords = {Theorema, S-decomposition, automated theorem proving},

length = {29},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

**techreport**{RISC6293,author = {Tudor Jebelean},

title = {{A Heuristic Prover for Elementary Analysis in Theorema}},

language = {english},

abstract = {We present the application of certain heuristic techniques for the automation of proofs in elementary analysis. the techniques used are: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the [Epsilon]-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admisibility of solutions to the metavariables. The proofs are very similar to those produced automatically, but they are edited for readability and aspect, and also for inserting the appropriate explanation about the use of the proof techniques. The proofs are: convergence of product of two sequences, continuity of the sum of two functions, uniform continuity of the sum of two functions, uniform continuity of the product of two functions, and continuity of the composition of functions.},

number = {21-07},

year = {2021},

month = {April},

keywords = {Theorema, S-decomposition, automated theorem proving},

length = {29},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

[Jimenez Pastor]

### On C2-Finite Sequences

#### Antonio Jiménez-Pastor, Philipp Nuspl, Veronika Pillwein

In: Proceedings of the 2021 on International Symposium on Symbolic and Algebraic Computation, Frédéric Chyzak, George Labahn (ed.), ISSAC '21 , pp. 217-224. 2021. Association for Computing Machinery, New York, NY, USA, ISBN 9781450383820. [doi]@

author = {Antonio Jiménez-Pastor and Philipp Nuspl and Veronika Pillwein},

title = {{On C2-Finite Sequences}},

booktitle = {{Proceedings of the 2021 on International Symposium on Symbolic and Algebraic Computation}},

language = {english},

abstract = {Holonomic sequences are widely studied as many objects interesting to mathematiciansand computer scientists are in this class. In the univariate case, these are the sequencessatisfying linear recurrences with polynomial coefficients and also referred to asD-finite sequences. A subclass are C-finite sequences satisfying a linear recurrencewith constant coefficients.We investigate the set of sequences which satisfy linearrecurrence equations with coefficients that are C-finite sequences. These sequencesare a natural generalization of holonomic sequences. In this paper, we show that C2-finitesequences form a difference ring and provide methods to compute in this ring.},

series = {ISSAC '21},

pages = {217--224},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

isbn_issn = {ISBN 9781450383820},

year = {2021},

editor = {Frédéric Chyzak and George Labahn},

refereed = {yes},

keywords = {holonomic sequences, algorithms, closure properties, difference equations},

length = {8},

url = {https://doi.org/10.1145/3452143.3465529}

}

**inproceedings**{RISC6348,author = {Antonio Jiménez-Pastor and Philipp Nuspl and Veronika Pillwein},

title = {{On C2-Finite Sequences}},

booktitle = {{Proceedings of the 2021 on International Symposium on Symbolic and Algebraic Computation}},

language = {english},

abstract = {Holonomic sequences are widely studied as many objects interesting to mathematiciansand computer scientists are in this class. In the univariate case, these are the sequencessatisfying linear recurrences with polynomial coefficients and also referred to asD-finite sequences. A subclass are C-finite sequences satisfying a linear recurrencewith constant coefficients.We investigate the set of sequences which satisfy linearrecurrence equations with coefficients that are C-finite sequences. These sequencesare a natural generalization of holonomic sequences. In this paper, we show that C2-finitesequences form a difference ring and provide methods to compute in this ring.},

series = {ISSAC '21},

pages = {217--224},

publisher = {Association for Computing Machinery},

address = {New York, NY, USA},

isbn_issn = {ISBN 9781450383820},

year = {2021},

editor = {Frédéric Chyzak and George Labahn},

refereed = {yes},

keywords = {holonomic sequences, algorithms, closure properties, difference equations},

length = {8},

url = {https://doi.org/10.1145/3452143.3465529}

}

[Legersky]

### On the maximal number of real embeddings of minimally rigid graphs in R2, R3 and S2

#### E. Bartzos, I.Z. Emiris, J. Legerský, E. Tsigaridas

Journal of Symbolic Computation 102, pp. 189-208. 2021. ISSN 0747-7171. [doi]@

author = {E. Bartzos and I.Z. Emiris and J. Legerský and E. Tsigaridas},

title = {{On the maximal number of real embeddings of minimally rigid graphs in R2, R3 and S2}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {102},

pages = {189--208},

isbn_issn = {ISSN 0747-7171},

year = {2021},

refereed = {yes},

length = {20},

url = {https://doi.org/10.1016/j.jsc.2019.10.015}

}

**article**{RISC5992,author = {E. Bartzos and I.Z. Emiris and J. Legerský and E. Tsigaridas},

title = {{On the maximal number of real embeddings of minimally rigid graphs in R2, R3 and S2}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {102},

pages = {189--208},

isbn_issn = {ISSN 0747-7171},

year = {2021},

refereed = {yes},

length = {20},

url = {https://doi.org/10.1016/j.jsc.2019.10.015}

}

[Maletzky]

### A generic and executable formalization of signature-based Gröbner basis algorithms

#### Alexander Maletzky

J. Symb. Comput. 106, pp. 23-47. 2021. Elsevier, ISSN 0747-7171. arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001. [url]@

author = {Alexander Maletzky},

title = {{A generic and executable formalization of signature-based Gröbner basis algorithms}},

language = {english},

journal = {J. Symb. Comput.},

volume = {106},

pages = {23--47},

publisher = {Elsevier},

isbn_issn = {ISSN 0747-7171},

year = {2021},

note = {arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001},

refereed = {yes},

length = {25},

url = {https://arxiv.org/abs/2012.02239}

}

**article**{RISC6225,author = {Alexander Maletzky},

title = {{A generic and executable formalization of signature-based Gröbner basis algorithms}},

language = {english},

journal = {J. Symb. Comput.},

volume = {106},

pages = {23--47},

publisher = {Elsevier},

isbn_issn = {ISSN 0747-7171},

year = {2021},

note = {arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001},

refereed = {yes},

length = {25},

url = {https://arxiv.org/abs/2012.02239}

}

[Pau]

### Proximity-Based Unification and Matching for Full Fuzzy Signatures

#### Temur Kutsia, Cleo Pau

Technical report no. 21-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]@

author = {Temur Kutsia and Cleo Pau},

title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},

language = {english},

abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},

number = {21-08},

year = {2021},

month = {April},

keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},

length = {15},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

**techreport**{RISC6296,author = {Temur Kutsia and Cleo Pau},

title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},

language = {english},

abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},

number = {21-08},

year = {2021},

month = {April},

keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},

length = {15},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

[Pau]

### Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures

#### Temur Kutsia, Cleo Pau

Technical report no. 21-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]@

author = {Temur Kutsia and Cleo Pau},

title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},

language = {english},

abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},

number = {21-09},

year = {2021},

month = {April},

keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},

length = {15},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

**techreport**{RISC6297,author = {Temur Kutsia and Cleo Pau},

title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},

language = {english},

abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},

number = {21-09},

year = {2021},

month = {April},

keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},

length = {15},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

[Paule]

### An Invitation to Analytic Combinatorics

#### Peter Paule (ed.), Stephen Melczer

Texts and Monographs in Symbolic Computation 1st edition, 2021. Springer, 978-3-030-67080-1.@

author = {Peter Paule (ed.) and Stephen Melczer},

title = {{An Invitation to Analytic Combinatorics}},

language = {english},

series = {Texts and Monographs in Symbolic Computation},

publisher = {Springer},

isbn_issn = {978-3-030-67080-1},

year = {2021},

edition = {1st},

translation = {0},

length = {405}

}

**book**{RISC6277,author = {Peter Paule (ed.) and Stephen Melczer},

title = {{An Invitation to Analytic Combinatorics}},

language = {english},

series = {Texts and Monographs in Symbolic Computation},

publisher = {Springer},

isbn_issn = {978-3-030-67080-1},

year = {2021},

edition = {1st},

translation = {0},

length = {405}

}

[Reichl]

### Semantic Evaluation versus SMT Solving in the RISCAL Model Checker

#### Wolfgang Schreiner, Franz-Xaver Reichl

Technical report no. 21-11 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). June 2021. Licensed under CC BY 4.0 International. [doi] [pdf]@

author = {Wolfgang Schreiner and Franz-Xaver Reichl},

title = {{Semantic Evaluation versus SMT Solving in the RISCAL Model Checker}},

language = {english},

abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion oftheir fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room forimprovements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},

number = {21-11},

year = {2021},

month = {June},

keywords = {model checking, satisfiability solving, formal specification, formal verficiation},

sponsor = {JKU Linz Institute of Technology (LIT) Project LOGTECHEDU, Aktion Österreich- Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255.},

length = {30},

license = {CC BY 4.0 International},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

**techreport**{RISC6328,author = {Wolfgang Schreiner and Franz-Xaver Reichl},

title = {{Semantic Evaluation versus SMT Solving in the RISCAL Model Checker}},

language = {english},

abstract = {In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original built-in approach of “semantic evaluation” (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later implemented approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to formulas in the SMT-LIB logic QF_UFBV, respectively to quantified SMT-LIB bitvector formulas). After a short presentation of the two approaches and a discussion oftheir fundamental pros and cons, we quantitatively evaluate them, both by a set of artificial benchmarks and by a set of benchmarks taken from real-life applications of RISCAL; for this, we apply the state-of-the-art SMT solvers Boolector, CVC4, Yices, and Z3. Our benchmarks demonstrate that (while SMT solving generally vastly outperforms semantic evaluation), the various SMT solvers exhibit great performance differences. More important, our investigations also identify some classes of formulas where semantic evaluation is able to compete with (or even outperform) satisfiability solving, outlining some room forimprovements in the translation of RISCAL formulas to SMT-LIB formulas as well as in the current SMT technology.},

number = {21-11},

year = {2021},

month = {June},

keywords = {model checking, satisfiability solving, formal specification, formal verficiation},

sponsor = {JKU Linz Institute of Technology (LIT) Project LOGTECHEDU, Aktion Österreich- Slowakei Project 2019-10-15-003, Austrian Science Fund (FWF) grant W1255.},

length = {30},

license = {CC BY 4.0 International},

type = {RISC Report Series},

institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},

address = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

[Schneider]

### The Absent-Minded Passengers Problem: A Motivating Challenge Solved by Computer Algebra

#### C. Schneider

Mathematics in Computer Science , appeared electronically, pp. ?-?. 2021. ISSN 1661-8289. arXiv:2003.01921 [math.CO]. [doi]@

author = {C. Schneider},

title = {{The Absent-Minded Passengers Problem: A Motivating Challenge Solved by Computer Algebra}},

language = {english},

journal = {Mathematics in Computer Science , appeared electronically},

pages = {?--?},

isbn_issn = {ISSN 1661-8289},

year = {2021},

note = {arXiv:2003.01921 [math.CO]},

refereed = {yes},

length = {12},

url = {https://doi.org/10.1007/s11786-020-00494-w}

}

**article**{RISC6127,author = {C. Schneider},

title = {{The Absent-Minded Passengers Problem: A Motivating Challenge Solved by Computer Algebra}},

language = {english},

journal = {Mathematics in Computer Science , appeared electronically},

pages = {?--?},

isbn_issn = {ISSN 1661-8289},

year = {2021},

note = {arXiv:2003.01921 [math.CO]},

refereed = {yes},

length = {12},

url = {https://doi.org/10.1007/s11786-020-00494-w}

}

[Schneider]

### Three loop heavy quark form factors and their asymptotic behavior

#### J. Ablinger, J. Blümlein, P. Marquard, N. Rana, C. Schneider

In: Proc.of 23rd DAE-BRNS High Energy Physics Symposium 2018, Behera, P.K., Bhatnagar, V., Shukla, P., Sinha, R. (ed.), Springer Proceedings in Physics 261, pp. 91-100. 2021. Springer, ISBN 978-981-33-4407-5. arXiv:1906.05829 [hep-ph], https://doi.org/10.1007/978-981-33-4408-2_14. [url]@

author = {J. Ablinger and J. Blümlein and P. Marquard and N. Rana and C. Schneider},

title = {{Three loop heavy quark form factors and their asymptotic behavior}},

booktitle = {{Proc.of 23rd DAE-BRNS High Energy Physics Symposium 2018}},

language = {english},

series = {Springer Proceedings in Physics},

volume = {261},

pages = {91--100},

publisher = {Springer},

isbn_issn = {ISBN 978-981-33-4407-5},

year = {2021},

note = {arXiv:1906.05829 [hep-ph], https://doi.org/10.1007/978-981-33-4408-2_14},

editor = {Behera and P.K. and Bhatnagar and V. and Shukla and P. and Sinha and R.},

refereed = {yes},

length = {10},

url = {https://arxiv.org/abs/1906.05829}

}

**inproceedings**{RISC6024,author = {J. Ablinger and J. Blümlein and P. Marquard and N. Rana and C. Schneider},

title = {{Three loop heavy quark form factors and their asymptotic behavior}},

booktitle = {{Proc.of 23rd DAE-BRNS High Energy Physics Symposium 2018}},

language = {english},

series = {Springer Proceedings in Physics},

volume = {261},

pages = {91--100},

publisher = {Springer},

isbn_issn = {ISBN 978-981-33-4407-5},

year = {2021},

note = {arXiv:1906.05829 [hep-ph], https://doi.org/10.1007/978-981-33-4408-2_14},

editor = {Behera and P.K. and Bhatnagar and V. and Shukla and P. and Sinha and R.},

refereed = {yes},

length = {10},

url = {https://arxiv.org/abs/1906.05829}

}

[Schneider]

### A case study for ζ(4)

#### Carsten Schneider, Wadim Zudilin

In: Proceedings of the conference 'Transient Transcendence in Transylvania', Alin Bostan and Kilian Raschel (ed.), Proceedings in Mathematics & Statistics , pp. ?-?. 2021. Springer, arXiv:2004.08158 [math.NT]. [url]@

author = {Carsten Schneider and Wadim Zudilin},

title = {{A case study for ζ(4)}},

booktitle = {{Proceedings of the conference 'Transient Transcendence in Transylvania'}},

language = {english},

series = {Proceedings in Mathematics & Statistics},

pages = {?--?},

publisher = {Springer},

isbn_issn = {?},

year = {2021},

note = {arXiv:2004.08158 [math.NT]},

editor = {Alin Bostan and Kilian Raschel},

refereed = {no},

length = {0},

url = {https://arxiv.org/abs/2004.08158}

}

**incollection**{RISC6210,author = {Carsten Schneider and Wadim Zudilin},

title = {{A case study for ζ(4)}},

booktitle = {{Proceedings of the conference 'Transient Transcendence in Transylvania'}},

language = {english},

series = {Proceedings in Mathematics & Statistics},

pages = {?--?},

publisher = {Springer},

isbn_issn = {?},

year = {2021},

note = {arXiv:2004.08158 [math.NT]},

editor = {Alin Bostan and Kilian Raschel},

refereed = {no},

length = {0},

url = {https://arxiv.org/abs/2004.08158}

}

[Schneider]

### On Rational and Hypergeometric Solutions of Linear Ordinary Difference Equations in ΠΣ∗-field extensions

#### Sergei A. Abramov, Manuel Bronstein, Marko Petkovšek, Carsten Schneider

J. Symb. Comput. 107, pp. 23-66. 2021. ISSN 0747-7171. arXiv:2005.04944 [cs.SC]. [doi]@

author = {Sergei A. Abramov and Manuel Bronstein and Marko Petkovšek and Carsten Schneider},

title = {{On Rational and Hypergeometric Solutions of Linear Ordinary Difference Equations in ΠΣ∗-field extensions}},

language = {english},

journal = {J. Symb. Comput.},

volume = {107},

pages = {23--66},

isbn_issn = {ISSN 0747-7171},

year = {2021},

note = {arXiv:2005.04944 [cs.SC]},

refereed = {yes},

length = {44},

url = {https://doi.org/10.1016/j.jsc.2021.01.002}

}

**article**{RISC6224,author = {Sergei A. Abramov and Manuel Bronstein and Marko Petkovšek and Carsten Schneider},

title = {{On Rational and Hypergeometric Solutions of Linear Ordinary Difference Equations in ΠΣ∗-field extensions}},

language = {english},

journal = {J. Symb. Comput.},

volume = {107},

pages = {23--66},

isbn_issn = {ISSN 0747-7171},

year = {2021},

note = {arXiv:2005.04944 [cs.SC]},

refereed = {yes},

length = {44},

url = {https://doi.org/10.1016/j.jsc.2021.01.002}

}

[Schneider]

### The Polarized Transition Matrix Element $A_{g, q}(N)$ of the Variable Flavor Number Scheme at $O(alpha_s^3)$

#### A. Behring, J. Blümlein, A. De Freitas, A. von Manteuffel, K. Schönwald, and C. Schneider

Nuclear Physics B 964, pp. 115331-115356. 2021. ISSN 0550-3213. arXiv:2101.05733 [hep-ph]. [doi]@

author = {A. Behring and J. Blümlein and A. De Freitas and A. von Manteuffel and K. Schönwald and and C. Schneider},

title = {{The Polarized Transition Matrix Element $A_{g,q}(N)$ of the Variable Flavor Number Scheme at $O(alpha_s^3)$}},

language = {english},

journal = {Nuclear Physics B},

volume = {964},

pages = {115331--115356},

isbn_issn = {ISSN 0550-3213},

year = {2021},

note = {arXiv:2101.05733 [hep-ph]},

refereed = {yes},

length = {26},

url = {https://doi.org/10.1016/j.nuclphysb.2021.115331}

}

**article**{RISC6278,author = {A. Behring and J. Blümlein and A. De Freitas and A. von Manteuffel and K. Schönwald and and C. Schneider},

title = {{The Polarized Transition Matrix Element $A_{g,q}(N)$ of the Variable Flavor Number Scheme at $O(alpha_s^3)$}},

language = {english},

journal = {Nuclear Physics B},

volume = {964},

pages = {115331--115356},

isbn_issn = {ISSN 0550-3213},

year = {2021},

note = {arXiv:2101.05733 [hep-ph]},

refereed = {yes},

length = {26},

url = {https://doi.org/10.1016/j.nuclphysb.2021.115331}

}