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

## Bruno Buchberger

## Tudor Jebelean

## Teimuraz Kutsia

## Alexander Maletzky

## Wolfgang Windsteiger

## Jakob Praher

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

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

}

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

}

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

}

### An overview of PρLog

#### Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayr

In: Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017, Y. Lierler and W. Taha (ed.), Lecture Notes in Computer Science 10137, pp. 34-49. 2017. Springer, ISBN 978-3-319-51675-2. [pdf]**inproceedings**{RISC5416,

author = {Besik Dundua and Temur Kutsia and Klaus Reisenberger-Hagmayr},

title = {{An overview of PρLog}},

booktitle = {{ Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {10137},

pages = {34--49},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-51675-2},

year = {2017},

editor = {Y. Lierler and W. Taha},

refereed = {yes},

length = {16}

}

### Rewriting Logic from a ρLog Point of View

#### Mauricio Ayala-Rincon, Besik Dundua, Temur Kutsia, Mircea Marin

In: Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) , Sandra Alves and Renata Wasserman (ed.), pp. -. 2017. [pdf]**inproceedings**{RISC5473,

author = {Mauricio Ayala-Rincon and Besik Dundua and Temur Kutsia and Mircea Marin},

title = {{Rewriting Logic from a ρLog Point of View}},

booktitle = {{Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) }},

language = {english},

pages = {--},

isbn_issn = { },

year = {2017},

editor = {Sandra Alves and Renata Wasserman},

refereed = {yes},

length = {16}

}

### Pattern-Based Calculi with Finitary Matching

#### Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia

Logic Journal of the IGPL, pp. -. 2017. Oxford University Press, ISSN 1367-0751. To appear. [url]**article**{RISC5517,

author = {Sandra Alves and Besik Dundua and Mario Florido and Temur Kutsia},

title = {{Pattern-Based Calculi with Finitary Matching}},

language = {english},

journal = {Logic Journal of the IGPL},

pages = {--},

publisher = {Oxford University Press},

isbn_issn = {ISSN 1367-0751},

year = {2017},

note = {To appear},

refereed = {yes},

length = {41},

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

}

### Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks

#### E. Abraham, T. Jebelean

