Universal Logic

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 of extending old results or even to start from scratch. 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.

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.

PREREQUISITES: some familiarity with non-classical logics and basic proof theory.



	Labelled Deductive Systems Luca Vigano Swiss Federal Institute of Technology - Switzerland
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 of extending old results or even to start from scratch. 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. 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. PREREQUISITES: some familiarity with non-classical logics and basic proof theory.		References: The course is based on recent and ongoing work by the lecturer and colleagues. Some relevant publications can be found on my webpage e.g. * Luca Vigano`, Labelled non-classical logics, Kluwer Academic Publishers, 2000. * David Basin, Marcello D'Agostino, Dov M. Gabbay, Sean Matthews, Luca Vigano` (eds.). Labelled Deduction. Kluwer Academic Publishers, 2000. as well as * Dov M. Gabbay, Labelled deductive systems, Clarendon Press, 1996. * Melvin Fitting, Proof methods for modal and intuitionistic logics, Kluwer Academic Publishers, 1983. * Lincoln A. Wallen, Automated deduction in non-classical logics, MIT Press, 1990.