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.