Publications

2019

[Ablinger]

Discovering and Proving Infinite Pochhammer Sum Identities

J. Ablinger

submitted, pp. 1-21. 2019. arXiv:1902.11001 [math.CO]. [url]

[bib]

@article{RISC5896,
author = {J. Ablinger},
title = {{Discovering and Proving Infinite Pochhammer Sum Identities}},
language = {english},
journal = {submitted},
pages = {1--21},
isbn_issn = {?},
year = {2019},
note = {arXiv:1902.11001 [math.CO]},
refereed = {yes},
length = {21},
url = {http://arxiv.org/abs/1902.11001}
}

[Berkovich]

Polynomial Identities Implying Capparelli's Partition Theorems

Ali Kemal Uncu, Alexander Berkovich

Accepted - Journal of Number Theory, pp. -. 2019. N/A. [url]

[bib]

@article{RISC5790,
author = {Ali Kemal Uncu and Alexander Berkovich},
title = {{Polynomial Identities Implying Capparelli's Partition Theorems }},
language = {english},
journal = {Accepted - Journal of Number Theory},
pages = {--},
isbn_issn = {N/A},
year = {2019},
refereed = {yes},
length = {21},
url = {https://arxiv.org/pdf/1807.10974.pdf}
}

[Berkovich]

Refined q-Trinomial Coefficients and Two Infinite Hierarchies of q-Series Identities

Ali Kemal Uncu, Alexander Berkovich

ArXiv e-prints (accepted), pp. 1-10. 2019. N/A. [url]

[bib]

@article{RISC5801,
author = {Ali Kemal Uncu and Alexander Berkovich},
title = {{Refined q-Trinomial Coefficients and Two Infinite Hierarchies of q-Series Identities }},
language = {english},
abstract = {We will prove an identity involving refined q-trinomial coefficients. We then extend this identity to two infinite families of doubly bounded polynomial identities using transformation properties of the refined q-trinomials in an iterative fashion in the spirit of Bailey chains. One of these two hierarchies contains an identity which is equivalent to Capparelli's first Partition Theorem. },
journal = {ArXiv e-prints (accepted)},
pages = {1--10},
isbn_issn = {N/A},
year = {2019},
refereed = {yes},
length = {10},
url = {https://arxiv.org/abs/1810.12048}
}

[Capco]

Sum of Squares over Rationals

J. Capco, C. Scheiderer

RISC. Technical report, 2019. [url] [pdf]

[bib]

@techreport{RISC5884,
author = {J. Capco and C. Scheiderer},
title = {{Sum of Squares over Rationals}},
language = {english},
abstract = {Recently it has been shown that a multivariate (homogeneous) polynomialwith rational coefficients that can be written as a sum of squares offorms with real coefficients, is not necessarily a sum of squares offorms with rational coefficients. Essentially, only one constructionfor such forms is known, namely taking the $K/\Q$-norm of a sufficientlygeneral form with coefficients in a number field $K$. Whether thisconstruction yields a form with the desired properties depends onGalois-theoretic properties of $K$ that are not yet well understood.We construct new families of examples, and we shed new light on somewell-known open questions.},
year = {2019},
institution = {RISC},
length = {0},
url = {https://www3.risc.jku.at/~jcapco/public_files/ss18/sosq.html}
}

[Cerna]

On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences

David M. Cerna

In: T.B.D, T.B.D (ed.), Proceedings of T.B.D, pp. 1-17. 2019. T.B.D. [pdf]

[bib]

@inproceedings{RISC5841,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
booktitle = {{T.B.D}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
pages = {1--17},
isbn_issn = {T.B.D},
year = {2019},
editor = {T.B.D},
refereed = {yes},
length = {17},
conferencename = {T.B.D}
}

[Cerna]

A Generic Framework for Higher-Order Generalizations

David M. Cerna, Temur Kutsia

Technical report no. 19-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]

[bib]

@techreport{RISC5883,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
language = {english},
number = {19-01},
year = {2019},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Cerna]

Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire

David M. Cerna

Feburary 2019. [pdf] [xlsx]

[bib]

@techreport{RISC5885,
author = {David M. Cerna},
title = {{Evaluation of the VL Logic (342.208-9) 2018W End of Semester Questionnaire}},
language = {english},
abstract = {In this technical report we cover the choice of layout and intentions behind our end of the semester questionnaire as well as our interpretation of student answers, resulting statistical analysis, and inferences. Our questionnaire is to some extent free-form in that we provide instructions concerning the desired content of the answers but leave the precise formulation of the answer to the student. Our goal, through this approach, was to gain an understanding of how the students viewed there own progress and interest in the course without explicitly guiding them. Towards this end, we chose to have the students draw curves supplemented by short descriptions of important features. We end with a discussion of the benefits and downsides of such a questionnaire as well as what the results entail concerning future iterations of the course. },
year = {2019},
month = {Feburary},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Cerna]

The Castle Game

David M. Cerna

2019. [pdf]

[bib]

@techreport{RISC5886,
author = {David M. Cerna},
title = {{The Castle Game}},
language = {english},
abstract = {A description of a game for teaching certain aspects of first-order logic based on the Drink's Paradox. },
year = {2019},
length = {3},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Cerna]

Manual for AXolotl

David M. Cerna

2019. [pdf] [zip] [jar]

[bib]

@techreport{RISC5887,
author = {David M. Cerna},
title = {{Manual for AXolotl}},
language = {english},
abstract = {In this document we outline how to play our preliminary version of \textbf{AX}olotl. We present a sequence of graphics illustrating the step by step process of playing the game. },
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Cerna]

Higher-Order Pattern Generalization Modulo Equational Theories

David M. Cerna and Temur Kutsia

2019. [pdf]

[bib]

@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {We consider anti-unification for simply typed lambda terms in theories defined by associativity,commutativity, identity (unit element) axioms and their combinations, and develop a sound andcomplete algorithm which takes two lambda terms and computes their equational generalizations inthe form of higher-order patterns. The problem is finitary: the minimal complete set of suchgeneralizations contains finitely many elements. We define the notion of optimal solution andinvestigate special fragments of the problem for which the optimal solution can be computed in linearor polynomial time.},
year = {2019},
length = {25},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Cerna]

AXolotl: A Self-study Tool for First-order Logic

David Cerna

May 2019. [pdf]

[bib]

@techreport{RISC5936,
author = {David Cerna},
title = {{AXolotl: A Self-study Tool for First-order Logic}},
language = {english},
year = {2019},
month = {May},
length = {4},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Hemmecke]

The Generators of all Polynomial Relations among Jacobi Theta Functions

Ralf Hemmecke, Silviu Radu, Liangjie Ye

In: Elliptic Integrals, Elliptic Functions and Modular Forms in Quantum Field Theory, Johannes Blümlein and Carsten Schneider and Peter Paule (ed.), Texts & Monographs in Symbolic Computation 18-09, pp. 259-268. 2019. Springer International Publishing, Cham, 978-3-030-04479-4. Also available as RISC Report 18-09 http://www.risc.jku.at/publications/download/risc_5719/thetarelations.pdf. [url]

[bib]

@incollection{RISC5913,
author = {Ralf Hemmecke and Silviu Radu and Liangjie Ye},
title = {{The Generators of all Polynomial Relations among Jacobi Theta Functions}},
booktitle = {{Elliptic Integrals, Elliptic Functions and Modular Forms in Quantum Field Theory}},
language = {english},
abstract = {In this article, we consider the classical Jacobi theta functions$\theta_i(z)$, $i=1,2,3,4$ and show that the ideal of all polynomialrelations among them with coefficients in$K :=\setQ(\theta_2(0|\tau),\theta_3(0|\tau),\theta_4(0|\tau))$ isgenerated by just two polynomials, that correspond to well knownidentities among Jacobi theta functions.},
series = {Texts & Monographs in Symbolic Computation},
number = {18-09},
pages = {259--268},
publisher = {Springer International Publishing},
address = {Cham},
isbn_issn = {978-3-030-04479-4},
year = {2019},
note = {Also available as RISC Report 18-09 http://www.risc.jku.at/publications/download/risc_5719/thetarelations.pdf},
editor = {Johannes Blümlein and Carsten Schneider and Peter Paule},
refereed = {yes},
length = {9},
url = {https://doi.org/10.1007/978-3-030-04480-0_11}
}

[Jimenez Pastor]

A Computable Extension for Holonomic Functions: DD-Finite Functions

Jiménez-Pastor Antonio, Pillwein Veronika

Journal of Symbolic Computation 94, pp. 90-104. September-October 2019. ISSN 0747-7171. [url]

[bib]

@article{RISC5831,
author = {Jiménez-Pastor Antonio and Pillwein Veronika},
title = {{A Computable Extension for Holonomic Functions: DD-Finite Functions}},
language = {english},
abstract = {Differentiably finite (D-finite) formal power series form a large class of useful functions for which a variety of symbolic algorithms exists. Among these methods are several closure properties that can be carried out automatically. We introduce a natural extension of these functions to a larger class of computable objects for which we prove closure properties. These are again algorithmic. This extension can be iterated constructively preserving the closure properties},
journal = {Journal of Symbolic Computation},
volume = {94},
pages = {90--104},
isbn_issn = {ISSN 0747-7171},
year = {2019},
month = {September-October},
refereed = {yes},
length = {15},
url = {https://doi.org/10.1016/j.jsc.2018.07.002}
}

[Maletzky]

Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL

A. Maletzky

In: Intelligent Computer Mathematics (Proceedings of CICM 2019, Prague, Czech Republic, July 8-12), Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti-Coen (ed.), Proceedings of CICM 2019, Lecture Notes in Computer Science , pp. ?-?. 2019. Springer, to appear. [pdf]

[bib]

@inproceedings{RISC5919,
author = {A. Maletzky},
title = {{Formalization of Dubé's Degree Bounds for Gröbner Bases in Isabelle/HOL}},
booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2019, Prague, Czech Republic, July 8-12)}},
language = {english},
series = {Lecture Notes in Computer Science},
pages = {?--?},
publisher = {Springer},
isbn_issn = {?},
year = {2019},
note = {to appear},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti-Coen},
refereed = {yes},
length = {16},
conferencename = {CICM 2019}
}

[Maletzky]

Gröbner Bases and Macaulay Matrices in Isabelle/HOL

A. Maletzky

RISC, JKU Linz. Technical report, 2019. Submitted to Formal Aspects of Computing. [pdf]

[bib]

@techreport{RISC5929,
author = {A. Maletzky},
title = {{Gröbner Bases and Macaulay Matrices in Isabelle/HOL}},
language = {english},
year = {2019},
note = {Submitted to Formal Aspects of Computing},
institution = {RISC, JKU Linz},
length = {14}
}

[Maletzky]

Theorema-HOL: Classical Higher-Order Logic in Theorema

A. Maletzky

Technical report no. 19-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. June 2019. [pdf]

[bib]

@techreport{RISC5930,
author = {A. Maletzky},
title = {{Theorema-HOL: Classical Higher-Order Logic in Theorema}},
language = {english},
number = {19-03},
year = {2019},
month = {June},
length = {24},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Paule]

A Proof of the Weierstrass Gap Theorem not using the Riemann-Roch Formula

Peter Paule, Silviu Radu

Technical report no. 19-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. May 2019. [pdf]

[bib]

@techreport{RISC5928,
author = {Peter Paule and Silviu Radu},
title = {{A Proof of the Weierstrass Gap Theorem not using the Riemann-Roch Formula}},
language = {english},
number = {19-02},
year = {2019},
month = {May},
length = {47},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Pillwein]

On the positivity of the Gillis–Reznick–Zeilberger rational function

V. Pillwein

Advances in Applied Mathematics 104, pp. 75 - 84. 2019. ISSN 0196-8858. [url]

[bib]

@article{RISC5813,
author = {V. Pillwein},
title = {{On the positivity of the Gillis–Reznick–Zeilberger rational function}},
language = {english},
journal = {Advances in Applied Mathematics},
volume = {104},
pages = {75 -- 84},
isbn_issn = { ISSN 0196-8858},
year = {2019},
refereed = {yes},
keywords = {Positivity, Cylindrical decomposition, Rational function, Symbolic summation},
length = {10},
url = {http://www.sciencedirect.com/science/article/pii/S0196885818301179}
}

[Schicho]

Projective and affine symmetries and equivalences of rational and polynomial surfaces

M. Hauer, B. Jüttler, J. Schicho

J. Comp. Appl. Math. 349, pp. 424-437. 2019. 0377-0427.

[bib]

@article{RISC5875,
author = {M. Hauer and B. Jüttler and J. Schicho},
title = {{Projective and affine symmetries and equivalences of rational and polynomial surfaces}},
language = {english},
journal = {J. Comp. Appl. Math.},
volume = {349},
pages = {424--437},
isbn_issn = {0377-0427},
year = {2019},
refereed = {yes},
length = {14}
}

[Schneider]

Towards a symbolic summation theory for unspecified sequences

P. Paule, C. Schneider

In: Elliptic Integrals, Elliptic Functions and Modular Forms in Quantum Field Theory, J. Blümlein, P. Paule, C. Schneider (ed.), Texts and Monographs in Symbolic Computation , pp. 351-390. 2019. Springer, ISBN 978-3-030-04479-4. arXiv:1809.06578 [cs.SC]. [url]

[bib]

@incollection{RISC5750,
author = {P. Paule and C. Schneider},
title = {{Towards a symbolic summation theory for unspecified sequences}},
booktitle = {{Elliptic Integrals, Elliptic Functions and Modular Forms in Quantum Field Theory}},
language = {english},
series = {Texts and Monographs in Symbolic Computation},
pages = {351--390},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-04479-4},
year = {2019},
note = {arXiv:1809.06578 [cs.SC]},
editor = {J. Blümlein and P. Paule and C. Schneider},
refereed = {yes},
length = {40},
url = {https://arxiv.org/abs/1809.06578}
}