# Generalization ALgorithms and Applications [GALA]

### Project Lead

### Project Duration

01/02/2016 - 31/01/2021### Project URL

Go to Website## Partners

### The Austrian Science Fund (FWF)

## Publications

### 2020

[Cerna]

### Unital Anti-Unification: Type and Algorithms

#### David M. Cerna , Temur Kutsia

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

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

title = {{Unital Anti-Unification: Type and Algorithms}},

language = {english},

abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },

number = {20-02},

year = {2020},

month = {Febrary},

howpublished = {RISC Report},

keywords = {Anti-unification, tree grammars, unital theories, collapse theories},

length = {19},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

title = {{Unital Anti-Unification: Type and Algorithms}},

language = {english},

abstract = {Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete and return tree grammars from which set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions. },

number = {20-02},

year = {2020},

month = {Febrary},

howpublished = {RISC Report},

keywords = {Anti-unification, tree grammars, unital theories, collapse theories},

length = {19},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

[Kutsia]

### Unification modulo alpha-equivalence in a mathematical assistant system

#### Temur Kutsia

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

author = {Temur Kutsia},

title = {{Unification modulo alpha-equivalence in a mathematical assistant system}},

language = {english},

number = {20-01},

year = {2020},

length = {21},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

**techreport**{RISC6074,author = {Temur Kutsia},

title = {{Unification modulo alpha-equivalence in a mathematical assistant system}},

language = {english},

number = {20-01},

year = {2020},

length = {21},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### 2019

[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 = {In this paper we address Three problems related to unital anti-unification. First, we develop a generalalgorithm based on a tree grammar representation of the set of computed generalizations. Secondlywe show that restricting the algorithm to computing linear generalizations only or to term signaturescontaining a single unital function results in a procedure which is minimal complete and Finitary.Thirdly, we show that when the term signature contains two unital functions, unital anti-unification isNullary.The algorithm does not depend on the number of idempotent function symbols in the input terms. Thelanguage generated by the grammar is the minimal complete set of generalizations of the givenanti-unification problem, which implies that idempotent anti-unification is infinitary.},

year = {2019},

length = {40},

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 = {In this paper we address Three problems related to unital anti-unification. First, we develop a generalalgorithm based on a tree grammar representation of the set of computed generalizations. Secondlywe show that restricting the algorithm to computing linear generalizations only or to term signaturescontaining a single unital function results in a procedure which is minimal complete and Finitary.Thirdly, we show that when the term signature contains two unital functions, unital anti-unification isNullary.The algorithm does not depend on the number of idempotent function symbols in the input terms. Thelanguage generated by the grammar is the minimal complete set of generalizations of the givenanti-unification problem, which implies that idempotent anti-unification is infinitary.},

year = {2019},

length = {40},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

[Cerna]

### A Generic Framework for Higher-Order Generalizations

#### David M. Cerna, Temur Kutsia

In: Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [url]@

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

title = {{A Generic Framework for Higher-Order Generalizations}},

booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},

language = {english},

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

volume = {131},

pages = {10:1--10:19},

publisher = {Schloss Dagstuhl},

isbn_issn = {ISSN 1868-8969},

year = {2019},

editor = {Herman Geuvers},

refereed = {yes},

length = {19},

url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}

}

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

title = {{A Generic Framework for Higher-Order Generalizations}},

booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},

language = {english},

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

volume = {131},

pages = {10:1--10:19},

publisher = {Schloss Dagstuhl},

isbn_issn = {ISSN 1868-8969},

year = {2019},

editor = {Herman Geuvers},

refereed = {yes},

length = {19},

url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}

}

[Cerna]

### Idempotent Anti-unification

#### David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2019. ACM Press, ISSN 1529-3785. [url] [pdf]@

author = {David Cerna and Temur Kutsia},

title = {{Idempotent Anti-unification}},

language = {english},

journal = {ACM Transactions on Computational Logic (TOCL)},

volume = {21},

number = {2},

pages = {10:1--10:32},

publisher = {ACM Press},

isbn_issn = {ISSN 1529-3785},

