| Acronym: MoLC |
| Main Objective: The growing developments of computer science and artificial intelligence, and their applications in critical areas, demand new formal methods (read logics) able to cope with the reasoning tasks involved in their analysis. Often, these logics combine different features, whose interactions are not well studied, and are thus tailored on a case-by- case basis. Hilbert-style calculi are arguably the most widespread way of defining logics, and also the least studied one. Furthermore This is mostly due to the fact that proofs in Hilbert-calculi are hard to obtain and systematize. It is embarrassing how little is known in general about the logics resulting from small modifications of a given calculus, eg, by simply adding a new logical operator, axiom schema or inference rule. This contrasts with other methods for defining logics, eg, sequent calculi and their well developed proof-theory, or semantic methods involving algebraic and/or relational structures. However each of these alternatives are often tailored to study specific logics and none of them seems to provide the right general framework to study some of the most basic problems. The pervasiveness of Hilbert Calculli seems also to be connected with its minimality, in the sense that the reasoning manipulations are limited to the language of the logic in question, no meta-language is present apart from the very notion of consequence. We intend to capitalize the general results we have obtained (and the techniques developed) in recent years regarding Hilbert calculli in understanding how relevant properties (finite-valuedness, (un)decidability, complexity) emerge from combining (simpler) logical systems. |
| Reference: ITLA |
| Funding: FCT |
| Start Date: 01-11-2017 |
| End Date: 01-11-2020 |
| Team: Sérgio Roseiro Teles Marcelino, Carlos Manuel Costa Lourenco Caleiro |
| Groups: Security and Quantum Information - Lx |
| Partners: |
| Local Coordinator: Sérgio Roseiro Teles Marcelino |
|
|
|
Associated Publications
|
