# Symbolic Solutions of Algebraic Differential Equations [ADE-solve]

### Project Lead

### Project Duration

01/05/2018 - 30/04/2021## Members

## Johann Mitteramskogler

## Partners

### The Austrian Science Fund (FWF)

## Publications

### 2019

### 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},

abstract = {In this note we provide further evidence for a conjecture of Gillis, Reznick, and Zeilberger on the positivity of the diagonal coefficients of a multivariate rational function. Kauers had proven this conjecture for up to 6 variables using computer algebra. We present a variation of his approach that allows us to prove positivity of the coefficients up to 17 variables using symbolic computation.},

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

abstract = {In this note we provide further evidence for a conjecture of Gillis, Reznick, and Zeilberger on the positivity of the diagonal coefficients of a multivariate rational function. Kauers had proven this conjecture for up to 6 variables using computer algebra. We present a variation of his approach that allows us to prove positivity of the coefficients up to 17 variables using symbolic computation.},

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}

}

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

}

### 2018

### An Improved Method to Compute the Inverse Mellin Transform of Holonomic Sequences

#### J. Ablinger

In: Proceedings of "Loops and Legs in Quantum Field Theory - LL 2018, J. Blümlein and P. Marquard (ed.), PoS(LL2018) , pp. 1-10. 2018. ISSN 1824-8039. [url]@

author = {J. Ablinger},

title = {{An Improved Method to Compute the Inverse Mellin Transform of Holonomic Sequences}},

booktitle = {{Proceedings of "Loops and Legs in Quantum Field Theory - LL 2018}},

language = {english},

series = {PoS(LL2018)},

pages = {1--10},

isbn_issn = {ISSN 1824-8039},

year = {2018},

editor = {J. Blümlein and P. Marquard},

refereed = {yes},

length = {10},

url = {https://pos.sissa.it/303/063/pdf}

}

**inproceedings**{RISC5789,author = {J. Ablinger},

title = {{An Improved Method to Compute the Inverse Mellin Transform of Holonomic Sequences}},

booktitle = {{Proceedings of "Loops and Legs in Quantum Field Theory - LL 2018}},

language = {english},

series = {PoS(LL2018)},

pages = {1--10},

isbn_issn = {ISSN 1824-8039},

year = {2018},

editor = {J. Blümlein and P. Marquard},

refereed = {yes},

length = {10},

url = {https://pos.sissa.it/303/063/pdf}

}

### Anti-Unification and Natural Language Processing

#### N. Amiridze, T. Kutsia

In: Fifth Workshop on Natural Language and Computer Science, NLCS’18, A. Asudeh, V. de Paiva, L. Moss (ed.), EasyChair preprints 203, pp. 1-12. 2018. [url] [pdf]@

author = {N. Amiridze and T. Kutsia},

title = {{Anti-Unification and Natural Language Processing}},

booktitle = {{Fifth Workshop on Natural Language and Computer Science, NLCS’18}},

language = {english},

series = {EasyChair preprints},

number = {203},

pages = {1--12},

isbn_issn = { },

year = {2018},

editor = {A. Asudeh and V. de Paiva and L. Moss},

refereed = {yes},

length = {12},

url = {https://doi.org/10.29007/fkrh}

}

**inproceedings**{RISC5707,author = {N. Amiridze and T. Kutsia},

title = {{Anti-Unification and Natural Language Processing}},

booktitle = {{Fifth Workshop on Natural Language and Computer Science, NLCS’18}},

language = {english},

series = {EasyChair preprints},

number = {203},

pages = {1--12},

isbn_issn = { },

year = {2018},

editor = {A. Asudeh and V. de Paiva and L. Moss},

refereed = {yes},

length = {12},

url = {https://doi.org/10.29007/fkrh}

}

### Varieties of apolar subschemes of toric surfaces

#### Gallet Matteo, Ranestad Kristian, Villamizar Nelly

Ark. Mat. 56(1), pp. 73-99. 2018. ISSN 0004-2080. [url]@

author = {Gallet Matteo and Ranestad Kristian and Villamizar Nelly},

title = {{Varieties of apolar subschemes of toric surfaces}},

language = {english},

journal = {Ark. Mat.},

volume = {56},

number = {1},

pages = {73--99},

isbn_issn = { ISSN 0004-2080},

year = {2018},

refereed = {yes},

length = {27},

url = {https://doi.org/10.4310/ARKIV.2018.v56.n1.a6}

}

**article**{RISC5796,author = {Gallet Matteo and Ranestad Kristian and Villamizar Nelly},

title = {{Varieties of apolar subschemes of toric surfaces}},

language = {english},

journal = {Ark. Mat.},

volume = {56},

number = {1},

pages = {73--99},

isbn_issn = { ISSN 0004-2080},

year = {2018},

refereed = {yes},

length = {27},

url = {https://doi.org/10.4310/ARKIV.2018.v56.n1.a6}

}

### Varieties of apolar subschemes of toric surfaces

#### Gallet Matteo, Ranestad Kristian, Villamizar Nelly

Ark. Mat. 56(1), pp. 73-99. 2018. ISSN 0004-2080. [url]@

author = {Gallet Matteo and Ranestad Kristian and Villamizar Nelly},

title = {{Varieties of apolar subschemes of toric surfaces}},

language = {english},

journal = {Ark. Mat.},

volume = {56},

number = {1},

pages = {73--99},

isbn_issn = { ISSN 0004-2080},

year = {2018},

refereed = {yes},

length = {27},

url = {https://doi.org/10.4310/ARKIV.2018.v56.n1.a6}

}

**article**{RISC5811,author = {Gallet Matteo and Ranestad Kristian and Villamizar Nelly},

title = {{Varieties of apolar subschemes of toric surfaces}},

language = {english},

journal = {Ark. Mat.},

volume = {56},

number = {1},

pages = {73--99},

isbn_issn = { ISSN 0004-2080},

year = {2018},

refereed = {yes},

length = {27},

url = {https://doi.org/10.4310/ARKIV.2018.v56.n1.a6}

}

### Term-Graph Anti-Unification

#### Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

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

author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},

title = {{Term-Graph Anti-Unification}},

language = {english},

number = {18-02},

year = {2018},

length = {19},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

**techreport**{RISC5549,author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},

title = {{Term-Graph Anti-Unification}},

language = {english},

number = {18-02},

year = {2018},

length = {19},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Term-Graph Anti-Unification

#### Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Helene Kirchner (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 108, pp. 9:1-9:17. 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, ISBN 978-3-95977-077-4 ISSN 1868-8969. [url]@

author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},

title = {{Term-Graph Anti-Unification}},

booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},

language = {english},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {108},

pages = {9:1--9:17},

publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},

address = {Dagstuhl, Germany},

isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},

year = {2018},

editor = {Helene Kirchner},

refereed = {yes},

length = {17},

url = {http://drops.dagstuhl.de/opus/volltexte/2018/9179}

}

**inproceedings**{RISC5764,author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},

title = {{Term-Graph Anti-Unification}},

booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},

language = {english},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {108},

pages = {9:1--9:17},

publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},

address = {Dagstuhl, Germany},

isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},

