Abstract:
The Theorema system (https://www3.risc.jku.at/research/theorema/software) is a complex framework built upon Mathematica (www.wolfram.com/mathematica) that supports the processes of defining mathematical theories, including the definition of algorithms through logical formulae, experimentation by running the algorithms, and the development and use of mechanical provers. The system enhances the synthesis and the certification of algorithms as they are implemented directly in predicate logic along with their specifications, bypassing the need for a programming language. A distinctive feature of the Theorema system is its use of a natural style, similar to human expression, for presenting logical formulae and algorithms, formulating the inference rules of the provers, and displaying proofs.
The tutorial will be based on a live demo of the system showing how to implement and execute definitions, and how to automatically generate proofs by using the existent provers in the system.
Short bio:
Isabela Drămnesc (https://staff.fmi.uvt.ro/~isabela.dramnesc) is Associate Professor at the Department of Computer Science (https://www.info.uvt.ro) of Faculty of Mathematics and Computer Science from
West University of Timișoara (www.uvt.ro). She teaches various subjects: Logic and Functional Programming, Graph Theory and Combinatorics,
Automated Theorem Proving, Algorithm Synthesis and Mathematical Theory Exploration. Her research interests include: logic; automated reasoning; mathematical theory exploration; algorithm synthesis, verification and transformation.
She received her PhD in Computer Science in 2013 from West University of Timișoara under the supervision of
Tudor Jebelean from Johannes Kepler University, Linz, Austria. Afterwards, she was a postdoc at West University of Timișoara
and at INRIA, Sophia-Antipolis, France.
She has experience in European projects both as a member, and also as a manager of the Erasmus+ projects strategic and cooperation partnerships
for higher education “ARC: Automated Reasoning in the Class” (https://www.arc.info.uvt.ro), “AiRobo: Artificial Intelligence based Robotics” (https://airobo.info.uvt.ro).
She received in 2020 the “Mihail Ghermănescu” award for Mathematics and Computer Science from
West University of Timișoara at the sixth edition of Gala Premiilor UVT.
