# Computer-assisted Chemical Synthesis design (industrial project

### Project Description

Topics: graph isomorphism problem, search for subgraphs of molecular graphs, mathematical software implementation in LISP.

### Project Lead

### Project Duration

01/01/1986 - 31/12/1988## Publications

### 2019

[Ablinger]

### Discovering and Proving Infinite Pochhammer Sum Identities

#### J. Ablinger

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

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}

}

**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]@

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}

}

**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]@

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}

}

**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]@

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}

}

**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]@

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}

}

**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]@

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}

}

**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]@

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}

}

**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]@

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}

}

**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. [jar] [zip] [pdf]@

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}

}

**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]@

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}

}

**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}

}

[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]@

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}

}

**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}

}

[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]@

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}

}

**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.@

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}

}

**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]@

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}

}

**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}

}

[Schneider]

### Numerical Implementation of Harmonic Polylogarithms to Weight w = 8

#### J. Ablinger, J. Blümlein, M. Round, C. Schneider

To appear in Comput. Phys. Comm., pp. 1-19. 2019. ISSN 0010-4655. arXiv:1809.07084 [hep-ph]. [url]@

author = {J. Ablinger and J. Blümlein and M. Round and C. Schneider},

title = {{Numerical Implementation of Harmonic Polylogarithms to Weight w = 8}},

language = {english},

journal = {To appear in Comput. Phys. Comm.},

pages = {1--19},

isbn_issn = {ISSN 0010-4655},

year = {2019},

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

refereed = {yes},

length = {19},

url = {https://arxiv.org/pdf/1809.07084.pdf}

}