year = {2019},

refereed = {yes},

length = {32},

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

}

**article**{RISC6023,author = {David Cerna and Temur Kutsia},

title = {{Idempotent Anti-unification}},

language = {english},

journal = {ACM Transactions on Computational Logic (TOCL)},

volume = {21},

number = {2},

pages = {10:1--10:32},

publisher = {ACM Press},

isbn_issn = {ISSN 1529-3785},

year = {2019},

refereed = {yes},

length = {32},

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

}

[Dundua]

### Variadic Equational Matching

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

In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen (ed.), Lecture Notes in Computer Science 11617, pp. 77-92. 2019. Springer, ISBN 978-3-030-23249-8. [pdf]@

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

title = {{Variadic Equational Matching}},

booktitle = {{Intelligent Computer Mathematics - 12th International Conference, CICM 2019}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {11617},

pages = {77--92},

publisher = {Springer},

isbn_issn = {ISBN 978-3-030-23249-8},

year = {2019},

editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti Coen},

refereed = {yes},

length = {16}

}

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

title = {{Variadic Equational Matching}},

booktitle = {{Intelligent Computer Mathematics - 12th International Conference, CICM 2019}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {11617},

pages = {77--92},

publisher = {Springer},

isbn_issn = {ISBN 978-3-030-23249-8},

year = {2019},

editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti Coen},

refereed = {yes},

length = {16}

}

[Pau]

### Computing All Maximal Clique Partitions in a Graph

#### Temur Kutsia, Cleo Pau

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

author = {Temur Kutsia and Cleo Pau},

title = {{Computing All Maximal Clique Partitions in a Graph}},

language = {english},

number = {19-04},

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**{RISC5939,author = {Temur Kutsia and Cleo Pau},

title = {{Computing All Maximal Clique Partitions in a Graph}},

language = {english},

number = {19-04},

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}

}

[Pau]

### Solving Proximity Constraints

#### Temur Kutsia, Cleo Pau

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

author = {Temur Kutsia and Cleo Pau},

title = {{Solving Proximity Constraints}},

language = {english},

number = {19-06},

year = {2019},

length = {22},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

title = {{Solving Proximity Constraints}},

language = {english},

number = {19-06},

year = {2019},

length = {22},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

[Pau]

### Matching and Generalization Modulo Proximity and Tolerance

#### Temur Kutsia, Cleo Pau

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

author = {Temur Kutsia and Cleo Pau},

title = {{Matching and Generalization Modulo Proximity and Tolerance}},

language = {english},

number = {19-07},

year = {2019},

length = {5},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

title = {{Matching and Generalization Modulo Proximity and Tolerance}},

language = {english},

number = {19-07},

year = {2019},

length = {5},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

[Pau]

### Solving Proximity Constraints

#### Temur Kutsia, Cleo Pau

In: Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019. Revised Selected Papers, Maurizio Gabbrielli (ed.), Lecture Notes in Computer Science 12042, pp. 107-122. 2019. ISBN 978-3-030-45259-9. [pdf]@

author = {Temur Kutsia and Cleo Pau},

title = {{Solving Proximity Constraints}},

booktitle = {{Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019. Revised Selected Papers}},

language = {english},

series = {Lecture Notes in Computer Science },

volume = {12042},

pages = {107--122},

isbn_issn = {ISBN 978-3-030-45259-9},

year = {2019},

editor = {Maurizio Gabbrielli},

refereed = {yes},

length = {16}

}

**inproceedings**{RISC6100,author = {Temur Kutsia and Cleo Pau},

title = {{Solving Proximity Constraints}},

booktitle = {{Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019. Revised Selected Papers}},

language = {english},

series = {Lecture Notes in Computer Science },

volume = {12042},

pages = {107--122},

isbn_issn = {ISBN 978-3-030-45259-9},

year = {2019},

editor = {Maurizio Gabbrielli},

refereed = {yes},

length = {16}

}

### 2018

[Amiridze]

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

}

[Baumgartner]

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

}

[Cerna]

