PhD defences & YouTube

Automated reasoning is a core branch of artificial intelligence that enables machines to perform logical inference, solve complex problems, and make transparent decisions. While large language models like GPT show strong language understanding, they still lack reliable logical reasoning, especially under uncertainty. Neural-symbolic AI seeks to bridge this gap by combining the pattern recognition of neural networks with the structured logic of symbolic systems. My research advances this direction by developing formal logic frameworks for conceptual, causal, and defeasible reasoning—allowing AI to classify and explain concepts, represent and reason about causality, and update conclusions when exceptions arise. These capabilities enhance the explainability, adaptability, and trustworthiness of next-generation AI systems.

My thesis develops logical and algebraic frameworks connecting categorization and decision-making, grounded in Formal Concept Analysis (FCA) and modal logic. It introduces novel description logics that integrate FCA with classical systems, enabling efficient conceptual reasoning within the FCA framework. The work further models multi-agent deliberation via interrogative agendas, uncovering structural correspondences between categorization systems, deliberation and decision-making. Finally, these theoretical insights are applied to the design of explainable algorithms for outlier detection, uniting formal methods with practical applications to interpretability.

My thesis focuses on the study of the mathematical (specifically: algebraic and order-theoretic) structures underlying input/output logic. Building on insights from Abstract Algebraic Logic and on the recent introduction of subordination algebras and related structures as a semantic environment for input/output logic, the present thesis establishes a strong and systematic bridge between areas of logic which have been investigated for decades independently of each other, and by doing so, it opens new possibilities of interpretations and areas of applications for these formal frameworks.

This thesis presents a unified, computational, and algebraic exploration of correspondence and inverse correspondence theory across a wide landscape of modal and non-classical logics. Building on the insight that correspondence phenomena depend on a small set of order-theoretic principles, it advances the framework of unified correspondence, which reveals deep structural commonalities among diverse logical systems, including LE-logics, substructural logics, intuitionistic and bi-intuitionistic logics, and many-valued settings. The first part establishes new complexity bounds for identifying inductive axioms—the class on which the algorithm ALBA is guaranteed to succeed—and provides efficient methods for computing their first-order correspondents. The second part develops a general inverse correspondence theory, introducing an algorithm that reconstructs inductive axioms from suitable first-order conditions. The final part investigates how different relational semantics yield systematically related correspondents, laying foundations for parametric correspondence.

My dissertation explores the connections between labelled sequent calculi and display calculi, two foundational proof-theoretic frameworks that, despite differences in syntax, structural constraints, and historical motivations, are shown to be deeply intertwined through the duality of their semantic underpinnings. Furthermore, it applies the two frameworks to investigate the properties of (D) LE logics. Central to this exploration is the transfer of ideas and techniques between these calculi via their semantic common ground, specifically relational and algebraic semantics.