**1. Proof theory for intuitionistic and intermediate logics**

The logics taken into consideration are intuitionistic logic,

Dummett's logic and Jankov's logic (characterized, respectively, by linear orders and directed partial orders.).

I have solved some open problems by presenting a cut free calculus for Dummett's logic, and semantic tableaux for intuitionistic logic.

Recently with G.Tassi I have presented a completely new calculus for intuitionistic logic in which the problems of termination and back-tracking are solved. We have done so by a multi-succedent sequent calculus which fulfils the subformula property and the termination property. A decision procedure is defined too so that for any formula either a proof in the given calculus or a counter-model is provided.

Cut-free calculi for both Dummett's logic and Jankov's logic are provided in which the termination property is fulfilled.

**2. Semantics and proof theory for quantified modal logic**

Quantified modal logic has been the main focus of my research. As well known the topic presents many interesting and controversial philosophical aspects and at the same time it is rather difficult to treat by formal methods. A line of attack has been to introduce a new language and a new semantics in order to see clearly the interplay between substitution, modalities, quantifiers and identity.

I work with a language with types and the so-called counterpart semantics. As well known D.Lewis has been the first to introduce the notion of counterpart in order to model the modal discourse.

A language with types is very effective to show all the subtle and critical relations between modalities and substitution, but at the same time it is not handy to deal with. At present, my research is focused on the construction of a modal language which is as expressive and flexible as the language with types and at the same time closer to standard first-order languages.

As to the problem of completeness of quantified modal logics with respect to Kripke semantics I have provided a general method which allows us to show in a uniform way the completeness of several quantified modal logics: with/without the Converse of the Barcan Formula, with/without the Barcan Formula, with/without identity, with/without empty domains.

Moreover I have shown that the free quantified logic B plus the Barcan formula is Kripke incomplete.

**3. Modal languages with indexed modalities**A new language for quantified modal logic has been introduced in which the modal operators are indexed by terms : ``

*it is necessary for t_1, ... , t_n*''. Systems of quantified modal logic are defined in that language and shown to be complete with respect to

*transition semantics*. Formulas such as the Barcan formula, the Ghilardi formula, the necessity of identity can be expressed in a natural way in the new language and are shown to correspond to particular properties of the transition relation.

**4. Epistemic logic**

Indexed operators are proved to be very useful in the analysis of epistemic operators `

*`t knows of t_1, ... , t_n that*''.

**1. Proof theory for weak and intermediate logics**

Logics considered: propositional logics weaker than intuitionistic logic, such as paraconsistent logic and quantum logic. A general completeness theorem is provided.

As to intermediate logics I have considered particularly

Dummett's logic and Jankov's logic (characterized, respectively, by linear orders and directed partial orders.) and

I have solved some open problems by presenting a cut free calculus for Dummett's logic, and semantic tableaux for intuitionistic logic.

Recently with G.Tassi I have presented a completely new calculus for intuitionistic logic in which the problems of termination and back-tracking are solved.

We have done so by a multi-succedent sequent calculus which fulfils the subformula property and the termination property. A decision procedure is defined too so that for any formula either a proof in the given calculus or a counter-model is provided.

Cut-free calculi for both Dummett's logic and Jankov's logic are provided in which the termination property is fulfilled.

**2. Propositional modal logic**

My main contribution is about the extensions of the modal logic S4.3 (characterized by linearly ordered Kripke frames) for which I have provided a new method, the method of diagrams, according to which it is possible to show in a simple and direct way that any extension of S4.3 has the finite model property.

**3. Quantified intermediate logics**

As to the classically quantified extension of Dummett's logic I have solved a long standing problem by showing that that system is characterized by the positive rational numbers with increasing domains.

With S.Ghilardi we have solved another open problem relative to the completeness of the classically quantified extension of Jankov's logic. We have proved that it is complete with respect to the class of directed Kripke frames with increasing domains

**4. Semantics for quantified modal logic**

Quantified modal logic has been the main focus of my research. As well known the topic presents many interesting and controversial philosophical aspects and at the same time it is rather difficult to treat by formal methods. A line of attack has been to introduce a new language and a new semantics in order to see clearly the interplay between substitution, modalities, quantifiers and identity.

I work with a language with types and the so-called counterpart semantics. As well known D.Lewis has been the first to introduce the notion of counterpart in order to model the modal discourse.

A language with types is very effective to show all the subtle and critical relations between modalities and substitution, but at the same time it is not handy to deal with. At present, my research is focused on the construction of a modal language which is as expressive and flexible as the language with types and at the same time closer to standard first-order languages.

As to the problem of completeness of quantified modal logics with respect to Kripke semantics I have provided a general method which allows us to show in a uniform way the completeness of several quantified modal logics: with/without the Converse of the Barcan Formula, with/without the Barcan Formula, with/without identity, with/without empty domains.

Moreover I have shown that the free quantified logic B plus the Barcan formula is Kripke incomplete.

**3. Modal languages with indexed modalities**A new language for quantified modal logic has been introduced in which the modal operators are indexed by terms : ``it is necessary for t_1, ... , t_n''. Systems of quantified modal logic are defined in that language and shown to be complete with respect to

*transition semantics*. Formulas such as the Barcan formula, the Ghilardi formula, the necessity of identity can be expressed in a natural way in the new language and are shown to correspond to particular properties of the transition relation.

**4. Epistemic logic**

Indexed operators are proved to be very useful in the analysis of epistemic operators `

*`t knows of t_1, ... , t_n that*''.