# Theorema Project

### Project Description

The *Theorema* project aims at extending current computer algebra systems by facilities for supporting mathematical proving. The present early-prototype version of the *Theorema* software system is implemented in *Mathematica *. The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. The individual provers imitate the proof style of human mathematicians and produce human-readable proofs in natural language presented in nested cells. The special provers are intimately connected with the functors that build up the various mathematical domains.

The long-term goal of the project is to produce a complete system which supports the mathematician in creating interactive textbooks, i.e. books containing, besides the ordinary passive text, *active* text representing *algorithms* in executable format, as well as *proofs* which can be studied at various levels of detail, and whose routine parts can be automatically generated. This system will provide a uniform (logic and software) framework in which a working mathematician, without leaving the system, can get computer-support while looping through all phases of the mathematical problem solving cycle:

- the phase of
*specifying a problem*including the compilation of relevant knowledge and the definition of new concepts (predicates, functions) and auxiliary algorithms; - the phase of
*exploring*a given problem and creating ideas and conjectures by studying examples using the available knowledge and algorithms; - the phase of
*proving*or disproving conjectures and thereby increasing the relevant knowledge base; - the phase of
*programming*, i.e. transforming useful new and provenly correct mathematical knowledge into algorithms for solving the initial problem; - the phase of
*writing up one’s finding*in interactive mathematical documents.

### Project Lead

### Project Duration

01/01/1994 -## Software

The present prototype version of the Theorema software system is implemented in Mathematica . The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. ...

## Publications

### 2022

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

}

### 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]**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)}

}

### Learning to Reason Assisted by Automated Reasoning

#### W. Windsteiger

In: Intelligent Computer Mathematics: 15th International Conference, K. Buzzard and T. Kutsia (ed.), Proceedings of CICM 2022, Lecture Notes in Artificial Intelligence LNAI 13467, pp. 305-320. 2022. Springer, ISBN 978-3-031-16681-5. [doi] [pdf]**inproceedings**{RISC6530,

author = {W. Windsteiger},

title = {{Learning to Reason Assisted by Automated Reasoning}},

booktitle = {{Intelligent Computer Mathematics: 15th International Conference}},

language = {english},

abstract = {We report on using logic software in a novel course-format for an undergraduate logic course for studentsin computer science or artificial intelligence. Although being designed as the students' basic introduction tothe field of logic, the course features a novel structure and it adds some modern content, such as SATand SMT solving, to the traditional and established topics, such as propositional logicand first order predicate logic. The novel course design is characterized by, among others, the integration ofexisting logic software into the teaching of logic.In this paper we focus on the module on first-order predicate logic and the use of the Theorema system as a proof-tutor for the students. We report on statistical evaluation of data collected over two consecutiveyears of teaching this course. On the one hand, we asked for feedback of students on howhelpful they felt the software support was. On the other hand, we evaluated their results in the exams during thecourse and their development over the entire teaching period. The performance in exams is then correlated withstudents'' own perception of the helpfulness of software.},

series = {Lecture Notes in Artificial Intelligence LNAI},

number = {13467},

pages = {305--320},

publisher = {Springer},

isbn_issn = {ISBN 978-3-031-16681-5},

year = {2022},

editor = {K. Buzzard and T. Kutsia},

refereed = {yes},

length = {16},

conferencename = {CICM 2022},

url = {https://doi.org/10.1007/978-3-031-16681-5_22}

}

### 2021

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

}

### Variadic equational matching in associative and commutative theories

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

Journal of Symbolic Computation 106, pp. 78-109. 2021. Elsevier, ISSN 0747-7171. [doi] [pdf]**article**{RISC6260,

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

title = {{Variadic equational matching in associative and commutative theories}},

language = {english},

journal = {Journal of Symbolic Computation},

volume = {106},

pages = {78--109},

publisher = {Elsevier},

isbn_issn = {ISSN 0747-7171},

year = {2021},

refereed = {yes},

length = {32},

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

}

### A Heuristic Prover for Elementary Analysis in Theorema

#### T. Jebelean

In: Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania, F. Kamaredine, C. Sacerdoti Coen (ed.), Proceedings of Intelligent Computer Mathematics, 14th International Conference, CICM 2021, LNAI 12833, pp. 130-134. July 2021. Springer, 978-3-030-81096-2. [pdf]**inproceedings**{RISC6477,

author = {T. Jebelean},

title = {{A Heuristic Prover for Elementary Analysis in Theorema}},

booktitle = {{Intelligent Computer Mathematics, 14th International Conference, CICM 2021, Timisoara, Romania}},

language = {english},

abstract = { We present a plug-in to the Theorema system, which generates proofs similar to those produced by humans for theorems in elementary analysis and is based on heuristic techniques combining methods from automated reasoning and computer algebra. The prover is able to construct automatically natural-style proofs for various examples related to convergence of sequences as well as to limits, continuity, and uniform continuity of functions. Additionally to general inference rules for predicate logic, the techniques used are: the S-decomposition method for formulae with alternating quantifiers, use of Quantifier Elimination by Cylindrical Algebraic Decomposition, analysis of terms behavior in zero, bounding the epsilon-bounds, semantic simplification of expressions involving absolute value, polynomial arithmetic, usage of equal arguments to arbitrary functions, and automatic reordering of proof steps in order to check the admissibility of solutions to the metavariables. The problem of proving such theorems directly without using refutation and clausification is logically equivalent to the problem of satisfiability modulo the theory of real numbers, thus these techniques are relevant for SMT solving also.},

series = {LNAI},

volume = {12833},

pages = {130--134},

publisher = {Springer},

isbn_issn = {978-3-030-81096-2},

year = {2021},

month = {July},

editor = {F. Kamaredine and C. Sacerdoti Coen},

refereed = {yes},

keywords = {Satisfiability Checking, Natural-style Proofs, Computer Algebra, Symbolic Computation, Satisfiability Modulo Theories},

length = {5},

conferencename = {Intelligent Computer Mathematics, 14th International Conference, CICM 2021}

}

### Proximity-Based Unification and Matching for Full Fuzzy Signatures

#### Temur Kutsia, Cleo Pau

Technical report no. 21-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]**techreport**{RISC6296,

author = {Temur Kutsia and Cleo Pau},

title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},

