Acknowledgment

I wish to thank the many people who have in one way or other made this thesis possible. First of all, I thank my supervisor Professor Nobuyoshi Asai for all his help, support, and valuable discussions. I also thank all members of the Mathematical Foundation of Computer Science Laboratory, including Yoshikatsu Matsumoto, Wataru Ishikawa, Shingo Ootake and Daisuke Takahashi, for their help and discussions. I would especially like to extend a special thanks to my parents whose support enabled me to complete this work.