Lydia Kondylidou

Hi! I’m Lydia Kondylidou, a PhD student in the Department of Theoretical Computer Science and Theorem Proving at LMU Munich, working under the supervision of Prof. Jasmin Blanchette.

My research interests lie in automated reasoning, with a focus on automated theorem proving and higher-order logic. My PhD explores how to enhance SMT solvers with native support for higher-order reasoning.

contact

email	L.<my last name>@lmu.de
office	Room L 103, Oettingenstr. 67, 80538 Munich, Germany
github	kondylidou

news

Feb 12, 2024	Subreviewer, IJCAR 2024

talks

May 5, 2025	TACAS 2025

publications

Augmenting Model-Based Instantiation with Fast Enumeration

Lydia Kondylidou, Andrew Reynolds, and Jasmin Blanchette

In Tools and Algorithms for the Construction and Analysis of Systems, 2025

Abs HTML PDF

Satisfiability-modulo-theories (SMT) solvers rely on various quantifier instantiation strategies to support first- and higher-order logic. We introduce MBQI-Enum, an approach that extends model-based quan- tifier instantiation (MBQI) with syntax-guided synthesis (SyGuS) tech- niques. Our approach targets first-order theories without well-established quantifier instantiation techniques and higher-order quantifiers that can benefit from instantiations with λ-terms. By incorporating a SyGuS enu- merator, it generates a broader set of candidate instantiations, including identity functions and terms containing uninterpreted symbols, thereby improving the effectiveness of MBQI.