language = {english},

abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},

number = {21-08},

year = {2021},

month = {April},

keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},

length = {15},

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

}

### Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures

#### Temur Kutsia, Cleo Pau

Technical report no. 21-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]**techreport**{RISC6297,

author = {Temur Kutsia and Cleo Pau},

title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},

language = {english},

abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},

number = {21-09},

year = {2021},

month = {April},

keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},

length = {15},

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

}

### Automated Theorem Proving in the Classroom

#### W. Windsteiger

In: Proceedings Automated Deduction in Geometry (ADG 2021), Predrag Janicic (ed.), Proceedings of Automated Deduction in Geometry (ADG 2021), Electronic Proceedings in Theoretical Computer Science (EPTCS) 352, pp. 54-63. 2021. ISSN 2075-2180. Extended abstract. [doi] [pdf]**inproceedings**{RISC6355,

author = {W. Windsteiger},

title = {{Automated Theorem Proving in the Classroom}},

booktitle = {{Proceedings Automated Deduction in Geometry (ADG 2021)}},

language = {english},

abstract = {We report on several scenarios of using automated theorem proving software in university education. In particular,we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial intelligence. The purpose of using logic-software in our teaching is emph{not} to teach studentsthe proper use of a particular piece of software. In contrast, we try to emph{employ} certain software in orderto spark students' motivation and to support their understanding of logic principles they are supposed tounderstand after having passed the course. In a sense, we try to let the software act as a logic-tutor, the software is not an additional subject we teach.},

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

volume = {352},

pages = {54--63},

isbn_issn = {ISSN 2075-2180},

year = {2021},

note = {Extended abstract},

editor = {Predrag Janicic},

refereed = {no},

length = {10},

conferencename = {Automated Deduction in Geometry (ADG 2021)},

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

}

### Automated Theorem Proving in the Classroom

#### W. Windsteiger

Technical report no. 21-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2021. Extended version of keynote talk at ADG 2021 conference. Licensed under CC BY 4.0 International. [doi] [pdf]**techreport**{RISC6356,

author = {W. Windsteiger},

title = {{Automated Theorem Proving in the Classroom}},

language = {english},

abstract = {We report on several scenarios of using automated theorem proving software in university education. In particular,we focus on using the Theorema system in a software-enhanced logic-course for students in computer science or artificial intelligence. The purpose of using logic-software in our teaching is emph{not} to teach studentsthe proper use of a particular piece of software. In contrast, we try to emph{employ} certain software in orderto spark students' motivation and to support their understanding of logic principles they are supposed tounderstand after having passed the course. In a sense, we try to let the software act as a logic-tutor, the software is not an additional subject we teach.},

number = {21-15},

year = {2021},

month = {August},

note = {Extended version of keynote talk at ADG 2021 conference},

keywords = {Theorema, Logic Education},

length = {18},

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

}

### 2020

### Idempotent Anti-unification

#### David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [doi] [pdf]**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 = {2020},

refereed = {yes},

length = {32},

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

}

### Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema

#### Isabela Dramnesc, Tudor Jebelean

Technical report no. 20-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2020. [pdf]**techreport**{RISC6094,

author = {Isabela Dramnesc and Tudor Jebelean},

title = {{Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema}},

language = {english},

number = {20-04},

year = {2020},

month = {April},

length = {25},

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

}

### Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema

#### Isabela Dramnesc, Tudor Jebelean

Technical report no. 20-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). September 2020. [pdf]**techreport**{RISC6206,

author = {Isabela Dramnesc and Tudor Jebelean},

title = {{Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema}},

language = {English},

abstract = {We demonstrate the deduction based synthesis of element deletion algorithms for[sorted] lists and [sorted] binary trees, by first developing the necessary theory which ismulti–type: basic ordered elements, multisets, lists, and trees. The generated algorithms are“pattern matching”, namely sets of conditional equalities, and we also demonstrate theirtransformation into functional algorithms and, for lists, into tail recursive algorithms. Thiswork constitutes a case study first in theory exploration and second in automated synthesisand transformation of algorithms synthesized on the basis of natural style proofs, whichallows to investigate the heuristics of theory construction on multiple types, as well as thenatural style inferences and strategies for constructing human readable synthesis proofs. Theexperiments are performed in the frame of the Theorema system.},

number = {20-15},

year = {2020},

month = {September},

keywords = {automated reasoning; algorithm synthesis; lists; binary trees; multisets; Theorema},

length = {22},

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

}

