RISC PhD Fellowships 2017

Project Lead

Project Duration

01/01/2017 - 31/12/2017

Publications

2022

[Dundua]

Unranked Nominal Unification

Besik Dundua, Temur Kutsia, Mikheil Rukhaia

In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Proceedings of 13th International Tbilisi Symposium on Logic, Language, and Computation, Lecture Notes in Computer Science 13206, pp. 279-296. 2022. Springer, ISBN 978-3-030-98478-6. [doi] [pdf]
[bib]
@inproceedings{RISC6498,
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {279--296},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {17},
conferencename = {13th International Tbilisi Symposium on Logic, Language, and Computation},
url = {https://doi.org/10.1007/978-3-030-98479-3_14}
}
[Falkensteiner]

On Formal Power Series Solutions of Algebraic Ordinary Differential Equations

S. Falkensteiner, Yi Zhang, N. Thieu Vo

Mediterranean Journal of Mathematics 19(74), pp. 1-16. March 2022. ISSN 1660-5446. [doi]
[bib]
@article{RISC6490,
author = {S. Falkensteiner and Yi Zhang and N. Thieu Vo},
title = {{On Formal Power Series Solutions of Algebraic Ordinary Differential Equations}},
language = {english},
journal = {Mediterranean Journal of Mathematics},
volume = {19},
number = {74},
pages = {1--16},
isbn_issn = {ISSN 1660-5446},
year = {2022},
month = {March},
refereed = {yes},
keywords = {Formal power series, algebraic differential equation.},
length = {16},
url = {https://doi.org/10.1007/s00009-022-01984-w}
}
[Grasegger]

Flexible placements of graphs with rotational symmetry

Sean Dewar, Georg Grasegger, Jan Legerský

In: 2nd IMA Conference on Mathematics of Robotics, W. Holderbaum, J.M. Selig (ed.), Springer Proceedings in Advanced Robotics 21, pp. 89-97. 2022. 978-3-030-91351-9. [doi]
[bib]
@inproceedings{RISC6387,
author = {Sean Dewar and Georg Grasegger and Jan Legerský},
title = {{Flexible placements of graphs with rotational symmetry}},
booktitle = {{2nd IMA Conference on Mathematics of Robotics}},
language = {english},
series = {Springer Proceedings in Advanced Robotics},
volume = {21},
pages = {89--97},
isbn_issn = {978-3-030-91351-9},
year = {2022},
editor = {W. Holderbaum and J.M. Selig},
refereed = {yes},
length = {9},
url = {https://doi.org/10.1007/978-3-030-91352-6_9}
}
[Grasegger]

Zero-Sum Cycles in Flexible Non-triangular Polyhedra

Matteo Gallet, Georg Grasegger, Jan Legerský, Josef Schicho

In: 2nd IMA Conference on Mathematics of Robotics, W. Holderbaum, J.M. Selig (ed.), Springer Proceedings in Advanced Robotics 21, pp. 137-143. 2022. 978-3-030-91351-9. [doi]
[bib]
@inproceedings{RISC6388,
author = {Matteo Gallet and Georg Grasegger and Jan Legerský and Josef Schicho},
title = {{Zero-Sum Cycles in Flexible Non-triangular Polyhedra}},
booktitle = {{2nd IMA Conference on Mathematics of Robotics}},
language = {english},
series = {Springer Proceedings in Advanced Robotics},
volume = {21},
pages = {137--143},
isbn_issn = {978-3-030-91351-9},
year = {2022},
editor = {W. Holderbaum and J.M. Selig},
refereed = {yes},
length = {7},
url = {https://doi.org/10.1007/978-3-030-91352-6_14}
}
[Kutsia]

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz

Fundamenta Informaticae 185(3), pp. 247-283. 2022. IOS Press, ISSN 1875-8681. [url]
[bib]
@article{RISC6506,
author = {Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz},
title = {{Nominal Unification and Matching of Higher Order Expressions with Recursive Let}},
language = {english},
journal = {Fundamenta Informaticae},
volume = {185},
number = {3},
pages = {247--283},
publisher = {IOS Press},
isbn_issn = {ISSN 1875-8681},
year = {2022},
refereed = {yes},
length = {37},
url = {https://arxiv.org/abs/2102.08146v4}
}
[Mitteramskogler]

The algebro-geometric method: Solving algebraic differential equations by parametrizations

S. Falkensteiner, J.J. Mitteramskogler, R. Sendra, F. Winkler

Bulletin of the American Mathematical Society, pp. 1-41. 2022. ISSN 0273-0979.
[bib]
@article{RISC6507,
author = {S. Falkensteiner and J.J. Mitteramskogler and R. Sendra and F. Winkler},
title = {{The algebro-geometric method: Solving algebraic differential equations by parametrizations}},
language = {english},
journal = {Bulletin of the American Mathematical Society},
pages = {1--41},
isbn_issn = {ISSN 0273-0979},
year = {2022},
refereed = {yes},
length = {41}
}
[Nuspl]

Simple $C^2$-finite Sequences: a Computable Generalization of $C$-finite Sequences

P. Nuspl, V. Pillwein

Technical report no. 22-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). February 2022. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6479,
author = {P. Nuspl and V. Pillwein},
title = {{Simple $C^2$-finite Sequences: a Computable Generalization of $C$-finite Sequences}},
language = {english},
abstract = {The class of $C^2$-finite sequences is a natural generalization of holonomic sequences and consists of sequences satisfying a linear recurrence with C-finite coefficients, i.e., coefficients satisfying a linear recurrence with constant coefficients themselves. Recently, we investigated computational properties of $C^2$-finite sequences: we showed that these sequences form a difference ring and provided methods to compute in this ring.From an algorithmic point of view, some of these results were not as far reaching as we hoped for. In this paper, we define the class of simple $C^2$-finite sequences and show that it satisfies the same computational properties, but does not share the same technical issues. In particular, we are able to derive bounds for the asymptotic behavior, can compute closure properties more efficiently, and have a characterization via the generating function.},
number = {22-02},
year = {2022},
month = {February},
keywords = {difference equations, holonomic sequences, closure properties, generating functions, algorithms},
length = {16},
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)}
}
[Pau]

Matching and Generalization Modulo Proximity and Tolerance Relations

Temur Kutsia, Cleo Pau

In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Lecture Notes in Computer Science 13206, pp. 323-342. 2022. Springer, ISBN 978-3-030-98478-6. [doi] [pdf]
[bib]
@inproceedings{RISC6491,
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance Relations}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {323--342},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-030-98479-3_16}
}
[Pau]