year = {2018},

editor = {Helene Kirchner},

refereed = {yes},

length = {17},

url = {http://drops.dagstuhl.de/opus/volltexte/2018/9179}

}

### On some polynomials and series of Bloch-Polya Type

#### Berkovich A., Uncu A. K.

PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY 146(7), pp. 2827-2838. July 2018. 1088-6826. [url]@

author = {Berkovich A. and Uncu A.~K.},

title = {{On some polynomials and series of Bloch-Polya Type}},

language = {english},

journal = {PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY},

volume = {146},

number = {7},

pages = {2827--2838},

isbn_issn = {1088-6826},

year = {2018},

month = {July},

refereed = {yes},

keywords = {Mathematics - Number Theory, Mathematics - Combinatorics, 05A17, 05A19, 11B65, 11P81},

length = {12},

url = {http://www.ams.org/journals/proc/2018-146-07/S0002-9939-2018-13982-9/}

}

**article**{RISC5557,author = {Berkovich A. and Uncu A.~K.},

title = {{On some polynomials and series of Bloch-Polya Type}},

language = {english},

journal = {PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY},

volume = {146},

number = {7},

pages = {2827--2838},

isbn_issn = {1088-6826},

year = {2018},

month = {July},

refereed = {yes},

keywords = {Mathematics - Number Theory, Mathematics - Combinatorics, 05A17, 05A19, 11B65, 11P81},

length = {12},

url = {http://www.ams.org/journals/proc/2018-146-07/S0002-9939-2018-13982-9/}

}

### Some Elementary Partition Inequalities and Their Implications

#### Berkovich A., Uncu A. K.

ArXiv e-prints (to appear in Annals of Cobinatorics), pp. -. 2018. Preprint. [url]@

author = {Berkovich A. and Uncu A.~K.},

title = {{Some Elementary Partition Inequalities and Their Implications}},

language = {english},

journal = {ArXiv e-prints (to appear in Annals of Cobinatorics)},

pages = {--},

isbn_issn = {Preprint},

year = {2018},

refereed = {yes},

keywords = {Mathematics - Combinatorics, Mathematics - Number Theory, 05A15, 05A17, 05A19, 05A20, 11B65, 11P81, 11P84, 33D15},

length = {12},

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

}