### Constraint Solving over Multiple Similarity Relations

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

In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 30:1-30:19. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [doi]**inproceedings**{RISC6133,

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

title = {{Constraint Solving over Multiple Similarity Relations}},

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

language = {english},

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

volume = {167},

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

publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},

isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},

year = {2020},

editor = {Zena M. Ariola},

refereed = {yes},

length = {19},

url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.30}

}

### Specification and Analysis of ABAC Policies in a Rule-Based Framework

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

In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 101-116. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [doi] [pdf]**incollection**{RISC6228,

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

title = {{Specification and Analysis of ABAC Policies in a Rule-Based Framework}},

booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},

language = {english},

series = {Springer Proceedings in Mathematics & Statistics},

volume = {334},

pages = {101--116},

publisher = {Springer},

isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},

year = {2020},

editor = {George Jaiani and David Natroshvili},

refereed = {yes},

length = {16},

url = {https://doi.org/10.1007/978-3-030-56356-1_7}

}

### A Rule-Based System for Computation and Deduction in Mathematica

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

In: WRLA 2020: Rewriting Logic and Its Applications, Santiago Escobar, Narciso Martí-Oliet (ed.), Lecture Notes in Computer Science 12328, pp. 57-74. 2020. Springer, ISBN 978-3-030-63595-4, 978-3-030-63594-7. [doi] [pdf]**inproceedings**{RISC6229,

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

title = {{A Rule-Based System for Computation and Deduction in Mathematica}},

booktitle = {{WRLA 2020: Rewriting Logic and Its Applications}},

language = {english},

series = { Lecture Notes in Computer Science},

volume = {12328},

pages = {57--74},

publisher = {Springer},

isbn_issn = {ISBN 978-3-030-63595-4, 978-3-030-63594-7},

year = {2020},

editor = {Santiago Escobar and Narciso Martí-Oliet},

refereed = {yes},

length = {18},

url = {https://doi.org/10.1007/978-3-030-63595-4_4}

}

### Extending the 𝜌Log Calculus with Proximity Relations

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

In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 83-100. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [doi] [pdf]**incollection**{RISC6227,

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

title = {{Extending the 𝜌Log Calculus with Proximity Relations}},

booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},

language = {english},

series = {Springer Proceedings in Mathematics & Statistics},

volume = {334},

pages = {83--100},

publisher = {Springer},

isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},

year = {2020},

editor = {George Jaiani and David Natroshvili},

refereed = {yes},

length = {18},

url = {https://doi.org/10.1007/978-3-030-56356-1_6}

}

### Unranked Nominal Unification

#### Besik Dundua, Temur Kutsia, Mikheil Rukhaia

Technical report no. 20-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2020. [pdf]**techreport**{RISC6273,

author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},

title = {{Unranked Nominal Unification}},

language = {english},

number = {20-21},

year = {2020},

sponsor = {FWF, project 28789-N32},

length = {18},

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

}

### 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, Austria. ISSN 2791-4267 (online). 2020. [pdf]**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 = {Altenberger Straße 69, 4040 Linz, Austria},

issn = {2791-4267 (online)}

}

### 2019

### 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. [doi]**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}

}