SemPER
Semantics, Proofs, and Effective Reasoning
Funded by the European Union — Horizon Europe MSCA Staff Exchanges 2025
About the Project
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 contradictions, and modal/temporal epistemic logics — to create 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. In concert 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 provides the essential catalyst: sustained mobility across our vast collaboration network spanning five 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: 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.
Project Details
Horizon Europe • Call: HORIZON-MSCA-2025-SE-01
Instituto de Telecomunicações (IT), Lisbon, Portugal
Work Packages
| WP | Title |
|---|---|
| 1 | Management & Organization |
| 2 | Dissemination & Communication |
| 3 | Schools & Training |
| 4 | Reasoning Across Uncertainty, Norms, and Cognition |
| 5 | Modular Semantics, Duality and Representation |
| 6 | Compositional Proof Systems |
| 7 | Bridges, Transfer Results, and Tractability |
| 8 | Automated Reasoning and Implementations |
| 9 | Applied Logics |
Building on a Legacy
SemPER continues a trajectory of successful European collaborative projects in non-classical logic:
Consortium
Europe • Americas • Asia • Africa • Oceania
Beneficiaries
Associated Partners
Work Packages
SemPER is organised into nine Work Packages. WP1–3 cover management, dissemination, and training. WP4–6 and WP8–9 correspond to the five scientific objectives. WP7 bridges theory and applications.
Management & Organization
- Partnership Agreement
- Management Meetings
- Progress Reports
Dissemination & Communication
- Conferences
- Open Lectures and Interviews
- Workshops
- Special Sessions Organisation
- Project Website
- Social Media
Schools & Training
- Organisation of the First and Second Schools
Reasoning Across Uncertainty, Norms, and Cognition
- Consequence Relations, Meta-properties and Admissibility
- Non-Monotonicity, Paraconsistency, and Reactivity
- Abstract Dualities with Contact Algebras
- Reasoning under Uncertainty — from Fuzzy to Probabilistic
- Reasoning under Constraints and Beyond Deduction
Modular Semantics, Duality and Representation
- LE-logics and Parametric Correspondence
- Dynamic and Reactive Modalities
- Dualities for Enriched Semantics
- Functional and Structural Representations
- Extended truth-functionality via non-determinism
- Coalgebraic frameworks for extended modalities
Compositional Proof Systems
- Multiple-Conclusion and Analytic Natural Deduction Calculi
- Multi-Type Gentzen Extensions
- Relative Expressivity and Metaproperty-Preserving Embeddings
- Cut Control and Proof System Translations
- Tableaux Methods for Non-Classical Logics
Bridges, Transfer Results, and Tractability
- Parametric Correspondences between Semantics and Calculi
- Tracking Complexity in Combinations
- Approximations and Depth-Bounded Reasoning
- Combining Decision Procedures
Automated Reasoning and Implementations
- Semantic Operations and Algebra-based Algorithms
- Mixed Reasoning Frameworks with Context Control
- Prototype Implementations of Analytic Calculi
- Integration with Proof Assistants
- Formalisation of Project Results in Proof Assistants
- Benchmarks and Evaluation
Applied Logics
- Belief Revision, Deontic, Dynamic, and Similarity-Based Reasoning
- Categorization, Deliberation, and Explainable ML
- Logic-based Systems for Legal Reasoning
- Natural Language, Argumentation, and Uncertainty
Outputs
Publications, software, and other outcomes produced during the SemPER project will be listed here.
Check back for new papers, tools, and results from the SemPER network.
Scientific Reports
The project is funded under Grant Agreement No. 101299559.
Events
Conferences, workshops, schools, and other events organized or co-organized by the SemPER network.
Stay tuned for upcoming workshops, conferences, and training schools.
News
Contacts
Project Coordinator
Sérgio Marcelino
Instituto de Telecomunicações (IT)
SQIG — Security and Quantum Information Group
Instituto Superior Técnico, Universidade de Lisboa
Lisbon, Portugal
sergio.marcelino@lx.it.pt