**article**{RISC5558,author = {Berkovich A. and Uncu A.~K.},

title = {{Some Elementary Partition Inequalities and Their Implications}},

language = {english},

journal = {ArXiv e-prints (to appear in Annals of Cobinatorics)},

pages = {--},

isbn_issn = {Preprint},

year = {2018},

refereed = {yes},

keywords = {Mathematics - Combinatorics, Mathematics - Number Theory, 05A15, 05A17, 05A19, 05A20, 11B65, 11P81, 11P84, 33D15},

length = {12},

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

}

### Polynomial Identities Implying Capparelli's Partition Theorems

#### Ali Kemal Uncu, Alexander Berkovich

ArXiv e-prints (submitted), pp. -. 2018. N/A. [url]@

author = {Ali Kemal Uncu and Alexander Berkovich},

title = {{Polynomial Identities Implying Capparelli's Partition Theorems }},

language = {english},

journal = {ArXiv e-prints (submitted)},

pages = {--},

isbn_issn = {N/A},

year = {2018},

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 = {ArXiv e-prints (submitted)},

pages = {--},

isbn_issn = {N/A},

year = {2018},

refereed = {yes},

length = {21},

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

}

### Elementary Polynomial Identities Involving q-Trinomial Coefficients

#### Ali Kemal Uncu, Alexander Berkovich

ArXiv e-prints (submitted), pp. -. 2018. N/A. [url]@

author = {Ali Kemal Uncu and Alexander Berkovich},

title = {{Elementary Polynomial Identities Involving q-Trinomial Coefficients }},

language = {english},

journal = {ArXiv e-prints (submitted)},

pages = {--},

isbn_issn = {N/A},

year = {2018},

refereed = {yes},

length = {0},

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

}

**article**{RISC5791,author = {Ali Kemal Uncu and Alexander Berkovich},

title = {{Elementary Polynomial Identities Involving q-Trinomial Coefficients }},

language = {english},

journal = {ArXiv e-prints (submitted)},

pages = {--},

isbn_issn = {N/A},

year = {2018},

refereed = {yes},

length = {0},

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

}

### Refined q-Trinomial Coefficients and Two Infinite Hierarcies of q-Series Identities

#### Ali Kemal Uncu, Alexander Berkovich

ArXiv e-prints (submitted), pp. 1-10. 2018. N/A. [url]@

author = {Ali Kemal Uncu and Alexander Berkovich},

title = {{Refined q-Trinomial Coefficients and Two Infinite Hierarcies 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 hierarcies contains an identity which is equivalent to Capparelli's first Partition Theorem. },

journal = {ArXiv e-prints (submitted)},

pages = {1--10},

isbn_issn = {N/A},

year = {2018},

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 Hierarcies 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 hierarcies contains an identity which is equivalent to Capparelli's first Partition Theorem. },

journal = {ArXiv e-prints (submitted)},

pages = {1--10},

isbn_issn = {N/A},

year = {2018},

refereed = {yes},

length = {10},

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

}

### Generalizing some Results in Field Theory for Rings

#### Jose Capco

Communications in Algebra, pp. 0-12. 2018. 0092-7872. Preprint. [pdf]@

author = {Jose Capco},

title = {{Generalizing some Results in Field Theory for Rings}},

language = {english},

journal = {Communications in Algebra},

pages = {0--12},

isbn_issn = {0092-7872},

year = {2018},

note = {Preprint},

refereed = {no},

length = {13}

}

**article**{RISC5375,author = {Jose Capco},

title = {{Generalizing some Results in Field Theory for Rings}},

language = {english},

journal = {Communications in Algebra},

pages = {0--12},

isbn_issn = {0092-7872},

year = {2018},

note = {Preprint},

refereed = {no},

length = {13}

}

