@PhDThesis{	  vigano:framework:1997,
  author	= {Luca Vigan{\`o}},
  title		= {A Framework for Non-Classical Logics},
  school	= {Universit{\"a}t des Saarlandes},
  year		= 1997,
  address	= {Saarbr{\"u}cken, Germany},
  month		= sep,
  language	= {USenglish},
  abstract	= {The subject of this work is the development and
		  investigation of a \emph{framework} for the modular and
		  uniform representation and implementation of
		  \emph{non-classical logics}, in particular modal and
		  relevance logics. Logics are presented as labelled natural
		  deduction (or sequent) systems, which are proved to be
		  sound and complete with respect to the corresponding
		  Kripke-style semantics. We investigate the proof theory of
		  our systems, and show them to possess structural properties
		  such as normalization and the subformula property, which we
		  exploit to establish not only general advantages and
		  limitations of our approach with respect to related ones,
		  but also, by means of a substructural analysis,
		  decidability and complexity results for (some of) the
		  logics we consider. All of our proof systems have been
		  implemented in the generic theorem prover Isabelle, thus
		  providing a simple and natural environment for interactive
		  proof development. }
}