In: ICAI 2017: 10th International Conference on Applied Informatics, G. Kusper (ed.), Proceedings of ICAI 2017: 10th International Conference on Applied Informatics, pp. 0-0. 2017. ISBN 0. In print. [url] [pdf]**inproceedings**{RISC5546,

author = {E. Abraham and T. Jebelean},

title = {{Adapting Cylindrical Algebraic Decomposition for Proof Specific Tasks}},

booktitle = {{ICAI 2017: 10th International Conference on Applied Informatics}},

language = {English},

abstract = {We develop a case study on using quantifier elimination and cylindrical algebraic decomposition for the purpose of finding specific terms for the automation of proving mathematical properties in elementary analysis.Real--life proofs in specific mathematical domains are difficult to automate because of the high number of assumptions necessary for the prover to succeed. In particular, in elementary analysis, it is allmost impossible to find automatically the appropriate terms for the instantiation of universal assumptions and for witnessing the existential goals. We aim at developing such proofs in natural style, in the frame of the{\em Theorema} system.Finding such terms is actually possible by using quantifier elimination (QE) based on cylindrical algebraic decomposition (CAD). However, the current straightforward approach lacks in efficiency, because several redundant calls may be necessary, and because the nature of the problem is slightly different.We study some natural--style proofs, the necessary special terms, and the corresponding usage of the QE/CAD, and identify specific techniques for adapting these algorithms in order to increase their efficiency.The experiments are performed partially in {\em Mathematica} and partially in {\tt SMT-RAT}, the latter used as ``white--box'', which allows to inspect the intermediate results and to adapt certain parts of the algorithms.},

pages = {0--0},

isbn_issn = {ISBN 0},

year = {2017},

note = {In print},

editor = {G. Kusper},

refereed = {yes},

length = {0},

conferencename = {ICAI 2017: 10th International Conference on Applied Informatics},

url = {https://icai.uni-eszterhazy.hu/}

}

### Nominal Unification of Higher Order Expressions with Recursive Let

#### Manfred Schmidt-Schauss, Temur Kutsia, Jordy Levy, Mateu Villaret

In: Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016, M. Hermenegildo and P. Lopez-Garcia (ed.), LNCS 10184, pp. 328-344. 2017. Springer, ISBN 978-3-319-63138-7. [pdf]**inproceedings**{RISC5438,

author = {Manfred Schmidt-Schauss and Temur Kutsia and Jordy Levy and Mateu Villaret},

title = {{Nominal Unification of Higher Order Expressions with Recursive Let}},

booktitle = {{ Proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2016}},

language = {english},

series = {LNCS},

volume = {10184},

pages = {328--344},

publisher = {Springer},

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

year = {2017},

editor = {M. Hermenegildo and P. Lopez-Garcia},

refereed = {yes},

length = {17}

}

### Mathematical Aspects of Computer and Information Sciences

#### Johannes Blömer, Ilias Kotsireas, Temur Kutsia, Dimitris E. Simos, editors

Lecture Notes in Computer Science 10693, 2017. Springer, ISBN 978-3-319-72452-2. [url]**booklet**{RISC5518,

author = {Johannes Blömer and Ilias Kotsireas and Temur Kutsia and Dimitris E. Simos and editors},

title = {{Mathematical Aspects of Computer and Information Sciences}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {10693},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-72452-2},

year = {2017},

edition = { },

translation = {0},

length = {462},

url = {https://doi.org/10.1007/978-3-319-72453-9}

}

### The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema

#### A. Maletzky, W. Windsteiger

In: Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, H. Geuvers, M. England, O. Hasan, F. Rabe, O. Teschke (ed.), Lecture Notes in Computer Science 10383, pp. 25-39. 2017. Springer, ISBN 978-3-319-62075-6. doi 10.1007/978-3-319-62075-6_3. [url] [pdf]**inproceedings**{RISC4536,

author = {A. Maletzky and W. Windsteiger},

title = {{The Formalization of Vickrey Auctions: A Comparison of Two Approaches in Isabelle and Theorema}},

booktitle = {{Intelligent Computer Mathematics: 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21}},

language = {english},

series = {Lecture Notes in Computer Science},

volume = {10383},

pages = {25--39},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-62075-6},

year = {2017},

note = {doi 10.1007/978-3-319-62075-6_3},

editor = {H. Geuvers and M. England and O. Hasan and F. Rabe and O. Teschke},

refereed = {yes},

length = {15},

url = {https://link.springer.com/chapter/10.1007/978-3-319-62075-6_3}

}

### Theorema 2.0: A Brief Tutorial

#### W. Windsteiger

In: Proceedings of SYNASC 2017, Tudor Jebelean and Daniela Zaharie (ed.), Proceedings of SYNASC 2017, IEEE Explore , pp. 1-3. 2017. [pdf]**inproceedings**{RISC5516,

author = {W. Windsteiger},

title = {{Theorema 2.0: A Brief Tutorial}},

booktitle = {{Proceedings of SYNASC 2017}},

language = {english},

abstract = {The Theorema system aims to be a computer assistant for theworking mathematician. Support should be given throughout all phases ofmathematical activity, from introducing new mathematical concepts bydefinitions or axioms, through first (computational) experiments, theformulation of theorems, their justification by an exact proof, theapplication of a theorem as an algorithm, to the dissemination of theresults in form of a mathematical publication, the build up of biggerlibraries of certified mathematical content and the like. One focus lieson the natural style of system input (in form of definitions, theorems,algorithms, etc.), system output (mainly in formof mathematical proofs) and user interaction. When using the Theoremasystem, a user should not have to follow a certain style of mathematicsenforced by the system (e.g. basing all of mathematics on set theory orcertain variants of type theory), rather should the system support theuser in her preferred flavor of doing math. The new implementation ofthe system, which we refer to as Theorema 2.0, is open-source andavailable through GitHub.},

series = {IEEE Explore},

pages = {1--3},

isbn_issn = {?},

year = {2017},

editor = {Tudor Jebelean and Daniela Zaharie},

refereed = {yes},

length = {3},

conferencename = {SYNASC 2017}

}

### 2016

### Stam's Identities Collection: A Case Study for Math Knowledge Bases

#### Bruno Buchberger

In: Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Gert-Martin Greuel, Thorsten Koch, Peter Paule and Andrew Sommese (ed.), pp. 437-442. 2016. Springer International Publishing, Cham, 978-3-319-42432-3. [url] [pdf]**inproceedings**{RISC5324,

author = {Bruno Buchberger},

title = {{Stam's Identities Collection: A Case Study for Math Knowledge Bases}},

booktitle = {{Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings}},

language = {english},

pages = {437--442},

publisher = {Springer International Publishing},

address = {Cham},

isbn_issn = {978-3-319-42432-3},

year = {2016},

editor = {Gert-Martin Greuel and Thorsten Koch and Peter Paule and Andrew Sommese},

refereed = {no},

length = {6},

url = {http://dx.doi.org/10.1007/978-3-319-42432-3_55}

}

### The GDML and EuKIM Projects: Short Report on the Initiative

#### Bruno Buchberger

In: Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, Gert-Martin Greuel, Thorsten Koch, Peter Paule and Andrew Sommese (ed.), pp. 443-446. 2016. Springer International Publishing, Cham, 978-3-319-42432-3. [url] [pdf]**inproceedings**{RISC5325,

author = {Bruno Buchberger},

title = {{The GDML and EuKIM Projects: Short Report on the Initiative}},

booktitle = {{Mathematical Software - ICMS 2016: 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings}},

language = {english},

pages = {443--446},

publisher = {Springer International Publishing},

address = {Cham},

isbn_issn = {978-3-319-42432-3},

year = {2016},

editor = {Gert-Martin Greuel and Thorsten Koch and Peter Paule and Andrew Sommese},

refereed = {no},

length = {4},

url = {http://dx.doi.org/10.1007/978-3-319-42432-3_56}

}

### Satisfiability Checking meets Symbolic Computation (Project Paper)

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

CoRR abs/1607.08028, pp. -. 2016. -. [url] [pdf]**article**{RISC5351,

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

title = {{Satisfiability Checking meets Symbolic Computation (Project Paper)}},

language = {english},

abstract = {Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community. },

journal = {CoRR},

volume = {abs/1607.08028},

pages = {--},

isbn_issn = {-},

year = {2016},

refereed = {yes},

length = {15},

url = {http://arxiv.org/abs/1607.08028}

}

### Proof-based Synthesis of Sorting Algorithms for Trees

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

In: Proceedings of LATA 2016, the 10th International Conference on Language and Automata Theory and Applications, Adrian-Horia Dediu, Jan Janousek, Carlos Martin-Vide, Bianca Truthe (ed.), Proceedings of LATA 2016, LNCS 9618, pp. 562-575. 2016. Springer, ISBN 978-3-319-29999-0.**inproceedings**{RISC5198,

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

title = {{Proof-based Synthesis of Sorting Algorithms for Trees}},

booktitle = {{Proceedings of LATA 2016, the 10th International Conference on Language and Automata Theory and Applications}},

language = {english},

series = {LNCS},

volume = {9618},

pages = {562--575},

publisher = {Springer},

isbn_issn = {ISBN 978-3-319-29999-0},

year = {2016},

editor = {Adrian-Horia Dediu and Jan Janousek and Carlos Martin-Vide and Bianca Truthe},

refereed = {yes},

length = {14},

conferencename = {LATA 2016}

}