### Primitive Recursive Proof Systems for Arithmetic

#### David M. Cerna

RISC. Technical report, January 2018. In revision. [pdf]@

author = {David M. Cerna},

title = {{Primitive Recursive Proof Systems for Arithmetic}},

language = {english},

abstract = {Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extensionof the LK-calculus with equality and an additional inference rule formalizing induction.While this formalism was enough (with the addition of some meta-theoretic argumentation)to show the consistency of arithmetic, alternative formulations of induction such asthe infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmeticproofs obfuscated by the inference rule formulation of induction. For example, questionsconcerning the elimination of cut, consistency, and proof shape are given more clarity. Thesame could be said for functional interpretations of arithmetic such as system T whichenumerates the recursive functions provably total by arithmetic. A key feature of thesevariations on the formalization of arithmetic is that they get somewhat closer to formalizingthe concept of induction directly using the inferences of the LK-calculus, albeit byadding extra machinery at the meta-level. In this work we present a recursive sequentcalculus for arithmetic which can be syntactically translated into Gentzen formalism ofarithmetic and allows proof normalization to the LK-calculus with equality.},

year = {2018},

month = {January },

note = {In revision},

institution = {RISC},

length = {20}

}

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

title = {{Primitive Recursive Proof Systems for Arithmetic}},

language = {english},

abstract = {Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extensionof the LK-calculus with equality and an additional inference rule formalizing induction.While this formalism was enough (with the addition of some meta-theoretic argumentation)to show the consistency of arithmetic, alternative formulations of induction such asthe infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmeticproofs obfuscated by the inference rule formulation of induction. For example, questionsconcerning the elimination of cut, consistency, and proof shape are given more clarity. Thesame could be said for functional interpretations of arithmetic such as system T whichenumerates the recursive functions provably total by arithmetic. A key feature of thesevariations on the formalization of arithmetic is that they get somewhat closer to formalizingthe concept of induction directly using the inferences of the LK-calculus, albeit byadding extra machinery at the meta-level. In this work we present a recursive sequentcalculus for arithmetic which can be syntactically translated into Gentzen formalism ofarithmetic and allows proof normalization to the LK-calculus with equality.},

year = {2018},

month = {January },

note = {In revision},

institution = {RISC},

length = {20}

}

### Idempotent Anti-unification

#### David M. Cerna Temur Kutsia

RISC. Technical report, Feb. 2018. Submitted for review. [pdf]@

author = {David M. Cerna Temur Kutsia},

title = {{Idempotent Anti-unification }},

language = {english},

abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},

year = {2018},

month = {Feb.},

note = {Submitted for review},

institution = {RISC},

length = {27}

}

**techreport**{RISC5530,author = {David M. Cerna Temur Kutsia},

title = {{Idempotent Anti-unification }},

language = {english},

abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},

year = {2018},

month = {Feb.},

note = {Submitted for review},

institution = {RISC},

length = {27}

}

### A General Recursive Construction for Schematic Resolution Derivations

#### David M. Cerna

2018. submitted for review. Preprint. [pdf]@

author = {David M. Cerna},

title = {{A General Recursive Construction for Schematic Resolution Derivations}},

language = {english},