**article**{RISC5751,author = {J. Ablinger and J. Blümlein and M. Round and C. Schneider},

title = {{Numerical Implementation of Harmonic Polylogarithms to Weight w = 8}},

language = {english},

journal = {To appear in Comput. Phys. Comm.},

pages = {1--19},

isbn_issn = {ISSN 0010-4655},

year = {2019},

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

refereed = {yes},

length = {19},

url = {https://arxiv.org/pdf/1809.07084.pdf}

}

[Schneider]

### Automated Solution of First Order Factorizable Systems of Differential Equations in One Variable

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

Nucl. Phys. B 939, pp. 253-291. 2019. ISSN 0550-3213. arXiv:1810.12261 [hep-ph]. [url]@

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

title = {{Automated Solution of First Order Factorizable Systems of Differential Equations in One Variable}},

language = {english},

journal = {Nucl. Phys. B},

volume = {939},

pages = {253--291},

isbn_issn = {ISSN 0550-3213},

year = {2019},

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

refereed = {yes},

length = {39},

url = {https://www.sciencedirect.com/science/article/pii/S055032131830350X?via%3Dihub}

}

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

title = {{Automated Solution of First Order Factorizable Systems of Differential Equations in One Variable}},

language = {english},

journal = {Nucl. Phys. B},

volume = {939},

pages = {253--291},

isbn_issn = {ISSN 0550-3213},

year = {2019},

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

refereed = {yes},

length = {39},

url = {https://www.sciencedirect.com/science/article/pii/S055032131830350X?via%3Dihub}

}

[Schreiner]

### Theorem and Algorithm Checking for Courses on Logic and Formal Methods

#### Wolfgang Schreiner

In: Post-Proceedings ThEdu'18, Pedro Quaresma and Walther Neuper (ed.), Proceedings of 7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018, Electronic Proceedings in Theoretical Computer Science (EPTCS) 290, pp. 56-75. April 1 2019. Open Publishing Association, ISSN 2075-2180. [url] [pdf]@

author = {Wolfgang Schreiner},

title = {{Theorem and Algorithm Checking for Courses on Logic and Formal Methods}},

booktitle = {{Post-Proceedings ThEdu'18}},

language = {english},

abstract = {The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms. A RISCAL specification describes an infinite class of models each of which has finite size; this allows to fully automatically check in such a model the validity of all theorems and the correctness of all algorithms. RISCAL thus enables us to quickly verify/falsify the specific truth of propositions in sample instances of a model class before attempting to prove their general truth in the whole class: the first can be achieved in a fully automatic way while the second typically requires our assistance. RISCAL has been mainly developed for educational purposes. To this end this paper reports on some new enhancements of the tool: the automatic generation of checkable verification conditions from algorithms, the visualization of the execution of procedures and the evaluation of formulas illustrating the computation of their results, and the generation of Web-based student exercises and assignments from RISCAL specifications. Furthermore, we report on our first experience with RISCAL in the teaching of courses on logic and formal methods and on further plans to use this tool to enhance formal education.},

series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},

volume = {290},

pages = {56--75},

publisher = {Open Publishing Association},

isbn_issn = {ISSN 2075-2180},

year = {2019},

month = {April 1},

editor = {Pedro Quaresma and Walther Neuper},

refereed = {yes},

sponsor = {Linz Institute of Technology (LIT), Project LOGTECHEDU “Logic Technology for Computer Science Education” and OEAD WTZ project SK 14/2018 SemTech},

length = {20},

conferencename = {7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018},

url = {http://dx.doi.org/10.4204/EPTCS.290.5}

}

**inproceedings**{RISC5895,author = {Wolfgang Schreiner},

title = {{Theorem and Algorithm Checking for Courses on Logic and Formal Methods}},

booktitle = {{Post-Proceedings ThEdu'18}},

language = {english},

abstract = {The RISC Algorithm Language (RISCAL) is a language for the formal modeling of theories and algorithms. A RISCAL specification describes an infinite class of models each of which has finite size; this allows to fully automatically check in such a model the validity of all theorems and the correctness of all algorithms. RISCAL thus enables us to quickly verify/falsify the specific truth of propositions in sample instances of a model class before attempting to prove their general truth in the whole class: the first can be achieved in a fully automatic way while the second typically requires our assistance. RISCAL has been mainly developed for educational purposes. To this end this paper reports on some new enhancements of the tool: the automatic generation of checkable verification conditions from algorithms, the visualization of the execution of procedures and the evaluation of formulas illustrating the computation of their results, and the generation of Web-based student exercises and assignments from RISCAL specifications. Furthermore, we report on our first experience with RISCAL in the teaching of courses on logic and formal methods and on further plans to use this tool to enhance formal education.},

series = {Electronic Proceedings in Theoretical Computer Science (EPTCS)},

volume = {290},

pages = {56--75},

publisher = {Open Publishing Association},

isbn_issn = {ISSN 2075-2180},

year = {2019},

month = {April 1},

editor = {Pedro Quaresma and Walther Neuper},

refereed = {yes},

sponsor = {Linz Institute of Technology (LIT), Project LOGTECHEDU “Logic Technology for Computer Science Education” and OEAD WTZ project SK 14/2018 SemTech},

length = {20},

conferencename = {7th International Workshop on Theorem proving components for Educational software, Oxford, United Kingdom, 18 July 2018},

url = {http://dx.doi.org/10.4204/EPTCS.290.5}

}

[Schreiner]

### A Categorical Semantics of Relational First-Order Logic

#### Wolfgang Schreiner, Valerie Novitzká, William Steingartner

Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Technical report, March 2019. [pdf]@

author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},

title = {{A Categorical Semantics of Relational First-Order Logic}},

language = {english},

abstract = {We present a categorical formalization of a variant of first-order logic. Unlike other textson this topic, the goal of this paper is to give a very transparent and self-contained accountwithout requiring more background than basic logic and set theory. Our focus is to showhow the semantics of first order formulas can be derived from their usual deduction rules.For understanding the core ideas, it is not necessary to investigate the internal term structureof atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations;in this sense our variant of first-order logic is “relational”. While the derived semanticsis based on categorical principles, it is nevertheless “constructive” in that it describesexplicit computations of the truth values of formulas. We demonstrate this by modeling thecategorical semantics in the RISCAL (RISC Algorithm Language) system which allows usto validate the core propositions by automatically checking them in finite models.},

year = {2019},

month = {March},

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

keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},

sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},

length = {34}

}

**techreport**{RISC5900,author = {Wolfgang Schreiner and Valerie Novitzká and William Steingartner},

title = {{A Categorical Semantics of Relational First-Order Logic}},

language = {english},

abstract = {We present a categorical formalization of a variant of first-order logic. Unlike other textson this topic, the goal of this paper is to give a very transparent and self-contained accountwithout requiring more background than basic logic and set theory. Our focus is to showhow the semantics of first order formulas can be derived from their usual deduction rules.For understanding the core ideas, it is not necessary to investigate the internal term structureof atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations;in this sense our variant of first-order logic is “relational”. While the derived semanticsis based on categorical principles, it is nevertheless “constructive” in that it describesexplicit computations of the truth values of formulas. We demonstrate this by modeling thecategorical semantics in the RISCAL (RISC Algorithm Language) system which allows usto validate the core propositions by automatically checking them in finite models.},

year = {2019},

month = {March},

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

keywords = {first-order logic, formal semantics, category theory, RISC Algorithm Language (RISCAL)},

sponsor = {OEAD WTZ project SK 14/2018 “SemTech — Semantic Technologies for Computer Science Education” and JKU LIT project LOGTECHEDU “Logic Technology for Computer Science Education”},

length = {34}

}

[Smoot]

### A Family of Congruences for Rogers-Ramanujan Subpartitions

#### Nicolas Allen Smoot

Journal of Number Theory 196, pp. 35-60. March 2019. ISSN 0022-314X. [pdf]@

author = {Nicolas Allen Smoot},

title = {{A Family of Congruences for Rogers--Ramanujan Subpartitions}},

language = {english},

abstract = {In 2015 Choi, Kim, and Lovejoy studied a weighted partition function, A1(m), which counted subpartitions with a structure related to the Rogers–Ramanujan identities. They conjectured the existence of an infinite class of congruences for A1(m), modulo powers of 5. We give an explicit form of this conjecture, and prove it for all powers of 5.},

journal = {Journal of Number Theory},

volume = {196},

pages = {35--60},

isbn_issn = {ISSN 0022-314X},

year = {2019},

month = {March},

refereed = {yes},

keywords = {Integer partitions, Partition congruences, Rogers--Ramanujan identities, Ramanujan--Kolberg identities, Modular functions},

sponsor = {FWF: W1214-N15},

length = {26}

}

