Part of our research has been devoted to the study of goal-directed proof procedures for non-classical and modal logics. The underlying idea is to extend the paradigm of deduction typical of logic programming to several families of non-classical logics. One of the main advantages of goal-directed proof-systems with respect to other traditional methods, is that they are more efficient and deterministic for the proof-search. Morever, the proof-systems we have investigated provide a uniform and strongly analytic presentation of each logical system which might be useful for studying properties of logical systems, such as cut-elimination, interpolation and obtaining bounds on the size of proofs [26,16]. This research has been carried on in collaboration with Prof. D. Gabbay of the Imperial College of London. The program has been successfully applied to modal logics of strict implication [17]. We are currently extending it to the so-called substructural logics, a family of logics which includes relevance and linear logic, and has recently gained a great interest for the possible applications in computer science (we just mention: modelling actions and computations, natural language processing, hypothetical reasoning).
Focusing on the specific class of multimodal logics which are characterized by inclusion axioms (and are a subclass of incestual modal logics mentioned above), we have defined a framework for developing modal extensions of logic programming, which are parametric with respect to the properties chosen for the modalities, and which allow sequences of modalities of the form [ t], where t is a term of the language, to occur in front of clauses, goals and clause heads [3,1]. A goal directed proof procedure for the language has been proposed, which is modular with respect to the properties of modalities. A Herbrand theorem has been proved to hold for this class of extended modal clauses, and a fixpoint semantics, which generalizes the standard one for Horn clauses, has been used to prove soundness and completeness of the goal directed proof procedure with respect to Kripke semantics.