abstract = {Proof schemata provide an alternative formalism for handling inductive argumentation, while non-trivially extending {\em Herbrand's theorem} to a fragment of arithmetic and thus allowing the construction of {\em Herbrand sequents} and {\em expansion trees}. Existing proof analysis methods for proof schemata extract an unsatisfiable characteristic formula representing the cut structure of the proof and from its refutation construct a Herbrand sequent. Unfortunately, constructing the refutation is a task which is highly non-trivial. An automated method for constructing such refutations exists, but it only works for a very weak fragment of arithmetic and is hard to use interactively. More expressive yet interactive methods for the formalization of recursive resolution refutation are complex, hard to work with, and still limited to an undesirably weak class of recursion. In this work we note a particular problem with previous methods, namely they mix the recursive structure with the calculus of refutation. Also we present a modular recursive structure independent of the resolution formalism and proof construction. We illustrate the expressive power of the so called {\em finite saturated tree} formalism by formalizing the Non-injectivity Assertion's schematic refutation (a variant of the infinitary Pigeonhole principle). None of the previously developed formalism are able to formalize this refutation.},

year = {2018},

note = {submitted for review},

length = {42},

type = {Preprint},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

title = {{A General Recursive Construction for Schematic Resolution Derivations}},

language = {english},

abstract = {Proof schemata provide an alternative formalism for handling inductive argumentation, while non-trivially extending {\em Herbrand's theorem} to a fragment of arithmetic and thus allowing the construction of {\em Herbrand sequents} and {\em expansion trees}. Existing proof analysis methods for proof schemata extract an unsatisfiable characteristic formula representing the cut structure of the proof and from its refutation construct a Herbrand sequent. Unfortunately, constructing the refutation is a task which is highly non-trivial. An automated method for constructing such refutations exists, but it only works for a very weak fragment of arithmetic and is hard to use interactively. More expressive yet interactive methods for the formalization of recursive resolution refutation are complex, hard to work with, and still limited to an undesirably weak class of recursion. In this work we note a particular problem with previous methods, namely they mix the recursive structure with the calculus of refutation. Also we present a modular recursive structure independent of the resolution formalism and proof construction. We illustrate the expressive power of the so called {\em finite saturated tree} formalism by formalizing the Non-injectivity Assertion's schematic refutation (a variant of the infinitary Pigeonhole principle). None of the previously developed formalism are able to formalize this refutation.},

year = {2018},

note = {submitted for review},

length = {42},

type = {Preprint},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Higher-Order Equational Pattern Anti-Unification

#### David M. Cerna, Temur Kutsia

In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Helene Kirchner (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 108, pp. 12:1-12:17. 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, ISBN 978-3-95977-077-4 ISSN 1868-8969. [url]@

author = {David M. Cerna and Temur Kutsia},

title = {{Higher-Order Equational Pattern Anti-Unification}},

booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},

language = {english},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {108},

pages = {12:1--12:17},

publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},

address = {Dagstuhl, Germany},

isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},

year = {2018},

editor = {Helene Kirchner},

refereed = {yes},

length = {17},

url = {http://drops.dagstuhl.de/opus/volltexte/2018/9182}

}

**inproceedings**{RISC5765,author = {David M. Cerna and Temur Kutsia},

title = {{Higher-Order Equational Pattern Anti-Unification}},

booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},

language = {english},

series = {Leibniz International Proceedings in Informatics (LIPIcs)},

volume = {108},

pages = {12:1--12:17},

publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},

address = {Dagstuhl, Germany},

isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},

year = {2018},

editor = {Helene Kirchner},

refereed = {yes},

length = {17},

url = {http://drops.dagstuhl.de/opus/volltexte/2018/9182}

}

### Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques

#### Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

Journal of Symbolic Computation 90, pp. 3-41. 2018. Elsevier, 07477171. [url]@

author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},

title = {{Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {90},

pages = {3--41},

publisher = {Elsevier},

isbn_issn = {07477171},

year = {2018},

refereed = {yes},

keywords = {algorithm synthesis ; automated reasoning ; natural--style proving},

length = {39},

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

}

**article**{RISC5715,author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},

title = {{Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {90},

pages = {3--41},

publisher = {Elsevier},

isbn_issn = {07477171},

year = {2018},

refereed = {yes},

keywords = {algorithm synthesis ; automated reasoning ; natural--style proving},

length = {39},

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

}

### Pattern-based calculi with finitary matching

#### Sandra Alves, Besik Dundua, Mário Florido, Temur Kutsia

Logic Journal of the IGPL 26(2), pp. 203-243. 2018. ISSN 1367-0751. [url]@

author = {Sandra Alves and Besik Dundua and Mário Florido and Temur Kutsia},

title = {{Pattern-based calculi with finitary matching}},

language = {english},

journal = {Logic Journal of the IGPL},

volume = {26},

number = {2},

pages = {203--243},

isbn_issn = {ISSN 1367-0751},

year = {2018},

refereed = {yes},

length = {41},

url = {https://doi.org/10.1093/JIGPAL/jzx059}

}

**article**{RISC5763,author = {Sandra Alves and Besik Dundua and Mário Florido and Temur Kutsia},

title = {{Pattern-based calculi with finitary matching}},

language = {english},

journal = {Logic Journal of the IGPL},

volume = {26},

number = {2},

pages = {203--243},

isbn_issn = {ISSN 1367-0751},

year = {2018},

refereed = {yes},

length = {41},

url = {https://doi.org/10.1093/JIGPAL/jzx059}

}