The project unites mathematicians, computer scientists, and philosophers across logic, algebra, category theory, automated reasoning,
and proof assistants to design modular reasoning systems with provable guarantees and validated prototypes. We draw on the vast
literature of non-classical logics – including graded and probabilistic logics, resource-sensitive (substructural) systems, paraconsistent
approaches that tolerate local contradictions, and modal/temporal/epistemic logics – to capture real-world reasoning that classical logic
cannot. This is made possible through the collaboration of specialists from the two prominent pillars of logic – semantics and proofs.
Not content with theoretical advances, we aim for effective reasoning: algorithms and tools (e.g., proof-assistant libraries, solvers, and
model-checking prototypes) with applications in AI, legal reasoning, and natural language processing. The MSCA Staff Exchange will
provide the essential catalyst: sustained mobility across our vast collaboration network spanning six continents, maximizing existing
collaborations and realizing new collaborations whose need has already been carefully identified. No single group or small consortium
could accomplish the goals of this project. The timing is compelling: after nearly a century of advances, the theoretical and technological
foundations are finally mature for genuine integration, while recent breakthroughs in AI and automated reasoning make the formal
understanding of opaque, black-box systems urgent. In short, this is a cutting-edge programme built on three pillars – Semantics, Proofs, and Effective Reasoning – delivering new theory, working prototypes, and a durable international collaboration.
and proof assistants to design modular reasoning systems with provable guarantees and validated prototypes. We draw on the vast
literature of non-classical logics – including graded and probabilistic logics, resource-sensitive (substructural) systems, paraconsistent
approaches that tolerate local contradictions, and modal/temporal/epistemic logics – to capture real-world reasoning that classical logic
cannot. This is made possible through the collaboration of specialists from the two prominent pillars of logic – semantics and proofs.
Not content with theoretical advances, we aim for effective reasoning: algorithms and tools (e.g., proof-assistant libraries, solvers, and
model-checking prototypes) with applications in AI, legal reasoning, and natural language processing. The MSCA Staff Exchange will
provide the essential catalyst: sustained mobility across our vast collaboration network spanning six continents, maximizing existing
collaborations and realizing new collaborations whose need has already been carefully identified. No single group or small consortium
could accomplish the goals of this project. The timing is compelling: after nearly a century of advances, the theoretical and technological
foundations are finally mature for genuine integration, while recent breakthroughs in AI and automated reasoning make the formal
understanding of opaque, black-box systems urgent. In short, this is a cutting-edge programme built on three pillars – Semantics, Proofs, and Effective Reasoning – delivering new theory, working prototypes, and a durable international collaboration.