Anela Lolić is a researcher in logic and proof theory in the Theory and Logic group at the Institute of Logic and Computation at TU Wien, where she focuses on computational proof theory and automated deduction. Her work contributes to advancing theoretical foundations in logic with applications to automated reasoning and computer science.
She completed her PhD in Computer Science (Logic) at TU Wien in 2020, with earlier degrees including an MSc in Computational Intelligence from TU Wien and a BSc in Computer Science from JKU Linz. Her doctoral work and ongoing research explore automated proof analysis and structural proof theory.
She has received multiple fellowships and awards, including competitive funding such as the Austrian Science Fund’s Elise Richter Program and the Austrian Academy of Sciences’ APART-MINT and DOC fellowships, and prizes like the SILFS Prize for Women in Logic. She has also served in the Kurt Gödel Society, including as publicity chair from 2015 to 2022, and as treasurer from 2022 to 2025, and organizes academic summer schools, workshops, and conferences.

Project: Skolemization and Equality
Equality is a fundamental concept in mathematics, logic, and everyday life – whether we use different terms to represent the same number (such as ‘two plus two’ and ‘four’) or different names for the same person. In research, equality is particularly important in proofs and automated theorem proving.
A key method in logic is Skolemization, where specific variables in formulas are replaced by new function symbols (Skolem functions) to simplify proofs. While Skolemization is well-studied, the reverse process, called de-Skolemization, poses challenges, especially when equality is part of the proofs. This reversal is however essential to transform machine-generated proofs into clear, human-readable formats.
Our research project aims to develop methods for efficiently removing Skolem functions in proofs involving equality. This will not only provide new theoretical insights into the complexity of de-Skolemization but also advance practical applications in automated reasoning. The results could contribute to making computer-based proof systems more understandable and effective