### Primitive Recursive Proof Systems for Arithmetic

#### David M. Cerna

RISC. Technical report, January 2018. In revision. [pdf] [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}

}

[Cerna]

### Idempotent Anti-unification

#### David M. Cerna, Temur Kutsia

RISC. Technical report, Feb. 2018. to appear in TOCL. [pdf]@

author = {David M. Cerna and 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 = {to appear in TOCL},

institution = {RISC},

length = {32}

}

**techreport**{RISC5530,author = {David M. Cerna and 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 = {to appear in TOCL},

institution = {RISC},

length = {32}

}

[Cerna]

### A General Recursive Construction for Schematic Resolution Derivations

#### David M. Cerna

2018.@

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

length = {42},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

**techreport**{RISC5982,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},

length = {42},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

[Dundua]

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

}

[Kutsia]

### Idempotent Generalization is Infinitary

#### David M. Cerna and Temur Kutsia

RISC. Technical report, RISC Report, 2018. [pdf]@

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

title = {{Idempotent Generalization is Infinitary}},

language = {english},

abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},

year = {2018},

howpublished = {RISC Report},

institution = {RISC},

length = {1}

}

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

title = {{Idempotent Generalization is Infinitary}},

language = {english},

abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},

year = {2018},

howpublished = {RISC Report},

institution = {RISC},

length = {1}

}

[Pau]

### Proximity-Based Generalization

#### Temur Kutsia, Cleo Pau

In: 32nd International Workshop on Unification, UNIF 2018, Mauricio Ayala-Rincon and Philippe Balbiani (ed.), pp. - . 2018. [pdf]@

author = {Temur Kutsia and Cleo Pau},

title = {{Proximity-Based Generalization}},

booktitle = {{32nd International Workshop on Unification, UNIF 2018}},

language = {english},

pages = { -- },

isbn_issn = { },

year = {2018},

editor = {Mauricio Ayala-Rincon and Philippe Balbiani},

refereed = {yes},

length = {0}

}

**inproceedings**{RISC5713,author = {Temur Kutsia and Cleo Pau},

title = {{Proximity-Based Generalization}},

booktitle = {{32nd International Workshop on Unification, UNIF 2018}},

language = {english},

pages = { -- },

isbn_issn = { },

year = {2018},

editor = {Mauricio Ayala-Rincon and Philippe Balbiani},

refereed = {yes},

length = {0}

}

### 2017

[Cerna]

### Integrating a Global Induction Mechanism into a Sequent Calculus

#### David M. Cerna and Michael Lettmann