**article**{RISC5809,author = {Nicolas Allen Smoot},

title = {{A Family of Congruences for Rogers--Ramanujan Subpartitions}},

language = {english},

abstract = {In 2015 Choi, Kim, and Lovejoy studied a weighted partition function, A1(m), which counted subpartitions with a structure related to the Rogers–Ramanujan identities. They conjectured the existence of an infinite class of congruences for A1(m), modulo powers of 5. We give an explicit form of this conjecture, and prove it for all powers of 5.},

journal = {Journal of Number Theory},

volume = {196},

pages = {35--60},

isbn_issn = {ISSN 0022-314X},

year = {2019},

month = {March},

refereed = {yes},

keywords = {Integer partitions, Partition congruences, Rogers--Ramanujan identities, Ramanujan--Kolberg identities, Modular functions},

sponsor = {FWF: W1214-N15},

length = {26}

}

[Smoot]

### A Method of Verifying Partition Congruences by Symbolic Computation

#### Cristian-Silviu Radu, Nicolas Allen Smoot

Journal of Symbolic Computation, pp. -. 2019. ISSN 0747-7171. Submitted.@

author = {Cristian-Silviu Radu and Nicolas Allen Smoot},

title = {{A Method of Verifying Partition Congruences by Symbolic Computation}},

language = {english},

abstract = {Conjectures involving infinite families of restricted partition congruences can be diffcult to verify for a number of individual cases, even with a computer. We demonstrate how the machinery of Radu's algorithm may be modifed and employed to efficiently check a very large number of cases of such conjectures. This allows substantial evidence to becollected for a given conjecture, before a complete proof is attempted.},

journal = {Journal of Symbolic Computation},

pages = {--},

isbn_issn = {ISSN 0747-7171},

year = {2019},

note = {Submitted},

refereed = {yes},

length = {37}

}

**article**{RISC5897,author = {Cristian-Silviu Radu and Nicolas Allen Smoot},

title = {{A Method of Verifying Partition Congruences by Symbolic Computation}},

language = {english},

abstract = {Conjectures involving infinite families of restricted partition congruences can be diffcult to verify for a number of individual cases, even with a computer. We demonstrate how the machinery of Radu's algorithm may be modifed and employed to efficiently check a very large number of cases of such conjectures. This allows substantial evidence to becollected for a given conjecture, before a complete proof is attempted.},

journal = {Journal of Symbolic Computation},

pages = {--},

isbn_issn = {ISSN 0747-7171},

year = {2019},

note = {Submitted},

refereed = {yes},

length = {37}

}