First of all, I wish to thank my supervisor Heinrich Herre for his excellent guidance throughout my studies at the University of Leipzig.
I am very much indebted to Peter Steinacker who introduced me to logic and who has always supported and encouraged me during the past several years.
Parts of this thesis were done at the Australian National University, Canberra. I thank John Slaney and other members of the Automated Reasoning Project at the ANU for their helpful discussions.
I thank the numerous other people with whom I had the chance to discuss the various problems I try to solve in the thesis. Their constructive comments have helped me very much to clarify my thoughts and to organize the thesis better. I am especially grateful to Jens Dietrich, Siegfried Gottwald, Georg Meggle, Gerd Wagner, Heinrich Wansing, and Georg Henrik von Wright.
I dedicate this work to my parents.