In: TABLEAUX 2017, Renate A. Schmidt and Cl{\'{a}}udia Nalon (ed.), Proceedings of Tableaux, lecture notes in computer science , pp. 278-294. September 2017. Springer, 978-3-319-66901-4.@

author = {David M. Cerna and Michael Lettmann},

title = {{Integrating a Global Induction Mechanism into a Sequent Calculus}},

booktitle = {{TABLEAUX 2017}},

language = {english},

abstract = {Most interesting proofs in mathematics contain an inductive argument which requires an extension of the \textbf{LK}-calculus to formalize. The mostcommonly used calculi contain a separate rule or axiom which reduces the important proof theoretic properties of the calculus. In such cases cut-elimination does not result in analytic proofs, i.e.\ every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a generalization of \textbf{LK}-proofs able to simulate induction by linking proofs, indexed by a natural number, together.Using a global cut-elimination method a normal form can be reached which allows a schema of {\em Herbrand Sequents} to be produced, an essential step for proof analysis in the presence ofinduction. However, proof schema have only been studied in a limited context and are currentlydefined for a very particular proof structure based on a slight extension of the \textbf{LK}-calculus. The result is an opaque and complex formalization. In this paper, we introduce a calculus integrating the proof schema formalization and in the process we elucidate properties of proof schemata which can be used to extend the formalism. },

series = {lecture notes in computer science},

pages = {278--294},

publisher = {Springer},

isbn_issn = {978-3-319-66901-4},

year = {2017},

month = {September},

editor = {Renate A. Schmidt and Cl{\'{a}}udia Nalon},

refereed = {yes},

length = {16},

conferencename = {Tableaux}

}

**inproceedings**{RISC5471,author = {David M. Cerna and Michael Lettmann},

title = {{Integrating a Global Induction Mechanism into a Sequent Calculus}},

booktitle = {{TABLEAUX 2017}},

language = {english},

abstract = {Most interesting proofs in mathematics contain an inductive argument which requires an extension of the \textbf{LK}-calculus to formalize. The mostcommonly used calculi contain a separate rule or axiom which reduces the important proof theoretic properties of the calculus. In such cases cut-elimination does not result in analytic proofs, i.e.\ every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a generalization of \textbf{LK}-proofs able to simulate induction by linking proofs, indexed by a natural number, together.Using a global cut-elimination method a normal form can be reached which allows a schema of {\em Herbrand Sequents} to be produced, an essential step for proof analysis in the presence ofinduction. However, proof schema have only been studied in a limited context and are currentlydefined for a very particular proof structure based on a slight extension of the \textbf{LK}-calculus. The result is an opaque and complex formalization. In this paper, we introduce a calculus integrating the proof schema formalization and in the process we elucidate properties of proof schemata which can be used to extend the formalism. },

series = {lecture notes in computer science},

pages = {278--294},

publisher = {Springer},

isbn_issn = {978-3-319-66901-4},

year = {2017},

month = {September},

editor = {Renate A. Schmidt and Cl{\'{a}}udia Nalon},

refereed = {yes},

length = {16},

conferencename = {Tableaux}

}

[Cerna]

### Towards a Clausal Analysis of Proof Schemata

#### David M. Cerna and Michael Lettmann

In: SYNASC 2017, Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephan Watt (ed.), IEEE Xplore , pp. 113-120. September 2017. 978-1-5386-2625-2.@

author = {David M. Cerna and Michael Lettmann},

title = {{Towards a Clausal Analysis of Proof Schemata}},

booktitle = {{SYNASC 2017}},

language = {english},

abstract = {Proof schemata are a variant of \LK-proofs able to simulate various induction schemes in first-order logic by adding so called {\em links} to the standard first-order \LK-calculus. Links allow proofs to reference other proofs, and thus give schemata a recursive structure. {\em Gentzen} style cut-elimination methods, which reduce cuts locally, does not work in the presence of links. However, an alternative method, such as cut-elimination by resolution (CERES), which eliminate cuts globally, is able to reduce cuts over the entire recursive structure simultaneously. Unfortunately, analysis of the cut structure of a proof after partial cut-elimination is non-trivial. By extending local methods to proof schemata, we provide such an analysis. },

series = {IEEE Xplore},

pages = {113--120},

isbn_issn = {978-1-5386-2625-2},

year = {2017},

month = {September},

editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephan Watt},

refereed = {yes},

length = {8}

}

**inproceedings**{RISC5472,author = {David M. Cerna and Michael Lettmann},

title = {{Towards a Clausal Analysis of Proof Schemata}},

booktitle = {{SYNASC 2017}},

language = {english},

abstract = {Proof schemata are a variant of \LK-proofs able to simulate various induction schemes in first-order logic by adding so called {\em links} to the standard first-order \LK-calculus. Links allow proofs to reference other proofs, and thus give schemata a recursive structure. {\em Gentzen} style cut-elimination methods, which reduce cuts locally, does not work in the presence of links. However, an alternative method, such as cut-elimination by resolution (CERES), which eliminate cuts globally, is able to reduce cuts over the entire recursive structure simultaneously. Unfortunately, analysis of the cut structure of a proof after partial cut-elimination is non-trivial. By extending local methods to proof schemata, we provide such an analysis. },

series = {IEEE Xplore},

pages = {113--120},

isbn_issn = {978-1-5386-2625-2},

year = {2017},

month = {September},

editor = {Tudor Jebelean and Viorel Negru and Dana Petcu and Daniela Zaharie and Tetsuo Ida and Stephan Watt},

refereed = {yes},

length = {8}

}