A framework for approximate generalization in quantitative theories

Temur Kutsia, Cleo Pau

Technical report no. 22-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). May 2022. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6505,
author = {Temur Kutsia and Cleo Pau},
title = {{A framework for approximate generalization in quantitative theories}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into "proximal'' up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.},
number = {22-04},
year = {2022},
month = {May},
keywords = {Generalization, anti-unification, quantiative theories, fuzzy proximity relations},
length = {22},
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)}
}
[Schicho]

And Yet it Moves - Paradoxically Moving Linkages in Kinematics

J. Schicho

Bulletin AMS 59, pp. 59-95. 2022. ISSN 0273-0979. [doi]
[bib]
@article{RISC6474,
author = {J. Schicho},
title = {{And Yet it Moves -- Paradoxically Moving Linkages in Kinematics}},
language = {english},
journal = {Bulletin AMS},
volume = {59},
pages = {59--95},
isbn_issn = {ISSN 0273-0979},
year = {2022},
refereed = {yes},
length = {37},
url = {https://doi.org/10.1090/bull/1721}
}
[Schneider]

The three-loop polarized singlet anomalous dimensions from off-shell operator matrix elements

J. Blümlein, P. Marquard, C. Schneider, K. Schönwald

Journal of High Energy Physics 2022(193), pp. 0-32. 2022. ISSN 1029-8479 . arXiv:2111.12401 [hep-ph]. [doi]
[bib]
@article{RISC6435,
author = {J. Blümlein and P. Marquard and C. Schneider and K. Schönwald},
title = {{The three-loop polarized singlet anomalous dimensions from off-shell operator matrix elements}},
language = {english},
abstract = {We calculate the polarized three--loop singlet anomalous dimensions and splitting functions in QCD in the M--scheme by using the traditional method of space--like off--shell massless operator matrix elements. This is a gauge--dependent framework. Here one obtains the anomalous dimensions without referring to gravitational currents. We also calculate the non--singlet splitting function $Delta P_{rm qq}^{(2), rm s, NS}$ and compare our results to the literature. },
journal = {Journal of High Energy Physics},
volume = {2022},
number = {193},
pages = {0--32},
isbn_issn = {ISSN 1029-8479 },
year = {2022},
note = {arXiv:2111.12401 [hep-ph]},
refereed = {yes},
keywords = {particle physics, solving recurrences, large moment method, harmonic sums},
length = {33},
url = {https://doi.org/10.1007/JHEP01(2022)193}
}
[Schneider]

The SAGEX Review on Scattering Amplitudes, Chapter 4: Multi-loop Feynman Integrals

J. Blümlein, C. Schneider

Technical report no. 22-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). March 2022. arXiv:2203.13015 [hep-th]. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6495,
author = {J. Blümlein and C. Schneider},
title = {{The SAGEX Review on Scattering Amplitudes, Chapter 4: Multi-loop Feynman Integrals}},
language = {english},
abstract = {The analytic integration and simplification of multi-loop Feynman integrals to special functions and constants plays an important role to perform higher order perturbative calculations in the Standard Model of elementary particles. In this survey article the most recent and relevant computer algebra and special function algorithms are presented that are currently used or that may play an important role to perform such challenging precision calculations in the future. They are discussed in the context of analytic zero, single and double scale calculations in the Quantum Field Theories of the Standard Model and effective field theories, also with classical applications. These calculations play a central role in the analysis of precision measurements at present and future colliders to obtain ultimate information for fundamental physics.},
number = {22-03},
year = {2022},
month = {March},
note = {arXiv:2203.13015 [hep-th]},
keywords = {Feynman integrals, computer algebra, special functions, linear differential equations, linear difference integrals},
length = {40},
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 SAGEX Review on Scattering Amplitudes

G. Travaglini, A. Brandhuber, P. Dorey, T. McLoughlin, S. Abreu, Z. Bern, N. E. J. Bjerrum-Bohr, J. Bluemlein, R. Britto, J. J. M. Carrasco, D. Chicherin, M. Chiodaroli, P. H. Damgaard, V. Del Duca, L. J. Dixon, D. Dorigoni, C. Duhr, Y. Geyer, M. B. Green, E. Herrmann, P. Heslop, H. Johansson, G. P. Korchemsky, D. A. Kosower, L. Mason, R. Monteiro, D. O'Connell, G. Papathanasiou, L. Plante, J. Plefka, A. Puhm, A.-M. Raclariu, R. Roiban, C. Schneider, J. Trnka, P. Vanhove, C. Wen, C. D. White

arxiv.2203.13011 [hep-th]. Technical report, 2022. [url]
[bib]
@techreport{RISC6496,
author = {G. Travaglini and A. Brandhuber and P. Dorey and T. McLoughlin and S. Abreu and Z. Bern and N. E. J. Bjerrum-Bohr and J. Bluemlein and R. Britto and J. J. M. Carrasco and D. Chicherin and M. Chiodaroli and P. H. Damgaard and V. Del Duca and L. J. Dixon and D. Dorigoni and C. Duhr and Y. Geyer and M. B. Green and E. Herrmann and P. Heslop and H. Johansson and G. P. Korchemsky and D. A. Kosower and L. Mason and R. Monteiro and D. O'Connell and G. Papathanasiou and L. Plante and J. Plefka and A. Puhm and A.-M. Raclariu and R. Roiban and C. Schneider and J. Trnka and P. Vanhove and C. Wen and C. D. White},
title = {{The SAGEX Review on Scattering Amplitudes}},
language = {english},
year = {2022},
institution = {arxiv.2203.13011 [hep-th]},
keywords = {High Energy Physics - Theory (hep-th), General Relativity and Quantum Cosmology (gr-qc), High Energy Physics - Experiment (hep-ex), High Energy Physics - Phenomenology (hep-ph), FOS: Physical sciences},
length = {15},
url = {https://arxiv.org/abs/2203.13011}
}
[Schneider]

The Two-Loop Massless Off-Shell QCD Operator Matrix Elements to Finite Terms

J. Blümlein, P. Marquard, C. Schneider, K. Schönwald

To appear in Nuclear Physics B(22-01), pp. ?-?. February 2022. ISSN 0550-3213. arXiv:2202.03216 [hep-ph]. [doi]
[bib]
@article{RISC6497,
author = {J. Blümlein and P. Marquard and C. Schneider and K. Schönwald},
title = {{The Two-Loop Massless Off-Shell QCD Operator Matrix Elements to Finite Terms}},
language = {english},
abstract = {We calculate the unpolarized and polarized two--loop massless off--shell operator matrix elements in QCD to $O(ep)$ in the dimensional parameter in an automated way. Here we use the method of arbitrary high Mellin moments and difference ring theory, based on integration-by-parts relations. This method also constitutes one way to compute the QCD anomalous dimensions. The presented higher order contributions to these operator matrix elements occur as building blocks in the corresponding higher order calculations upto four--loop order. All contributing quantities can be expressed in terms of harmonic sums in Mellin--$N$ space or by harmonic polylogarithms in $z$--space. We also perform comparisons to the literature. },
journal = {To appear in Nuclear Physics B},
number = {22-01},
pages = {?--?},
isbn_issn = {ISSN 0550-3213},
year = {2022},
month = {February},
note = {arXiv:2202.03216 [hep-ph]},
refereed = {yes},
keywords = {QCD, Operator Matrix Element, 2-loop Feynman diagrams, computer algebra, large moment method},
length = {0},
url = {https://doi.org/10.35011/risc.22-01}
}
[Sendra]

Algebraic and Puiseux series solutions of systems of autonomous algebraic ODEs of dimension one in several variables

J. Cano, S. Falkensteiner, D. Robertz, R. Sendra

Journal of Symbolic Computation 114, pp. 1-17. 2022. ISSN 1095-855X. [doi]
[bib]
@article{RISC6501,
author = {J. Cano and S. Falkensteiner and D. Robertz and R. Sendra},
title = {{Algebraic and Puiseux series solutions of systems of autonomous algebraic ODEs of dimension one in several variables}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {114},
pages = {1--17},
isbn_issn = {ISSN 1095-855X},
year = {2022},
refereed = {yes},
length = {17},
url = {http://doi.org/10.1016/j.jsc.2022.04.012}
}

2021

[Ablinger]

Extensions of the AZ-algorithm and the Package MultiIntegrate

J. Ablinger

In: Anti-Differentiation and the Calculation of Feynman Amplitudes, J. Blümlein, C. Schneider (ed.), Texts & Monographs in Symbolic Computation (A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria) , pp. 35-61. 2021. Springer, ISBN 978-3-030-80218-9. arXiv:2101.11385 [cs.SC]. [doi]
[bib]
@incollection{RISC6408,
author = {J. Ablinger},
title = {{Extensions of the AZ-algorithm and the Package MultiIntegrate}},
booktitle = {{Anti-Differentiation and the Calculation of Feynman Amplitudes}},
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.},
series = {Texts & Monographs in Symbolic Computation (A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria)},
pages = {35--61},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-80218-9},
year = {2021},
note = {arXiv:2101.11385 [cs.SC]},
editor = {J. Blümlein and C. Schneider},
refereed = {yes},
keywords = {multivariate Almkvist-Zeilberger algorithm, hyperexponential integrals, iterated integrals, nested sums},
length = {27},
url = {https://doi.org/10.1007/978-3-030-80219-6_2}
}
[Ablinger]

Extensions of the AZ-algorithm and the Package MultiIntegrate

J. Ablinger

In: Anti-Differentiation and the Calculation of Feynman Amplitudes, J. Blümlein, C. Schneider (ed.), Texts & Monographs in Symbolic Computation (A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria) , pp. 35-61. 2021. Springer, ISBN 978-3-030-80218-9. arXiv:2101.11385 [cs.SC]. [doi]
[bib]
@incollection{RISC6409,
author = {J. Ablinger},
title = {{Extensions of the AZ-algorithm and the Package MultiIntegrate}},
booktitle = {{Anti-Differentiation and the Calculation of Feynman Amplitudes}},
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.},
series = {Texts & Monographs in Symbolic Computation (A Series of the Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria)},
pages = {35--61},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-80218-9},
year = {2021},
note = {arXiv:2101.11385 [cs.SC]},
editor = {J. Blümlein and C. Schneider},
refereed = {yes},
keywords = {multivariate Almkvist-Zeilberger algorithm, hyperexponential integrals, iterated integrals, nested sums},
length = {27},
url = {https://doi.org/10.1007/978-3-030-80219-6_2}
}
[Cerna]

A Special Case of Schematic Syntactic Unification

David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]
[bib]
@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}
}
[Cerna]

Learning Higher-Order Programs without Meta-Interpretive Learning

Stanislav Purgal and David Cerna and Cezary Kalisyk

Technical report no. 21-22 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2021. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6393,
author = {Stanislav Purgal and David Cerna and Cezary Kalisyk},
title = {{Learning Higher-Order Programs without Meta-Interpretive Learning}},
language = {english},
abstract = {Learning complex programs through textit{inductive logic programming} (ILP) remains a formidable challenge. Existing higher-order enabled ILP systems show improved accuracy and learning performance, though remain hampered by the limitations of the underlying learning mechanism. Experimental results show that our extension of the versatile textit{Learning From Failures} paradigm by higher-order definitions significantly improves learning performance without the burdensome human guidance required by existing systems. Furthermore, we provide a theoretical framework capturing the class of higher-order definitions handled by our extension.},
number = {21-22},
year = {2021},
month = {December},
keywords = {Inductive Logic Programming, Higher order definitions},
length = {8},
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)}
}
[Dramnesc]

