Theorema
The software system Theorema provides a uniform logic and software technologic frame for proving, solving, and simplifying formulae in all areas of mathematics. Theorema is developed at the Research Institute for Symbolic Computation (RISC), Austria.
This software is also referenced in ORMS.

Keywords for this software
References in zbMATH (referenced in 149 articles , 4 standard articles )
Showing results 1 to 20 of 149.
Sorted by year (- Drămnesc, Isabela; Jebelean, Tudor: Synthesis of sorting algorithms using multisets in \textitTheorema (2021)
- Drămnesc, Isabela; Jebelean, Tudor: \textitAlCons: deductive synthesis of sorting algorithms in \textitTheorema (2021)
- Dundua, Besik; Kutsia, Temur; Marin, Mircea: Variadic equational matching in associative and commutative theories (2021)
- Jebelean, Tudor: A heuristic prover for elementary analysis in \textitTheorema (2021)
- Xu, Runqing; Li, Liming; Zhan, Bohua: Verified interactive computation of definite integrals (2021)
- Kahl, Wolfram: Calculational relation-algebraic proofs in the teaching tool \textscCalcCheck (2020)
- Carette, Jacques; Farmer, William M.: Towards specifying symbolic computation (2019)
- Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
- Dundua, Besik; Kutsia, Temur; Marin, Mircea: Variadic equational matching (2019)
- Johansson, Moa: Lemma discovery for induction. A survey (2019)
- Carette, Jacques; Farmer, William M.; Laskowski, Patrick: HOL Light QE (2018)
- Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
- Kurtanidze, Lia; Rukhaia, Mikheil: Skolemization in unranked logics (2018)
- Ganesalingam, M.; Gowers, W. T.: A fully automatic theorem prover with human-style output (2017)
- Geuvers, Herman (ed.); England, Matthew (ed.); Hasan, Osman (ed.); Rabe, Florian (ed.); Teschke, Olaf (ed.): Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17--21, 2017. Proceedings (2017)
- Johansson, Moa: Automated theory exploration for interactive theorem proving: an introduction to the Hipster system (2017)
- Maletzky, Alexander; Windsteiger, Wolfgang: The formalization of Vickrey auctions: a comparison of two approaches in Isabelle and Theorema (2017)
- Smallbone, Nicholas; Johansson, Moa; Claessen, Koen; Algehed, Maximilian: Quick specifications for the busy programmer (2017)
- Buchberger, Bruno: The GDML and EuKIM projects: short report on the initiative (2016)
- Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Maletzky, Alexander; Windsteiger, Wolfgang: Theorema 2.0: computer-assisted natural-style mathematics (2016)
Further publications can be found at: http://www.risc.jku.at/publications/