# 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

### 2020

### 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, Schloss Hagenberg, 4232 Hagenberg, Austria. 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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### 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, Schloss Hagenberg, 4232 Hagenberg, Austria. 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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

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

}

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

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

}

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

}

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

}

### A Rule-based Approach to the Decidability of Safety of ABACα

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

In: Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019, Florian Kerschbaum, Atefeh Mashatan, Jianwei Niu, Adam J. Lee (ed.), pp. 173-178. 2019. ACM, ISBN 978-1-4503-6753-0. [url] [pdf]**inproceedings**{RISC5955,

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

title = {{A Rule-based Approach to the Decidability of Safety of ABACα}},

booktitle = {{Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019}},

language = {english},

pages = {173--178},

publisher = {ACM},

isbn_issn = {ISBN 978-1-4503-6753-0},

year = {2019},

editor = {Florian Kerschbaum and Atefeh Mashatan and Jianwei Niu and Adam J. Lee},

refereed = {yes},

length = {6},

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

}

### 2018

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

}

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

}

### Experiments with Automatic Proofs in Elementary Analysis

#### T. Jebelean

Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2018. Work in progress. [zip] [pdf] [pdf]**techreport**{RISC5692,

author = {T. Jebelean},

title = {{Experiments with Automatic Proofs in Elementary Analysis}},

language = {english},

abstract = {Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non--clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms.We demonstrate on some concrete examples several heuristic techniques for the automation of natural--style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra.Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions.These techniques are being implemented in the {\em Theorema} system and are able to construct automatically natural--style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.},

number = {18-06},

year = {2018},

month = {April},

keywords = {Satisfiability Checking, Natural-style Proofs, Symbolic Computation},

sponsor = {European project ``Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},

length = {33},

type = {Work in progress},

type = {RISC Report Series},

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

address = {Schloss Hagenberg, 4232 Hagenberg, Austria}

}

### Idempotent Generalization is Infinitary

#### David M. Cerna and Temur Kutsia

RISC. Technical report, RISC Report, 2018. [pdf]**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}

}

### Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL

#### A. Maletzky, F. Immler

In: Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17), Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef (ed.), Proceedings of CICM 2018, Lecture Notes in Computer Science 11006, pp. 178-193. 2018. Springer, ISBN 978-3-319-96811-7. The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16. [url]**inproceedings**{RISC5733,

author = {A. Maletzky and F. Immler},

title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL}},

booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17)}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {11006},

pages = {178--193},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-96811-7},

year = {2018},

note = {The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16},

editor = {Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef},

refereed = {yes},

length = {16},

conferencename = {CICM 2018},

url = {https://doi.org/10.1007/978-3-319-96812-4_16}

}

### Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)

#### A. Maletzky, F. Immler

RISC, JKU Linz. Technical report, May 2018. arXiv:1805.00304 [cs.LO]. [url]**techreport**{RISC5734,

author = {A. Maletzky and F. Immler},

title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)}},

language = {english},

year = {2018},

month = {May},

note = {arXiv:1805.00304 [cs.LO]},

institution = {RISC, JKU Linz},

length = {28},

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

}

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

### Unranked Second-Order Anti-Unification

#### Alexander Baumgartner, Temur Kutsia

Information and Computation 255(2), pp. 262-286. 2017. ISSN: 0890-5401. [url]**article**{RISC5192,

author = {Alexander Baumgartner and Temur Kutsia},

title = {{Unranked Second-Order Anti-Unification}},

language = {english},

journal = {Information and Computation},

volume = {255},

number = {2},

pages = {262--286},

isbn_issn = {ISSN: 0890-5401},

year = {2017},

refereed = {yes},

length = {25},

url = {http://doi.org/10.1016/j.ic.2017.01.005}

}

### Higher-Order Pattern Anti-Unification in Linear Time

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

Journal of Automated Reasoning 58(2), pp. 293-310. 2017. ISSN 0168-7433. [url]**article**{RISC5337,

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

title = {{Higher-Order Pattern Anti-Unification in Linear Time}},

language = {english},

journal = { Journal of Automated Reasoning},

volume = {58},

number = {2},

pages = {293--310},

isbn_issn = {ISSN 0168-7433},

year = {2017},

refereed = {yes},

length = {18},

url = {http://dx.doi.org/10.1007/s10817-016-9383-3}

}

### Gröbner Bases Computation by Triangularizing Macaulay Matrices

#### Bruno Buchberger

Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases) 75, pp. 1-9. 2017. Mathematical Society of Japan, 0.**article**{RISC5586,

author = {Bruno Buchberger},

title = {{Gröbner Bases Computation by Triangularizing Macaulay Matrices}},

language = {english},

journal = {Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)},

volume = {75},

pages = {1--9},

publisher = {Mathematical Society of Japan},

isbn_issn = {0},

year = {2017},

refereed = {no},

length = {9}

}

### Satisfiability Checking and Symbolic Computation

#### Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna Maria , Brain Martin , Buchberger Bruno , Cimatti Alessandro , Davenport James , England Matthew , Fontaine Pascal , Forrest Stephen , Griggio Alberto , Kröning Daniel , Seiler Werner M. , Sturm

ACM Communications in Computer Algebra 50(4), pp. 145-147. 2017. 0.**article**{RISC5587,

author = { Abraham Erika and Abbott John and Becker Bernd and Bigatti Anna Maria and Brain Martin and Buchberger Bruno and Cimatti Alessandro and Davenport James and England Matthew and Fontaine Pascal and Forrest Stephen and Griggio Alberto and Kröning Daniel and Seiler Werner M. and Sturm },

title = {{Satisfiability Checking and Symbolic Computation}},

language = {english},

journal = {ACM Communications in Computer Algebra},

volume = {50},

number = {4},

pages = {145--147},

isbn_issn = {0},

year = {2017},

refereed = {no},

length = {3}

}