本論文では,依存論理の重要な部分クラスである一階依存論理の構文と意味を定義し,その健全かつ準完全な公理系を導入する. さらに,一階依存論理にif文を表す特殊公理を追加した体系が, 任意の一般帰納的関数を定義できることを示す. また, 依存 論理の適用例としてデータベース設計変更問題を取り上げる. データベース設計変更問題とは, 変更前後のスキーマS,S'が 与えられたとき,SのもとでのインスタンスIをS'のもとでのインスタンスに変換する問題である. この問題を依存論理 の枠組内で形式的に定義し, 依存論理における推論を用いた解法を提案する.