Lydia Kondylidou

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

I’m interested in automated reasoning, particularly automated theorem proving and higher order logic. My PhD subject is achieving higher-order SMT solving by ensuring that extensions of SMT solvers natively support 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

publications

Augmenting Model-Based Instantiation with Fast Enumeration (Work in Progress)

Lydia Kondylidou, Andrew Reynolds, and Jasmin Blanchette

In , 2025

Abs PDF

We introduce MBQI-Enum, an approach that extends model-based quantifier instantiation (MBQI) with syntax-guided synthesis (SyGuS) techniques. 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 enumerator, it generates a broader set of candidate instantiations, including identity functions and terms containing uninterpreted symbols, thereby improving the effectiveness of MBQI.