| Publication | Date of Publication | Type |
|---|
Experiments with automated reasoning in the class
Lecture Notes in Computer Science | 2023-06-02 | Paper |
| A heuristic prover for elementary analysis in \textit{Theorema} | 2022-04-22 | Paper |
| \textit{AlCons}: deductive synthesis of sorting algorithms in \textit{Theorema} | 2022-03-31 | Paper |
Automatic Synthesis of Merging and Inserting Algorithms on Binary Trees Using Multisets in Theorema
Mathematical Aspects of Computer and Information Sciences | 2021-12-08 | Paper |
Synthesis of sorting algorithms using multisets in \textit{Theorema}
Journal of Logical and Algebraic Methods in Programming | 2021-02-26 | Paper |
| Theorema 2.0: computer-assisted natural-style mathematics | 2019-09-18 | Paper |
Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
Journal of Symbolic Computation | 2018-06-14 | Paper |
Proof-based synthesis of sorting algorithms for trees
Language and Automata Theory and Applications | 2016-04-13 | Paper |
Synthesis of list algorithms by mechanical proving
Journal of Symbolic Computation | 2015-01-14 | Paper |
Sound and complete verification condition generator for functional recursive programs
Texts & Monographs in Symbolic Computation | 2012-09-14 | Paper |
Using computer algebra techniques for the specification, verification and synthesis of recursive programs
Mathematics and Computers in Simulation | 2009-06-18 | Paper |
Combining logical and algebraic techniques for natural style proving in elementary analysis
Mathematics and Computers in Simulation | 2009-06-18 | Paper |
Functional–Based Synthesis of a Systolic Array for GCD Computation
Implementation and Application of Functional Languages | 2009-03-11 | Paper |
\textit{Theorema}: Towards computer-aided mathematical theory exploration
Journal of Applied Logic | 2007-02-20 | Paper |
| Automated generation of loop invariants by recurrence solving in \texttt{Theorema} | 2007-01-22 | Paper |
Solution lifting method for handling meta-variables in TH\(\exists\)OREM\(\forall\)
Journal of Mathematical Sciences (New York) | 2006-01-03 | Paper |
| scientific article; zbMATH DE number 2217740 (Why is no real title available?) | 2005-10-26 | Paper |
| scientific article; zbMATH DE number 2217820 (Why is no real title available?) | 2005-10-26 | Paper |
| scientific article; zbMATH DE number 2098736 (Why is no real title available?) | 2004-09-07 | Paper |
| scientific article; zbMATH DE number 2098742 (Why is no real title available?) | 2004-09-07 | Paper |
| scientific article; zbMATH DE number 2065273 (Why is no real title available?) | 2004-05-18 | Paper |
| scientific article; zbMATH DE number 1760135 (Why is no real title available?) | 2002-11-06 | Paper |
| scientific article; zbMATH DE number 1822266 (Why is no real title available?) | 2002-10-31 | Paper |
| The TH\(\exists\)OREM\(\forall\) project: A progress report | 2002-07-03 | Paper |
| Using meta-variables for natural deduction in \textit{Theorema} | 2001-10-21 | Paper |
| scientific article; zbMATH DE number 1254011 (Why is no real title available?) | 1999-05-30 | Paper |
| scientific article; zbMATH DE number 1263309 (Why is no real title available?) | 1999-03-16 | Paper |
| scientific article; zbMATH DE number 1254004 (Why is no real title available?) | 1999-02-23 | Paper |
| scientific article; zbMATH DE number 934894 (Why is no real title available?) | 1997-03-25 | Paper |
Bidirectional exact integer division
Journal of Symbolic Computation | 1997-01-22 | Paper |
| scientific article; zbMATH DE number 935096 (Why is no real title available?) | 1996-11-12 | Paper |
A double-digit Lehmer-Euclid algorithm for finding the GCD of long integers
Journal of Symbolic Computation | 1996-03-07 | Paper |
| scientific article; zbMATH DE number 572192 (Why is no real title available?) | 1994-06-16 | Paper |
| scientific article; zbMATH DE number 572172 (Why is no real title available?) | 1994-05-24 | Paper |
| scientific article; zbMATH DE number 572193 (Why is no real title available?) | 1994-05-24 | Paper |
An algorithm for exact division
Journal of Symbolic Computation | 1993-08-25 | Paper |
| scientific article; zbMATH DE number 6288 (Why is no real title available?) | 1992-06-25 | Paper |
| scientific article; zbMATH DE number 4052983 (Why is no real title available?) | 1987-01-01 | Paper |
| scientific article; zbMATH DE number 3900129 (Why is no real title available?) | 1985-01-01 | Paper |
| scientific article; zbMATH DE number 3874643 (Why is no real title available?) | 1984-01-01 | Paper |
| scientific article; zbMATH DE number 3874644 (Why is no real title available?) | 1984-01-01 | Paper |