AlCons: Deductive Synthesis of Sorting Algorithms in Theorema

I. Dramnesc, T. Jebelean

In: Theoretical Aspects of Computing - ICTAC 2021, A. Cerone, P. Csaba Ölveczky (ed.), Proceedings of 18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan, LNCS 12819, pp. 314-333. September 2021. Springer, 978-3-030-85315-0. [pdf]
[bib]
@inproceedings{RISC6478,
author = {I. Dramnesc and T. Jebelean},
title = {{AlCons: Deductive Synthesis of Sorting Algorithms in Theorema}},
booktitle = {{Theoretical Aspects of Computing - ICTAC 2021}},
language = {english},
abstract = {We describe the principles and the implementation of AlCons (em Algorithm Constructor), a system for the automatic proof--based synthesis of sorting algorithms on lists and on binary trees, in the frame of the Theorema system. The core of the system is a dedicated prover based on specific inference rules and strategies for constructive proofs over the domains of lists and of binary trees, aimed at the automatic synthesis of sorting algorithms and their auxiliary functions from logical specifications. The specific distinctive feature of our approach is the use of multisets for expressing the fact that two lists (trees) have the same elements. This allows a more natural expression of the properties related to sorting, compared to the classical approach using the permutation relation (a list is a permutation of another). Moreover, the use of multisets leads to special inference rules and strategies which make the proofs more efficient, as for instance: expand/compress multiset terms and solve meta-variables using multiset equalities. Additionally we use a Noetherian induction strategy based on the relation induced by the strict inclusion of multisets, which facilitates the synthesis of arbitrary recursion structures, without having to indicate the recursion schemes in advance. The necessary auxiliary algorithms (like, e.g., for insertion and merging) are generated by the same principles from the synthesis conjectures that are automatically produced during the main proof, using a ``cascading" method, which in fact contributes to the automation of theory exploration. The prover is implemented in the frame of the Theorema system and works in natural style, while the generated algorithms can be immediately tested in the same system.},
series = {LNCS},
volume = {12819},
pages = {314--333},
publisher = {Springer},
isbn_issn = {978-3-030-85315-0},
year = {2021},
month = {September },
editor = {A. Cerone and P. Csaba Ölveczky},
refereed = {yes},
length = {20},
conferencename = {18th International Colloquium on Theoretical Aspects of Computing - ICTAC, Nur-Sultan, Kazakhstan}
}

Loading…