PhD in Computer Science (last activated in 2013)

Course partially running (all years except the first)

Corso “Deduction systems for non-classical logics"

29 Aprile – 4 Giugno 2008 (20 ore)


Academic staff
Luca Vigano'

Series to which this belongs

21° ciclo
22° ciclo
23° ciclo


Non-classical logics such as modal, temporal or substructural logics are extensions or restrictions of classical logic that provide languages for reasoning about knowledge, belief, time, space, resources, and other dynamic `state oriented' properties. As such, they are increasingly finding applications in various fields of computer science, artificial intelligence, cognitive science and computational linguistics. Driven in part by the rising demands of practitioners, there has been an explosion of research in non-classical logics and the development of new application-driven logics. However, developing such logics is a specialized activity that is largely restricted to experts: each new logic demands, at a minimum, a semantics, a deduction system, and metatheorems connecting the two together. This is non-trivial and there is often an ad hoc nature to the entire enterprise where one is forced to find new ways to extend old results or even to start from scratch. A number of non-standard deduction systems have thus been proposed for non-classical logics. In particular, in this course, we will focus on Labelled deduction systems (e.g. natural deduction, sequent and tableaux systems), on the other hand, exploit additional information of a semantic or proof-theoretic nature to provide a means of formalizing and implementing non-classical logics in a uniform, modular and `natural' way. The course is organized in three modules. In the first module, I briefly introduce non-classical logics (their syntax and semantics, and their applications), and then present various labelled deduction systems for them, focusing in particular on modal and substructural logics. I also briefly present implementations of these systems in a typical logical framework such as Isabelle or the Edinburgh LF, and how to use them for semi-automated theorem proving. In the second module, I discuss the proof-theory and semantics of labelled deduction systems, focusing on completeness and normalization results. I also discuss proof-theoretical and semantical limitations of the systems (i.e. what one cannot do with them), especially in comparison with standard approaches, such as Hilbert-style axiomatizations, `unlabelled' natural deduction, and semantics-based translations. In the final module, I show how labelled deduction systems provide a basis for the combination and fibring of logics. I also show how to establish (un)decidability and complexity results for non-classical logics by means of a proof-theoretical analysis of the corresponding labelled deduction systems.