Prof. Martina Seidl has been a professor in the field of Artificial Intelligence at the JKU since October 1, 2020. Today we are talking with her about why it is important to understand Artificial Intelligence - even if you don’t really understand it at all - and why she uses games in class as part of the educational content.

Ms. Seidl, what is your area of research?
Martina Seidl: My research focuses on symbolic artificial intelligence, which is one of the oldest areas in artificial intelligence (AI). This is where symbols and rules are used to teach an AI how to think and reason logically. My research focuses on rapidly evaluating logical formulas which are represented in true or false statements. For example, these kinds of formulas can be used to express the rules an AI must follow in order to reach a certain goal. This leads to questions such as: "Can we reach the goal at all under the given rules?" or "How expensive is it to reach the goal?”. I address these tasks by conducting research to create techniques and develop tools.

What do you find particularly fascinating about this area?
Martina Seidl: I love the way theory and real-world practices come together. At first, my work seems very theoretical and mathematical because many formalizations and proofs are initially created on paper. But then - once they are developed to a computer program - it’s interesting to see whether or not the new ideas can really result in state-of-the-art advancements. These programs are then carefully evaluated (also as part of competitions) and often lead to tremendous new things. Of course, it is especially exciting when other research groups use and incorporate the techniques and programs in their work to further develop them.

Why is this research even necessary, meaning how will it improve our lives?
Martina Seidl: The formulas I study can be used to express and answer a variety of different questions. Being able to verify the correctness of computer systems and programs has been very successful. These programs can be very complex and it becomes difficult to manually ensure that they are working as they should. This not only involves the hardware and software we find in cell phones and computers, but also in airplanes. Formal methods play an important role in developing critical, safety applications, which are also used in social networks. Additional applications include planning issues, such as creating a school’s timetable, scheduling classrooms and lecture halls at universities, and planning large sports league events.

Why should students take your classes?
Martina Seidl: I make every effort to make sure that theoretical content demonstrates real-world relevance. Often, a gaming component helps spark the students’ interest. For example, it is very easy to automatically solve games like Sudoku using logical formulas.  It is especially important to me to give students an opportunity to try out a program’s strengths and weaknesses themselves by using different formalisms. Also, even during large-size courses, I believe that I try very hard to respond to individual questions and problems. 

What are you currently working on?
Martina Seidl: I am currently working on one issue in particular, namely the correctness of solvers, meaning programs to evaluate logical formulas. If a solver is used to verify that another program is correct, you have to be absolutely sure that the solver itself is correct. In most cases, a solver is so complex that the solver itself cannot be verified and you have to think of another way to be sure that the attained result is correct. Specifically, I use proof theory techniques for this purpose.

What are your hobbies?
Martina Seidl: I have a 9-month old daughter so at the moment, all of my free time is spent with my family.

What else do you want to do or achieve in your life?
Martina Seidl: There are still many research questions that need to be answered and I look forward to an exciting time at the JKU.